Hardware Reference
In-Depth Information
If both
a
and
b
are Boolean,
a
and
b
has a match iff both
a
and
b
are true.
Therefore, in this case
a
and
b
has the same meaning as
a&&b
.
4
Example 11.17.
Two transactions t1 and t2 start at the same time when
start_t
is
asserted. When both transactions complete,
ready
should be asserted. Transaction
completion is signaled by
end_t1
and
end_t2
, respectively.
Solution:
a1:
assert property
(start_t ##1 (end_t1[->1]
and
end_t2[->1])
|-> ready);
The antecedent matches when the longer of the two transactions completes.
t
Sequence Conjunction Versus Property Conjunction.
As the sequence and
property conjunctions have exactly the same syntax, how to distinguish between
a conjunction of two sequential properties and a sequence conjunction promoted
to a property? For example, in property
en |-> r
and
s
, where
r
and
s
are
sequences, should
r
and
s
be interpreted as sequences with
and
as a sequence
conjunction, or should they be interpreted as properties with
and
as a property
conjunction? The answer is the same as in the case of disjunction (see Sect.
6.6
):
if the conjunction arguments are sequences, it is a sequence conjunction. Note,
however, that essentially the result may be interpreted either way, both definitions
agree (this is also the case with disjunction), provided that the resulting sequence is
promoted a property.
Efficiency Tip.
Sequence conjunction has a reasonable overhead in simulation, but
in FV it may be expensive when it defines many different combinations of events
(this is similar to the situation with
intersect
, see Sect.
11.1.4
). However, top-level
conjunction in a sequence promoted to property is not expensive.
Example 11.18.
In property
en |-> r
and
s
, the sequence conjunction in the
consequent is not expensive in FV, since
r
and
s
is promoted to a property, and
and
is its top-level conjunction. This is because in that case sequence
and
can be
converted to a property
and
with equivalent behavior.
In property
en |-> (r
and
s)##1 a
,
and
is not a top-level conjunction pro-
moted to property, hence the conjunction may be expensive.
In property
(r
and
s)|-> p
, the conjunction is in the antecedent of a suffix
implication, the antecedent is never promoted to a property, hence the conjunction
may be expensive.
t
4
Except when
a
or
b
has a match item, see Chap.
16
.
Search WWH ::
Custom Search