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

10 20 30 40 50 60 70 80 90 100

clk

retry

a

b

Fig. 13.5 Waveform for a_accept

property begins. This starts monitoring of the abort condition, using sampled values
of retry , and also starts evaluation of the underlying property. Because the abort is
asynchronous, the sampled value of retry is checked in every time step, including
the first, that the evaluation of the underlying property is ongoing and has neither
been aborted nor already completed on its own. If the sampled value of retry is
1'b1 in any of these checks, then the evaluation is aborted and passes in that time
step. If the evaluation is not aborted, then it completes when the underlying property
evaluation completes (i.e., at the next occurrence of posedge clk ) and the result of
the evaluation is the same as that of the underlying property.
The difference between Figs. 13.1 and 13.4 is that in the former the condition is
not sampled and the outcome of evaluation when the condition is true is disabled ,
and in the latter the sampled value is used and the outcome is success .
Figure 13.5 shows an example waveform for a_accept . It is similar to Fig. 13.2
and will illustrate differences between an asynchronous abort and a disable clause.
The evaluation attempt of a_accept that begins at time 20 is aborted in the first
time step after time 35 and passes at that time. The evaluation does not abort at
time 35 because sampled value of retry is 1'b0 in that time step. The sampled
value of retry at time 40 is 1'b1 , so the attempt beginning at time 40 immediately
aborts and passes in that time step. The 0-width glitch on retry at time 60 does not
affect any sampled value, so the evaluation beginning at time 60 is not aborted. This
evaluation fails at time 80. The evaluation beginning at time 80 is also not aborted
and passes at time 100.
Abort operators may be nested. The scope of the outer abort condition includes
any nested abort property. The scope of the nested abort condition is limited to the
underlying property of that abort operator. While evaluating the inner abort property,
the outer abort condition takes precedence over the inner abort condition in case both
conditions occur in the same time step.
Figure 13.6 shows a concurrent assertion with nested asynchronous aborts. The
outer abort is an accept_on with abort condition retry whose scope is the entire
property of the concurrent assertion. The inner abort is a reject_on with abort
condition bad whose scope is the consequent of |=> . The entire assertion is singly
clocked by posedge clk . The inner abort does not begin evaluation until after