Procedural Concurrent Assertions - SVA: The Power of Assertions in SystemVerilog - page 318

procedural assertion queue, with a transfer to the matured assertion queue in the
Observed region, assuming no more triggers of B1 in this Active region. Now, in
the Reactive region, when variable v11 is assigned 1 , it causes the initiation of the
Active region once again, re-triggering block B1 . The procedural assertion queue for
B1 is purged, but the previous instance of a23 has already matured, so the purging
has no effect. Then another instance of assertion a23 is entered in the procedural
assertion queue. Finally, that assertion evaluation is also transferred to the matured
queue when the Observed region is entered for the second time. At that point, there
are now two instances of a23 in the matured assertion queue that await their clock
tick.

t

14.7 Dealing with Unwanted Procedural Assertion

Evaluations

As we learnt from Example 14.23 , there are some situations where redundant
evaluations of assertions occur. The user is provided with an explicit means to stop
such cases. The procedural assertion queue can be purged entirely or for a specific
assertion with the disable statement. But, the evaluation attempts already advanced
to the matured queue or the ongoing attempts that were started in previous time steps
are not affected.
The example below modifies Example 14.23 by adding a disable statement
for the assertion to prevent the extra evaluation of a24 in case both posedge v11
and posedge v12 occur in the same time step. Crafting the conditions for such a
disable statement can be delicate.
Example 14.24.

A disable statement purging an assertion evaluation:

program prg();
integer i;
initial
for (i=0; i<8 ; i++) begin
mod.v11= 1;
#5;
mod.v11 = 0;
end
endprogram
module mod( input bit sig2,clk);
bit v11,r11,r12;
wire v12;
assign v12 = sig2;
always @( posedge v11 or posedge v12) begin :B1
r11 = v11 | v12;
a24: assert property (@( posedge clk) v11 |=> v12);
r12 = v11 & v12;
if (v11 && !$sampled(v11) && v12 && !$sampled(v2))
disable a24;