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

Chapter 17
Recursive Properties
There is repetition everywhere, and nothing is found only once
in the world.
— Johann Wolfgang von Goethe
SystemVerilog allows named properties to be recursive. A named property is
recursive if its declaration instantiates itself. More generally, a set of named
properties may be mutually recursive , which means that there is a cyclic dependency
in the way that they instantiate themselves and one another. Recursion provides a
very flexible framework for coding properties. In general, from a flow diagram for a
desired check an encoding can be created in which certain nodes of the flow diagram
correspond to named properties. If the flow diagram contains cycles, then some of
the named properties will be recursive or mutually recursive. This situation occurs,
for example, if the check involves retry scenarios. Unlike recursion in programming
languages, property recursion does not return. It simply specifies that a thread of
evaluation should begin executing the named property again. As a result, there is no
stack associated with property recursion, and infinite property recursion is possible
on an infinite trace. As a theoretical matter, an instance of a recursive property can be
rewritten to avoid recursion. 1 However, for complex properties, it is often simpler
to write and maintain a recursive encoding, either because it is more succinct or
because the assertion writer can think about the properties in a more procedural
way.
1 An instance of a recursive property can be rendered as an alternating automaton. See [ 40 ]fora
sketch; restrictions on the actual arguments to recursive instances play a role. LTX augmented with
regular expressions is known to be as expressive as alternating automata (see [ 12 ], e.g.).