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

Having seen how recursion can get out of hand when Restriction 4 is violated, let
us consider the intuition for why it does not when at least one of the three conditions
is satisfied by each actual argument expression in a recursive instance.
If the first condition is satisfied, then the actual argument e is itself a formal
argument of the declaration of p . In this situation, e is simply being passed into the
recursive instance of q , modified at most by being cast to the type of the associated
formal argument of q . Iterated castings can involve some complexity, but it is benign
compared to expression explosion described above.
If the second condition is satisfied, then the actual argument e makes no reference
to any formal argument of p . As a result, e is composed of references to local
variables of p and references to entities outside of the declaration of p . Those entities
could be static variables, named sequences or properties, functions, etc. In any case,
whatever the local variables or external entities are, the meanings of references
to them are the same every time the recursive instance of q is encountered. Of
course the value stored in a local variable or an external static variable, e.g., may be
different, but the way in which these terms are combined to form e is not changing.
There is, thus, no expression explosion associated with e .
Finally, if the third condition is satisfied, then the formal argument to which
e is passed is an argument local variable. Argument local variables do not have
the expression explosion problem because they behave like value arguments, not
reference arguments. At each recursive instance, the value of the actual argument
expression is computed and stored in the corresponding argument local variable,
after which the form of the actual argument can be forgotten.

Exercises

17.1. The following is a variant of the encoding of ranged always from Fig. 17.2 :

property ranged_always( int unsigned low, high, property p);

1

ranged_always_recur(low, high, 0, p);

2

endproperty

3

property ranged_always_recur(

4

int unsigned low, high,

5

local input int unsigned cnt,

6

property p

7

);

8

if (cnt <= high)

9

(

10

( if (cnt >= low) p)

11

and

12

nexttime ranged_always_recur(low, high, cnt+1, p)

13

);

14

endproperty

15

In this encoding, the arguments low and high of the recursive property are not local
variables. How does this difference affect the meaning of the property?