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

a_accept_reject: assert property (

1

@( posedge clk)

2

accept_on (retry)

3

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

4

) else $error("FAIL");

5

Fig. 13.6 Concurrent assertion with nested asynchronous aborts

10 20 30 40 50 60 70 80 90 100

clk

retry

bad

a

b

Fig. 13.7 Waveform for a_accept_reject

matching the antecedent a and advancing to the next occurrence of posedge clk ,
as specified by |=> . Only at that point does the evaluation become sensitive to the
inner abort condition.
Figure 13.7 shows a waveform for a_accept_reject . The evaluation attempt
that begins at time 20 begins executing the outer abort, becomes sensitive to the
abort condition retry , and matches the antecedent of |=> at time 20. The evaluation
then advances to time 40 and begins executing the inner abort. At that time, it
becomes sensitive also to the abort condition bad and tests that the sampled value of
b is 1'b1 . The evaluation then continues toward time 60 and encounters both retry
and bad in the time step after time 55. In this situation, the outer abort condition
takes precedence. Therefore, the evaluation of the outer abort property aborts and
passes in that time step, and hence the overall evaluation of the concurrent assertion
also passes. The evaluation that begins at time 60 starts similarly. The fact that the
sampled value of bad is 1'b1 at time 60 is irrelevant because this evaluation is not
yet sensitive to the inner abort condition. After matching the antecedent of |=> ,the
evaluation advances to time 80. The glitch on retry at time 65 is not observable
by the abort operator. The evaluation does not abort in the time step after time 75
because, again, it is not yet sensitive to bad . At time 80, though, the evaluation
becomes sensitive to bad . Since the sampled value of bad is 1'b1 at time 80, the
evaluation of the inner abort property aborts and fails in that time step. This causes
the consequent of |=> to fail. Therefore, the overall evaluation of the concurrent
assertions fails at time 80 and the failing action block executes.