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

control #5 blocks further evaluation in the Active region. In the Observed region the
instance of a20_1 is transferred to the matured assertion queue, pending the arrival
of its clock. Due to the blocking effect of the delay control statement, multiple
triggerings of B1 in the same time step cannot occur since the process is suspended.
The behavior of a20_2 is quite different. After the delay of five units of time,
the procedural block restarts its evaluation in the Active region, and an instance
of a20_2 enters the procedural assertion queue for B1 .If B1 is not triggered again
prior to the Observed region in the same time step, then a20_2 is transferred to
the matured assertion queue. Otherwise, triggering B1 causes assertion a20_2 to be
purged from the procedural assertion queue. Execution of B1 would continue until
the delay control statement, without rescheduling a20_2 in that time step. t

The following variant of Example 14.20 switches the delay control from #5 to
#0 , significantly changing the assertion evaluation behavior.
Example 14.21. Assertions interleaved with a #0 delay control statement:

always @( * ) begin :B1
r11 <= v11 | v12;
a21_1: assert property (@( posedge clk) v11 |=> v12);
#0;
r12 <= v12 & v13;
a21_2: assert property (@( posedge clk) r11 |=> r12);
end
When B1 is triggered, an instance of a21_1 is placed in the procedural assertion
queue for B1 . Execution of #0 suspends the procedure and schedules its resumption
in the Inactive region of the current time step. When the Active region processing
finishes, Inactive region events are moved to Active and the procedure resumes. At
that point, the instance of a21_1 is flushed from the procedural assertion queue.
Because of this flushing, a21_1 can never survive to the Observed region to mature.
After the #0 delay, an instance of a21_2 is placed in the queue. That instance will
mature provided B1 is not triggered again before the Observed region. t

Another peculiar situation transpires when the event control of the always
procedure is different than the clock of the assertion, as in the example below.

Example 14.22. An assertion with a different clock than its always procedure:

always @( posedge clk) begin
i3 <= lb1 && lb8;
i4 <= lb2 && lb11;
end
always @( posedge e1) begin
d1 <= i1 + i2 ;
a22: assert property (@( posedge clk)d1|=>(i3||i4));
dout <= f_ecap(d1);
end