SVA Properties I : Basics

Property defines set of behaviours of the design. To use those behaviors verification directive must be used. In other words, a property itself does not produce any result. A named property can be declared in module, interface, program, clocking block, package, compilation-unit scope, generate block or checker. In simulation run, property will be either in inactive state or in evaluation start point or in run state or in finished state.

Property construct syntax (LRM)

Property Reference

A property can be referenced/instantiated in verification directive statements like assert, assume, cover, or restrict statement or in a property as shown below.

eg: A property can be referenced in a property

eg: A property can be referenced in an assert, assume, cover, or restrict statement.

Properties can have formal arguments in order to make Properties reusable. These are typed or untyped. Formal arguments are optional and can have default values. A formal argument may be written in place of various syntactic entities, such as identifier, expression, prop_expr, event_expression etc.

With typed arguments

A formal argument may be typed by specifying the type prior to the formal_port_identifier of the formal argument.A type shall apply to all formal arguments whose identifiers both follow the type and precede the next type, if any, specified in the port list.

With untyped arguments

A formal argument is said to be untyped if there is no type specified prior to its formal_port_identifier in the port list. There is no default type for a formal argument.

The actual argument of an untyped formal argument can be anything so that its substitution results in a valid property. Declaring formal arguments and default actual arguments and instantiating named properties with actual arguments are the same as those for named sequences. Please refer SVA Sequence I : Basic for more information.

Property evaluation result

The result of a property evaluation can be any of the following.

  • Hold:
  • The evaluation of property is a success and tool will report pass/hold status

  • Fail:
  • The evaluation of property is a failure and tool will report fail status

  • Disable:
  • Property evaluation has been disabled by disabled iff construct. The tool will not report pass or fail

  • Kill
  • Property evaluation has been killed by $assertkill and the tool will not report pass or fail status.

Disable iff

The clause disable iff is used in a property, usually to asynchronously reset a property. The expression of the disable iff is called disable condition. If disable condition is TRUE, any active evaluation attempt is aborted immediately and will not start any other evaluation attempts until the expression is TRUE.

A disabled evaluation of a property does not result in success or failure. The disable condition must not contain any reference to local variables. When disable condition is FALSE, evaluation of the property will be resumed.

Nesting of disable iff clause explicitly or through property instantiation is not allowed. Do not use disable iff in a property which will be be instantiated in other properties.

More about properties can be found in other sections of “SVA Properties” series

Sini Balakrishnan

Sini Balakrishnan

Staff Engineer at Intel
Sini has spent more than a dozen years in the semiconductor industry, focusing mostly on verification. She is an expert on Formal Verification and has written international papers and articles on related topics.
Sini Balakrishnan

Latest posts by Sini Balakrishnan (see all)

Leave a Reply

Your email address will not be published. Required fields are marked *