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

a_accept: assert property (

1

@( posedge clk)

2

accept_on (retry)

3

a |=> b

4

) else $error("FAIL");

5

Fig. 13.4 Simple concurrent assertion with an asynchronous abort

a_simple_abort: assert property (

1

@( posedge clk)

2

start

3

|=>

4

accept_on (retry) check_trans_complete

5

);

6

Line 5 specifies an asynchronous accept_on with retry as abort condition. The
underlying property is the instance check_trans_complete .
Aborts behave similarly to a disable clause in the way that they preempt evalua-
tion of the underlying property, but there are a number of important differences:

￿ The scope of an abort condition is limited to its underlying property operand,
not the entire concurrent assertion. A thread or subthread of evaluation does
not become sensitive to the abort condition until it reaches the associated abort
operator.
￿ Abort conditions are always checked using sampled values. Therefore, unlike a
disable condition, an abort condition is not sensitive to glitches.
￿ If the sampled value of an abort condition is 1'b1 in any time step in which an
evaluation is sensitive to it, then the evaluation of the underlying operand property
is aborted. This rule applies even in the same time step that the underlying
property evaluation would complete.
￿ An abort is a property, so the result of an evaluation is either pass or fail. An
aborted evaluation results in pass for the “accept” operators and fail for the
“reject” operators. This result applies only to the abort property itself. If the
abort property is a subproperty, then this result must be combined with the results
of other subevaluations in the usual ways to determine the overall result of the
concurrent assertion evaluation.
￿ Abort operators may be nested arbitrarily.
￿ There are no default abort conditions.

13.1.2.1 Asynchronous Aborts

Figure 13.4 shows a simple concurrent assertion with an asynchronous abort. It is
similar to the assertion a_disable of Fig. 13.1 , but its abort condition is retry .
The underlying property is a |=> b , and the entire concurrent assertion is clocked
by posedge clk . At each occurrence of this clocking event, evaluation of the abort