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

end
endmodule
The entry of assertion a24 is removed by the disable statement under the condition
that both v11 and v12 are high and posedge events have been seen on both in the
timestepsofar. t

Evaluation attempts already in the matured queue or ongoing from previous
time steps are not affected by the disable statement.

In some cases, purging of all assertions for a block may be appropriate. This
can be accomplished by executing a disable statement with the block name as its
target. Bear in mind that such a disable applies to all code in the block, not just
the procedural concurrent assertions.

Example 14.25. A disable statement purging all assertion evaluations in a block:

always @( * ) begin :B2
a25_1: assert property (@( negedge clk) !(dreg & tr));
if (c1_long) begin
for ( int i=0; i<4; i++) begin
dreg[i] = tr[i+1];
treg = flogic (dreg[i]);
a25_2: assert property (@( posedge clk) dreg[i] |=> r12);
end
end
if (retry_cond) disable B2;
end
Assume that retry_cond signals a condition under which all instances of assertions
of block B2 should be purged from the procedural assertion queue. This can be
accomplished with the disable targeting the whole block B2 .If retry_cond is true,
then the instance of a25_1 and all instances of a25_2 are purged from the procedural
assertion queue. Otherwise, the instances mature and are evaluated normally. By
placing the disable at the end of the block, it doesn't disturb any of the assignments
made in the block.

t

To conclude this section, we mention that a formal verification tool may extract
the procedural assertions from the procedures as shown in Example 14.16 , including
the enabling conditions, and evaluate them as regular concurrent assertions. Such
extraction may create differences between the simulation and formal verification
semantics. For more details on formal verification, see Chap. 21 .