Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 76

assertion main reset expression (the argument of disable iff statement) which
is never sampled as explained in detail in Sect. 13.1.1 . Sampling of variables is
explained in detail in Appendix A .

The value of the main assertion reset is not sampled in concurrent assertions.

4.4.4 Reset

Usually, we are interested in checking an assertion only when the reset signal
is inactive. disable iff operator is used to specify the reset expression of the
assertion. If the main assertion clock is explicitly specified, disable iff should
immediately follow it. If the assertion clock is omitted, disable iff should be the
first operator in the assertion body. There may be at most one disable iff operator
in the whole assertion.
If the disable condition is true between the start of an evaluation attempt in the
Observed region and the end of the evaluation attempt then the overall evaluation of
the property results in disabled. The evaluation attempt is discarded (neither success
nor failure). Such attempts are called disabled . The reset is asynchronous, in the
sense that it is monitored at every time step, and not only at the ticks of the assertion
clock. Therefore, it also makes it sensitive to 0-width simulation glitches. The
sensitivity can be removed by applying $sampled function to the disable expression
(or its component variables). This makes the disable condition insensitive to such
glitches like the body of the concurrent assertion.

Example 4.8. Consider assertion a1
a1: assert property (@( posedge clk) disable iff (rst)
req |-> nexttime [2] ack);
with the timing diagram shown in Fig. 4.11 .
In this example, there are three assertion evaluation attempts beginning at times
20, 40, and 70 that satisfy the antecedent signal req . 5 First two of them are disabled,
and therefore the assertion does not fail even though there is no ack received. The
last attempt is normal, and it succeeds because ack is received in two cycles after
req is issued. Refer to Chap. 13 for detailed discussion about assertion resets.

t

As we mentioned, the disable iff expression acts asynchronously. Its eva-
luation goes on evaluating regardless of the occurrence of the clock tick of the
associated assertion. And, should it evaluate to true, all evaluation attempts of that
assertion that are “in flight” are declared disabled.

5 One could be tempted to say that the attempts begin at times 15, 35, and 65, but recall that the
attempts are synchronized with the rising edge of the clock.