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

Fig. 14.1 The role of queues for procedural assertions

Each procedure containing a concurrent assertion uses its own procedural
assertion queue to enter and purge the assertion attempts.

Figure 14.1 illustrates the role of the two queues.
We will see later how an assertion gets removed from the procedural assertion
queue. First, let us follow an example to see how events cause assertion evaluation.

Example 14.18. Implicit events triggering assertion evaluation:

always @( * ) begin :B1
r11 <= v11;
if (c1_long) begin
r12 <= v12 & v13;
a18: assert property (@( posedge clk) r11 |=> r12);
end
end