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)

assertionitemdeclaration ::= 
propertydeclaration
...
propertydeclaration ::=
property propertyidentifier \[ ( \[ propertyportlist \] ) \] ;
{ assertionvariabledeclaration }
propertyspec \[ ; \]
endproperty \[ : propertyidentifier \]
propertyportlist ::=
propertyportitem {, propertyportitem}
propertyportitem ::=
{ attributeinstance } \[ local \[ propertylvarportdirection \] \] propertyformaltype
formalportidentifier {variabledimension} \[ = propertyactualarg \]
propertylvarportdirection ::= input
propertyformaltype ::=
sequenceformaltype
| property
propertyspec ::=
\[clockingevent \] \[ disable iff ( expressionordist ) \] propertyexpr
propertyexpr ::=
sequenceexpr
| strong ( sequenceexpr )
| weak ( sequenceexpr )
| ( propertyexpr )
| not propertyexpr
| propertyexpr or propertyexpr
| propertyexpr and propertyexpr
| sequenceexpr |-> propertyexpr
| sequenceexpr |=> propertyexpr
| if ( expressionordist ) propertyexpr \[ else propertyexpr \]
| case ( expressionordist ) propertycaseitem { propertycaseitem } endcase
| sequenceexpr #-# propertyexpr
| sequenceexpr #=# propertyexpr
| nexttime propertyexpr
| nexttime \[ constant expression \] propertyexpr
| snexttime propertyexpr
| snexttime \[ constantexpression \] propertyexpr
| always propertyexpr
| always \[ cycledelayconstrangeexpression \] propertyexpr
| salways \[ constantrange \] propertyexpr
| seventually propertyexpr
| eventually \[ constantrange \] propertyexpr
| seventually \[ cycledelayconstrangeexpression \] propertyexpr
| propertyexpr until propertyexpr
| propertyexpr suntil propertyexpr
| propertyexpr untilwith propertyexpr
| propertyexpr suntilwith propertyexpr
| propertyexpr implies propertyexpr
| propertyexpr iff propertyexpr
| accepton ( expressionordist ) propertyexpr
| rejecton ( expressionordist ) propertyexpr
| syncaccepton ( expressionordist ) propertyexpr
| syncrejecton ( expressionordist ) propertyexpr
| propertyinstance
| clockingevent propertyexpr
propertycaseitem::=
expressionordist { , expressionordist } : propertyexpr \[ ; \]
| default \[ : \] propertyexpr \[ ; \]
assertionvariabledeclaration ::=
vardatatype listofvariabledeclassignments ;
propertyinstance ::=
psorhierarchicalpropertyidentifier \[ ( \[ propertylistofarguments \] ) \]
propertylistofarguments ::=
\[propertyactualarg\] { , \[propertyactualarg\] } { , . identifier ( \[propertyactualarg\] ) }
| . identifier ( \[propertyactualarg\] ) { , . identifier ( \[propertyactualarg\] ) }
propertyactualarg ::=
propertyexpr
| sequenceactualarg

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

//declared myprop1
property myprop1;
  myseq |=> out1; 
endproperty: myprop1

//declared myprop2
property myprop2;
  seq2 |=> (out1 == in1);
endproperty : myprop2

//instantiated myprop1 and myprop2
property myproperty;
  @(posedge clk) disable iff (rst)
  if (flg==1’b1) myprop2
  else myprop1; 
endproperty : myproperty

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

assert property (@(posedge clk) myproperty);
assume property (@(posedge clk) myproperty);
cover  property (@(posedge clk) myproperty);
resrtict property (@(posedge clk) myproperty);

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, propexpr, eventexpression etc.

With typed arguments

A formal argument may be typed by specifying the type prior to the formalportidentifier 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 formalportidentifier 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

disable iff (expressionordist) propertyexpr

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.

property myprop1;
  seq1 |=> (out == in2);  
endproperty: myprop1

property prop;
  disable iff (!rstn)
  seq2 |=> myprop1;
endproperty: prop

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.

property myprop1;
  disable iff (!rstn)  //WRONG !!! 
  seq1 |=> (out == in2);  
endproperty: myprop1

property prop;
  disable iff (!rstn)
  seq2 |=> myprop1;
endproperty: prop

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