Hardware Reference
In-Depth Information
Example 5.5.
For a Boolean expression
e
,
always
e
is true iff
e
is true in every
clock tick.
t
Example 5.6.
What is the meaning of
nexttime always
p
?
Solution:
According to the definition of
nexttime
property,
always
p
should hold
in clock tick 1. Therefore, property
p
should hold in every clock tick starting from
clock tick 1.
t
Example 5.7.
What is the meaning of
always nexttime
p
?
Solution:
According to the definition of
always
property,
nexttime
p
should hold
in every clock tick. Therefore, property
p
should hold in every clock tick starting
from clock tick 1.
Discussion:
Properties
always nexttime
p
and
nexttime always
p
(Example
5.6
) are equivalent.
t
Example 5.8.
What is the meaning of
always always
p
?
Solution:
According to the definition of
always
property,
always
p
should hold in
every clock tick. Therefore, property
p
should hold in every clock tick.
Discussion:
It follows that
always always
p
is equivalent to
always
p
, and that
the outer
always
in this case is redundant.
t
Efficiency Tip.
Simulation performance of
always always
p
may be much
inferior to that of
always
p
(see Sect.
4.4.1
) if it is required to maintain information
about all evaluation attempts that are in progress (for example, for debugging
purposes).
5.3.1
Implicit Always Operator
The
always
operator is useful for specifying system invariants. As we discussed
in Sect.
4.4.6
, all concurrent assertions placed outside procedural code are contin-
uously monitored. This means that there is an implicit outermost
always
operator
which defines a series of evaluation attempts. Consequently, the following assertions
a1
and
a2
are equivalent in the sense that either both pass or both fail.
a1:
assert property
(@clk p);
is equivalent to
initial
a2:
assert property
(@clk
always
p);
However, simulation reporting may be different, as explained in Sect.
4.4.1
,
because
a1
has as many evaluation attempts as there are clock ticks, while
a2
has
only one attempt.
Search WWH ::
Custom Search