Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 63

1 module mod1( output b, ...);
2 assign b = ...;
3 ...
4 endmodule
5 module mod2(...);
6 wire a, b;
7 mod1(. * );
8 assign a = ...;
9 a2: assert #0 (a == b);
10 endmodule

Fig. 4.5 Observed Deferred assertion

Let us recall that a deferred assertion is evaluated as a result of a process
execution control reaching the location of the assertion. This linkage of an assertion
with the process is essential when determining whether to flush the assertion from
the deferred assertion report queue. When a process is retriggered it causes only
those previous entries of the assertion results to be flushed that are linked with the
process. To explain this, consider a function containing a deferred assertion. The
function can be invoked from two different processes in the same time slot, resulting
in a separate entry in the deferred assertion report queue for each process, but for the
same assertion. If an entry is later flushed it is determined according to the process
that initiated that action.
The following two examples revisit the example in Fig. 4.4 by replacing the
immediate assertion first with an observed deferred assertion and then with a final
deferred assertion. In the latter case, the scopes of the assertion and the assignments
are also indicated.

Example 4.1. Using observed deferred assertion as shown in Fig. 4.5 .
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 a2 is placed into the deferred assertion report queue.
￿Line 2 is executed and b is assigned the value 1.
￿Line 9 is executed again. The previous fail action entry of this assertion is flushed
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.

Observed region : The observed deferred assertion report queue entry matures.
Reactive region : 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 a2 .