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)

assertion_item_declaration ::= property_declaration ... property_declaration ::= property property_identifier [ ( [ property_port_list ] ) ] ; { assertion_variable_declaration } property_spec [ ; ] endproperty [ : property_identifier ] property_port_list ::= property_port_item {, property_port_item} property_port_item ::= { attribute_instance } [ local [ property_lvar_port_direction ] ] property_formal_type formal_port_identifier {variable_dimension} [ = property_actual_arg ] property_lvar_port_direction ::= input property_formal_type ::= sequence_formal_type | property property_spec ::= [clocking_event ] [ disable iff ( expression_or_dist ) ] property_expr property_expr ::= sequence_expr | strong ( sequence_expr ) | weak ( sequence_expr ) | ( property_expr ) | not property_expr | property_expr or property_expr | property_expr and property_expr | sequence_expr |-> property_expr | sequence_expr |=> property_expr | if ( expression_or_dist ) property_expr [ else property_expr ] | case ( expression_or_dist ) property_case_item { property_case_item } endcase | sequence_expr #-# property_expr | sequence_expr #=# property_expr | nexttime property_expr | nexttime [ constant _expression ] property_expr | s_nexttime property_expr | s_nexttime [ constant_expression ] property_expr | always property_expr | always [ cycle_delay_const_range_expression ] property_expr | s_always [ constant_range ] property_expr | s_eventually property_expr | eventually [ constant_range ] property_expr | s_eventually [ cycle_delay_const_range_expression ] property_expr | property_expr until property_expr | property_expr s_until property_expr | property_expr until_with property_expr | property_expr s_until_with property_expr | property_expr implies property_expr | property_expr iff property_expr | accept_on ( expression_or_dist ) property_expr | reject_on ( expression_or_dist ) property_expr | sync_accept_on ( expression_or_dist ) property_expr | sync_reject_on ( expression_or_dist ) property_expr | property_instance | clocking_event property_expr property_case_item::= expression_or_dist { , expression_or_dist } : property_expr [ ; ] | default [ : ] property_expr [ ; ] assertion_variable_declaration ::= var_data_type list_of_variable_decl_assignments ; property_instance ::= ps_or_hierarchical_property_identifier [ ( [ property_list_of_arguments ] ) ] property_list_of_arguments ::= [property_actual_arg] { , [property_actual_arg] } { , . identifier ( [property_actual_arg] ) } | . identifier ( [property_actual_arg] ) { , . identifier ( [property_actual_arg] ) } property_actual_arg ::= property_expr | sequence_actual_arg

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 my_prop1 property my_prop1; my_seq |=> out1; endproperty: my_prop1

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

//instantiated my_prop1 and my_prop2 property my_property; @(posedge clk) disable iff (rst) if (flg==1’b1) my_prop2 else my_prop1; endproperty : my_property

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

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

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

disable iff (expression_or_dist) property_expr

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 my_prop1; seq1 |=> (out == in2);
endproperty: my_prop1

property prop; disable iff (!rstn) seq2 |=> my_prop1; 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 my_prop1; disable iff (!rstn) //WRONG !!! seq1 |=> (out == in2);
endproperty: my_prop1

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

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