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