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

of each concurrent assertion in which it appears, preceded only by local variable
declarations and leading clocking event controls. The following variant of the code
in Fig. 13.1 behaves equivalently:

property p_disable;

1

disable iff (reset) a |=> b;

2

endproperty

3

a_disable: assert property (

4

@( posedge clk) p_disable

5

) else $error("FAIL");

6

A disable clause may not be specified within the declaration of a named
sequence.

13.1.1.1 Default Disable Condition

Like a clocking event, a disable condition may be shared by many concurrent
assertions. In this situation, it is convenient to be able to specify a default disable
condition . A default disable condition applies throughout the generate block,
module, interface, or program in which it appears, including nested scopes except
those with their own default disable condition. The default applies to all concurrent
assertions within the scope that do not have disable conditions otherwise specified.
It does not apply to declarations of named sequences or properties. The following
example illustrates the syntax:

module m_default_disable( logic reset, a, b, clk);

1

default disable iff reset;

2

a_disable: assert property (

3

@( posedge clk) a |=> b

4

) else $error("FAIL");

5

a_override: assert property (

6

disable iff (1'b0)

7

@( posedge clk) reset |=> !reset

8

);

9

endmodule

10

The default disable condition, reset , applies to a_disable . Since a_override
has an explicit disable condition, the disable condition 1'b0 applies to it and
overrides the default.
Nesting of disable conditions is only allowed when the inner disable condition
overrides an incoming default disable condition. The overriding by the disable
clause in Line 7 above is a legal example. Figure 13.3 shows an illegal example.
Line 8 results in a nesting of disable conditions, the outer one from the concurrent
assertion a_disable in Line 4 and the inner one from the instantiated property
p_disable in Line 7 . The outer disable condition is not a default. Therefore, the
nesting is illegal, despite the fact that the two disable conditions are identical.
The disable condition can also be inferred from the instantiation context using
the system function $inferred_disable which can be used in place of a default