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

a_disable: assert property (

1

disable iff (reset)

2

@( posedge clk) a |=> b

3

) else $error("FAIL");

4

Fig. 13.1 Simple concurrent assertion with a disable clause

condition is cumbersome, so SVA provides various reset constructs with which to
declare reset conditions and specify their scopes.
A reset is asynchronous if the associated reset condition is checked at every
time step during the evaluation of the underlying property. SVA provides three
asynchronous resets: disable iff , accept_on , and reject_on . A reset is syn-
chronous if the associated reset condition is governed by a clock and checked only
in time steps in which the clocking event occurs. SVA provides two synchronous
resets: sync_accept_on and sync_reject_on .Apartfrom disable iff ,allof
the resets are referred to collectively as abort operators.

13.1.1 Disable Clause

A disable clause is specified with the compound keyword disable iff . It defines
a top-level asynchronous reset condition that applies throughout the evaluation
of a concurrent assertion. The reset condition is called the disable condition of
the disable clause. With the exception of overriding an incoming default disable
condition (see below), all nesting of disable clauses is illegal.
The meaning of a disable clause is that the current ( not the sampled) value
of the disable condition is checked continuously throughout the evaluation of the
underlying property of the concurrent assertion. If the disable condition is true in
any time between the start of an evaluation attempt in the Observed region and the
end of the evaluation attempt then the evaluation attempt is disabled. The evaluation
of the property thus stops and neither passes nor fails. Instead, the overall result of
the evaluation is disabled . If the disable condition neither is nor becomes true during
the evaluation, then the evaluation either passes or fails according to the result of the
evaluation of the underlying property.
Figure 13.1 gives a simple example. A disable clause may be specified either
before or after an explicit clocking event control in a concurrent assertion, but it
must precede all other terms of the underlying property. In this example, the disable
condition is reset . The underlying property appears in Line 3 and is singly clocked
by posedge clk .
Figure 13.2 shows a possible waveform for a_disable . The attempt that begins
at time 20 is disabled by the transition to 1'b1 of reset at time 35. In the absence
of the disable clause, this attempt would have failed at time 40, but, because it is
preempted, no failure occurs and the failing action block in Line 4 does not execute.