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);
endproperty
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.
- A recursive property can not use a not operator.
- The operator disable iff can not be used in a
recursibe property.
- 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);
endproperty
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));
endproperty
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:
- A sequence used as a property itself must be non-degenerate.
- A sequence used as an antecedent in |-> type implication
must be non-degenerate.
- 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
|
