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

When always procedure block B1 gets triggered because of its sensitivity to implicit
events, the nonblocking assignment to r11 gets scheduled. Next, if c1_long is
false, no further action takes place. Otherwise, nonblocking assignment to r12 is
scheduled. An instance of assertion a18 is now placed in the procedural assertion
queue associated with B1 . Assume that no other implicit events occur in the Active
region. Eventually the simulation control moves to the Observed region. In the
Observed region, the instance of a18 is still in the procedural assertion queue, so it is
moved to the matured assertion queue. If the leading clock posedge clk occurred
in the Active region, then an evaluation attempt of a18 is initiated in the current time
step in the Observed region. Otherwise, a18 stays in the matured queue pending a
tick of posedge clk in a future time step. Once an evaluation attempt matures, it
continues its evaluation at every clock tick until it completes, independently of any
other attempt that may be initiated. t

Now, let us see how an extraneous assertion attempt is blocked from evaluation.
Suppose in Example 14.18 that multiple right-hand terms of the nonblocking
assignments are updated in the Active region of a time step. This causes multiple
occurrences of the implicit event for B1 . Assume also that c1_long is true
throughout the time step. To be specific, assume that first v11 gets a new value, and
then later in the Active region processing v12 get a new value. When v11 changes,
B1 gets triggered, and, as above, an instance of a18 is placed in the procedural
assertion queue for B1 . Then, when v12 changes, B1 is again triggered. This second
trigger of B1 causes all pending instances in the procedural assertion queue for B1
to be purged. Since we are assuming c1_long remains true, the second procedural
execution of B1 causes an instance of a18 to be placed in the procedural assertion
queue for B1 . In general, whenever a procedural block is triggered, all assertions
pending in the procedural assertion queue for that block are purged. No matter how
many times B1 is triggered in the Active region, only the instance of a18 from the
last execution of B1 can remain in the procedural assertion queue at the end of the
Active region. The one surviving instance subsequently matures in the Observed
region and awaits arrival of a tick of posedge clk to continue evaluation. By
purging pending assertions each time the procedural block is triggered, the effect
of zero-width glitches within a single time step is eliminated.

Triggering a procedural block causes immediate purging of its procedural
assertion queue. This prevents multiple invocations of the same procedural
concurrent assertion due to zero-width glitches.

Furthermore, the semantics also takes care of the situation where multiple
invocations are made to an assertion within a for-loop. The procedural assertion
queue for a block is purged only on triggering of that block. Multiple executions
of a statement within the block, as in the body of a loop, do not themselves cause
purging of the queue.