Tutorials

Learn More

A property is said to be recursive if its declaration has its own instantiation.

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

This property specifies that either req2 should be high or when en is high then property p1 should be true.

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.

Example with not operator

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

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

Example with ‘disable iff’ operator

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.

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

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

SystemVerilog Assertions