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:
  1. A module
  2. An interface,
  3. A program,
  4. A clocking block,
  5. A package,
  6. A compilation unit.

By itself, a property declaration does not affect a simulation behavior until the property is designated as one of the following:

  1. An assumed or anticipated behavior: By associating the property using an assume keyword. The verification environment assumes that the behavior occurs.
  2. A checker: By associating the property using an assert keyword. The verification environment checks if the behavior occurs.
  3. 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

Share/Save/Bookmark



Verification Management
Join Verification Management Group


Book of the Month


From Our Press