Tutorials

Protocols

Learn More

A recursive property refers to itself. It can repeat the same check on later clocks until a stopping condition is reached.

Simply, a property is said to be recursive if its declaration has its own instantiation.

What Makes a Property Recursive?

A property becomes recursive when its declaration contains an instance of the same property. The self-reference must move forward in time so that every recursive step is evaluated on a later clock.

property p1(req);
  req2 or (en |-> ##1 p1(req));
endproperty

This property has a stopping condition and a recursive step. req2 is the stopping condition. When recursion is needed, ##1 p1 evaluates the same property one clock later.

Note:

  1. The recursive property must include some time interval otherwise, the simulation will get stuck in an infinite recursion loop.
  2. The ‘not’ and ‘disable iff’ operators can not be used in a recursive property.

How the Recursive Property Works

What this example explains: the property continues to the next clock while req2 = 0 and en = 1.

If req2 = 1, the first side of or is true and the property succeeds on the current clock.

If req2 = 0 and en = 1, the implication requires p1 again one clock later.

If req2 = 0 and en = 0, the implication is vacuously true, so the property succeeds without another recursive step.

For example, suppose req2 = 0 and en = 1 at cycles 0 and 1. The property moves from cycle 0 to cycle 1 and then to cycle 2. If req2 = 1 at cycle 2, the recursion stops successfully there.

Why a Time Delay Is Required

A recursive call must include a time interval such as ##1. Without a delay, p1 would call itself again on the same clock, and the evaluation would never reach a later sampling point.

property illegal_no_delay;
  req2 or (en |-> illegal_no_delay);
endproperty

The recursive form should advance time before calling itself. In p1, the ##1 delay provides that required progress.

Restrictions on Recursive Properties

Using 'not' with a recursive property

A recursive property cannot be used under the not operator.

property p1(req);
  req2 or (en |-> ##1 p1(req));
endproperty

property illegal_prop1(req);
  not p1(req); // Illegal usage
endproperty

Using disable iff inside a recursive property

A disable iff condition cannot be placed inside the declaration that recursively calls itself.

property illegal_prop2(req);
  disable iff(dis)   // Illegal usage
  req2 or (en |-> ##1 illegal_prop2(req));
endproperty

Instead of using disable iff operator within a recursive property, it can be instantiated in another property and it is legal to use.

Legal reset wrapper

To disable the check during reset, instantiate the recursive property inside a separate non-recursive property and place disable iff on the wrapper.

property p1(req);
  req2 or (en |-> ##1 p1(req));
endproperty

property illegal_prop1(req);
  disable iff(dis) p1(req); // Legal usage
endproperty

p1 remains the recursive property, while p1_with_disable controls when that property is disabled.

Points to Remember

  1. A recursive property contains an instance of itself.
  2. The recursive call must move to a later clock, commonly with ##1.
  3. Define a clear condition that stops the recursive calls.
  4. Do not negate a recursive property with not.
  5. Apply disable iff through a separate wrapper property.

SystemVerilog Assertions