Let, Sequence and Property Declarations; Inference - SVA: The Power of Assertions in SystemVerilog - page 176

After clock inference, substitutions, and clock resolution are completed, this
combination of properties and their instances results in the following assertion:

a_imply: assert property (
disable iff (!reset)
@( posedge clock) !d ##1 d |-> a |-> b until c);

t

The lack of specified actual argument for clk in the instance of p1 causes to infer
the actual from default clocking declarations. Since p1 is the top-level property
in the assertion, the disable iff specification is legal.
If, on the other hand, disable iff were included in p2 as shown in the next
example, the resulting property expression in the assertion would become illegal.
This is because disable iff would not apply to the top-level property.

Example 8.14.
module m;
bit clock, reset, a, b, c, d;
default clocking @( posedge clock); endclocking
...
property p1( event clk = $inferred_clock, bit x, property p);
@clk !x ##1 x |-> p;
endproperty
property p2;
disable iff (reset) a |-> (b until c);
endproperty
a_illegal: assert property (p1(.x(d), .p(p2)));
...
endmodule
After substitutions are carried out, the result is the following illegal assertion
because disable iff is not applied to the top-level property expression (see
Sect. 4.4.4 ):

a_illegal: assert property (@( posedge clk) !d ##1 d |->
disable iff (!reset) (a |-> (b until c)) );

t

Placing disable iff specifications into property definitions must be planned
carefully, otherwise it can lead to unexpected compilation errors.

Like let definition, sequence and property definitions may be placed in
packages for later reuse. In that case, particularly the use of disable iff into such
reusable properties must be done with even greater care.
In the next sections, we examine the inference of disable iff expression and
of clocking event.