Hardware Reference
In-Depth Information
1 program prog( output b, ...);
2 assign b = ...;
3 ...
4 endprogram
5 module mod2(...);
6 wire a, b;
7 prog(. * );
8 assign a = ...;
9 a3: assert final (a == b);
10 endmodule
Fig. 4.6
Final Deferred assertion
As we can see, in spite of a glitch in simulation, this glitch does not affect the
behavior of deferred assertion a2 .
t
Example 4.2. Using final deferred assertion as shown in Fig. 4.6 .
Consider what happens at time 50 for the same simulation order as described in
Sect. 4.2.2 .
Active region :
￿Line 8 is executed. a is assigned the value 1, b is still keeping its old value 0.
￿Line 9 is executed. Since a and b at this point have different values, the fail action
entry of the assertion a3 is placed into the deferred assertion report queue.
Reactive region :
￿Line 2 is executed and b is assigned the value 1.
Active region :
￿Line 9 is executed again due to a change of value in b . The previous fail action
entry of this assertion is removed from the deferred assertion report queue, and
the success action entry is placed there instead. As the success action is void,
effectively only the success result is placed into the entry.
Postponed region : The final deferred assertion report queue entry matures. All
actions from the deferred assertion report queue are executed. Since in our case
the queue entry is without an action block, no actions are executed. A tool may,
however, choose to report a success result for assertion a3 .
As we can see, in spite of a glitch in simulation that spanned the Active-Reactive-
Active regions, this glitch does not affect the behavior of deferred assertion a3 .Ifthe
final assertion were replaced by an observed one, the glitch would not be filtered out
and the failure caused by a value change of a as well as the success caused by the
value change of b would be reported.
t
The above examples illustrate one case of flushing the results of deferred
assertions. There are other circumstances where the act of flushing is also needed.
In all, flushing should be perceived as unconditional when its enclosing process
encounters one of the following situations.
Search WWH ::




Custom Search