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

17.1 Overview of Recursion

This section gives an intuitive overview of recursion based on examples.
A named property is recursive if its declaration instantiates itself. Figure 17.1
shows a simple example. The instance my_always(p) behaves equivalently to
always p . Whenever evaluation of my_always(p) begins, Line 2 causes alignment
with the incoming clock, followed by evaluation of p .Line 4 has a recursive instance
and causes evaluation of my_always(p) to begin again after advancing to the next
occurrence of the incoming clock. The use of nexttime [0] in Line 2 ensures that
the first evaluation of p begins after alignment with a tick of the incoming clock. 2
From the beginning of an evaluation of my_always(p) , property p is checked
starting at each tick of the incoming clock. Indeed, the following is an unrolling
of the instances of the recursive form:

nexttime [0] p
and nexttime [1] p
and nexttime [2] p
...
Checking this is exactly the same as checking always p . In particular, the recursion
need not end: on a trace with infinitely many ticks of the incoming clock, there are
infinitely many recursive evaluations.
Suppose now that we want to get the effect of always [low:high] p in a
situation where low and high are not constants. In such a case, always cannot
be used. Instead, we can use a recursive property and capture the values of the
expressions defining the range bounds into local variables when the property begins.
Figure 17.2 shows an encoding. The recursive property ranged_always_recur
is called from the wrapper property ranged_always , which passes its arguments
through and passes 0 as actual argument to cnt . The wrapper is not necessary, but it
hides cnt , simplifying instantiation and usage. In the recursive property, low , high ,
and cnt are argument local variables. As a result, the values of the actual arguments
passed to low and high are captured when evaluation of the wrapper begins. If low
and high were not local variables, then changes to their actual arguments would

property my_always( property p);

1

( nexttime [0] p)

2

and

3

nexttime my_always(p);

4

endproperty

5

Fig. 17.1 Recursive encoding of always

2 Alignment with a tick of the incoming clock is necessary for equivalence of my_always(p)
and always p in case p has one or more leading clocks that differ from the incoming clock. See
Sect. 12.2.5.1 for more on nexttime [0] .