SystemVerilog Assertion

Part 4: Property Layer

Prev: Implication Operators | Next: Associating sense

Recursive Property

We saw earlier that a property expression can be another property. But can it be the same property? Can a property call itself? The answer is indeed yes; a proerty can call itself. Such a property is known as a recursive property.

   property recursive_always;
      sig_x and (1'b1 |=> recursive_always);
In the above example, the property recursive_always describes a behavior in which sig_x is true for this clock cycle and the property is true in the next clock tick as well. In other words, sig_x must be true in all clock ticks.

Restrictions for Recursive Properties

There are several restrictions on the use of recursive properties. These are described below.

  1. A recursive property can not use a not operator.
  2. The operator disable iff can not be used in a recursibe property.
  3. A recursive property can call itself only after a positive time delay (to avoid an infinite loop). For instance, the following code is illegal even though it looks very similar to the one above. (Notice the use of '|->' in place of '|=>'.)
       property recursive_always;
          sig_x and (1'b1 |-> recursive_always);

Recursive Property with Formal Argument(s)

A recursive property with one or more formal argument works in a manner similar to one which does not have formal arguments. Here is an example:

   property recursive_always (s0);
      s0 and (1'b1 |=> recursive_always(s0));
In this case, s0 is passed as an argument enhancing the portability of the property. One important aspect to note here is that s0 is evaluated on each clock tick too when recursive_always is called.

Non-degeneracy: Restrictions on Sequences Used in Properties

A sequence that can not match or has empty match (such as, 1'b0[*0]) is called a degenerate sequence. Otherwise, it is called non-degenerate. A sequence used inside a property must obey the following restrictions:

  1. A sequence used as a property itself must be non-degenerate.
  2. A sequence used as an antecedent in |-> type implication must be non-degenerate.
  3. A sequence used as an antecedent in |=> type implication can have empty matches, but not zero matches.

With this, we wrap up our Part 4 of the discussion on SystemVerilog assertion. In the next and concluding part, we will look into the effect of multiple clocks in a property, and also the top most layer of SV assertion - the Assertion Directive Layer.

Prev: Implication Operators | Next: Associating sense


Verification Management
Join Verification Management Group

Shop Amazon - Contract Cell Phones & Service Plans

Book of the Month