Resets - SVA: The Power of Assertions in SystemVerilog - page 296

a_sync_accept: assert property (

1

@( posedge clk)

2

sync_accept_on (retry)

3

a |=> b

4

) else $error("FAIL");

5

Fig. 13.8 Concurrent assertion with synchronous aborts

a_sync_accept_reject: assert property (

1

@( posedge clk)

2

sync_accept_on (retry)

3

a |=> sync_reject_on (bad) b[ * 2]

4

) else $error("FAIL");

5

Fig. 13.9 Concurrent assertion with nested synchronous aborts

13.1.2.2 Synchronous Aborts

The synchronous abort operators sync_accept_on and sync_reject_on behave
the same as their asynchronous counterparts with the exception that their abort
conditions are only checked in time steps in which there is an occurrence of the
clocking event.
Figure 13.8 shows a concurrent assertion with a synchronous abort. The assertion
behaves like a_accept in Fig. 13.4 except that the abort condition retry is only
checked in time steps in which posedge clk occurs. In the waveform in Fig. 13.5 ,
the evaluation of the synchronous abort property for the attempt of a_sync_accept
that begins in time 20 is aborted, but not in the time step after time 35 as in the case
of the asynchronous abort. Instead, the synchronous abort occurs at time 40, where
there is an occurrence of posedge clk and the sampled value of retry is 1'b1 .
This illustrates the fact that if the sampled value of an abort condition is 1'b1 in the
same time step that the underlying property evaluation would complete, the abort
condition takes precedence and the evaluation is aborted. Since the abort is of the
“accept” form, the evaluation of the synchronous abort property passes at time 40,
hence there is an overall pass for the concurrent assertion.
Figure 13.9 shows the result of rewriting a_accept_reject from Fig. 13.6
using synchronous aborts. Figure 13.10 shows the same waveform as Fig. 13.7 ,
but with arrows adjusted for the evaluations of a_sync_accept_reject . The pulse
on retry beginning at time 55 is not relevant to the synchronous abort because it
does not affect the sampled value at a tick of the clock. Therefore, the evaluation
beginning at time 20 is aborted at time 60. The clock ticks at this time, and the
sampled value of bad is 1'b1 . Therefore, the inner abort condition causes failure of
the consequent of |=> , hence failure of the overall concurrent assertion, and the
failing action block executes. The evaluation that begins at time 60 behaves the same
as that of a_accept_reject because both evaluations become sensitive to bad at
time 80, which is a tick of the clock at which the sampled value of bad is 1'b1 .