Recursive Properties - SVA: The Power of Assertions in SystemVerilog - page 397

Creating a framework for recursion that interacts well with the strong operators
involves dealing with negation and liveness in recursive forms. Again, SVA
currently avoids these issues through Restriction 1 .

17.3.2 Disable Clause

RESTRICTION 2: disable iff cannot be used in the declaration of a
recursive property.

disable iff cannot be nested, so its use within a recursive property declaration
is forbidden. If a disable clause is needed, it should be put in a wrapper property
around the recursive property or in an assertion statement. For example, the
following is illegal:
property illegal_disable( logic b, property p);
disable iff (b)
p and nexttime illegal_disable(b, p);
endproperty
The effect of the disable can be obtained using a wrapper, as in
property always_with_disable( logic b, property p);
disable iff (b)
my_always(p);
endproperty
where my_always is the recursive property from Fig. 17.1 .

17.3.3 Time Advance

RESTRICTION 3: If p is a recursive property, then, in the declaration of p ,
every instance of p must occur after a positive advance in time. In the case of
mutually recursive properties, all recursive instances must occur after positive
advances in time.

Briefly, recursion must occur after a positive advance in time. This restriction
is intended to avoid recursive forms that get “stuck” at a single point in time. For
example, the following is illegal:
property illegal_stuck( property p);
p and nexttime [0] illegal_stuck(p);
endproperty