SystemVerilog Assertion
Part 4: Property Layer
Prev: Local Variables in a Sequence |
Next: More Property Types
In Part 1, Part 2 and
Part 3, we saw how boolean and sequence layers
build the foundation for describing a SystemVerilog assertion. Built on
this foundation, the property layer, the next layer in the
hierarchy, describes the behavior of a design. Property layer delivers
a clear and concise way to express this behavior using property,
the main construct of this layer.
A property describes the behavior of a design using a property-endproperty
keyword pair.
property property_name (list_of_optional_args);
assertion_variable_declaration;
property_specification;
endproperty
A property declaration can occur in any of the following scope:
- A module
- An interface,
- A program,
- A clocking block,
- A package,
- A compilation unit.
By itself, a property declaration does not affect a simulation
behavior until the property is designated as one of the following:
- An assumed or anticipated behavior: By associating
the property using an assume keyword. The verification
environment assumes that the behavior occurs.
- A checker: By associating the property using an
assert keyword. The verification environment checks if
the behavior occurs.
- A coverage specification: By associating the property
using a cover keyword. The verification environment uses
the statement for measuring coverage.
We will learn more about the keywords assume, assert
and cover in a later part of this series.
Seven Types of Properties
A property can be expressed in seven different basic forms. These
forms are described below. A property can combine two or more of
these basic forms to describe a design behavior.
Property Type 1: A Sequence
A property expression may be a simple sequence expression as shown
below.
property sequence_example;
s1; // s1 is a sequence defined elsewhere
endproperty
A sequence as a property expression is valid if the sequence is not
an empty match (i.e., it contains a specific non-empty expression to
match).
Property Type 2: Another Property
An instance of a named property can be used as a valid property
expression. For instance, the property sequence_example
defined above is itself can be a property expression.
property property_example;
sequence_example;
endproperty
It is important to note that a property may call itself resulting
in a recursive property.
Property Type 3: An Inverse
A property expression may be an inverse of another property
expression. The inversion is done by using the not
operator. The not operator works on any of the seven
types of property expression. The example of a sequence
property expression is shown below in such a case.
property inversion_example;
not (sequence_example);
endproperty
Property Type 4: A Disjunction
A disjunction property is true if either of its constituent
property expressions is true. The disjunction operator
or is used to describe a disjunction operator.
property disjunction_example;
sequence_example or inversion_example;
endproperty
(Note that, in this particular case, the property
disjuction_example will always be true.)
Prev: Local Variables in a Sequence |
Next: More Property Types
|
