Hardware Reference
In-Depth Information
Fig. 11.6
Sequence
conjunction
r
clock ticks
s
Solution:
a1:
assert property
(req ##1 ack[->1] |-> ready);
Discussion:
As we discussed in Sect.
11.1.2
, this assertion may not be efficient
in simulation when
req
persists until
ack
, and
ack
is sent long time after
req
is
asserted or if
ack
is not sent at all. It is possible to modify assertion
a1
to limit the
time of waiting for
ack
to some predefined number of clock ticks, for example, 10:
a2:
assert property
(
(req ##1 ack[->1])
intersect
1[
*
1:10] |-> ready);
If
ack
is asserted within 10 clock ticks from
req
issue, assertion
a2
behaves
like assertion
a1
; otherwise, the assertion evaluation attempt is ignored. If it is
known that
ack
always arrives within 10 clock ticks, assertion
a2
is more efficient
in simulation than assertion
a1
for most industrial simulators.
Note that
1[
*
1:10]
could be replaced by
1[
*
2:10]
since the antecedent takes
at least two clock ticks.
t
Efficiency Tip.
Antecedent truncation is not efficient for formal verification. As
mentioned in Sect.
20.6
, the efficiency requirements for assertion checking in
emulation are usually aligned with the requirements for FV rather than with
simulation. Therefore, in emulation it is also better to avoid antecedent truncation,
though it is less critical than in FV.
Throughout.
The sequence operator
throughout
introduced in Sect.
11.1.1
is a
special case of
intersect
:
e
throughout
s
is equivalent to
e[
*
]
intersect
s
.
Since
throughout
does not introduce new event combinations, it is efficient both
in simulation and in FV.
11.1.5
Sequence Conjunction
Conjunction
of two sequences
r
and
s
is a sequence
r
and
s
. It has a match in
clock tick t iff one of the sequences r and s has a match in that clock tick, and the
other sequence has a match in some clock tick t
1
t , as illustrated in Fig.
11.6
Sequence conjunction belongs to the
intersect
family, and
r
and
s
is a
shortcut for
r ##1 1[
*
]
intersect
s
or
r
intersect
s ##1 1[
*
]
.
Search WWH ::
Custom Search