SVA Properties

`ifdef ASSERT_ON

 `ifdef UVM_DISPLAY_EN
   import uvm_pkg::*;
    `define PROJ_INFO_MSG(msg) \
             `uvm_info("DUT ASSERTION INFO:", $sformatf(msg))

    `define PROJ_FATAL_MSG(msg) \
             `uvm_error("DUT ASSERTION FATAL:", $sformatf(msg))

    `define PROJ_ERROR_MSG(msg) \
             `uvm_error("DUT ASSERTION ERROR:", $sformatf(msg))

 `else

  `define PROJ_INFO_MSG(msg) \
             $info("%s%0t%s%s","DUT ASSERTION INFO:", $time,"   ",msg)

  `define PROJ_FATAL_MSG(msg) \
             $fatal("%s%0t%s%s","DUT ASSERTION FATAL:", $time,"   ",msg)

  `define PROJ_ERROR_MSG(msg) \
             $fatal("%s%0t%s%s","DUT ASSERTION ERROR:", $time,"   ",msg)

 `endif

 `define PROJ_ASSERT_INFO(clk, disable_expr, test_expr, msg) \
             assert property (@(posedge clk) disable iff (disable_expr) test_expr) else `PROJ_INFO_MSG (msg);

 `define PROJ_ASSERT_FATAL(clk, disable_expr, test_expr, msg) \
             assert property (@(posedge clk) disable iff (disable_expr) test_expr) else `PROJ_FATAL_MSG (msg);

 `define PROJ_ASSERT_ERROR(clk, disable_expr, test_expr, msg) \
             assert property (@(posedge clk) disable iff (disable_expr) test_expr) else `PROJ_ERROR_MSG (msg);

 `define PROJ_ASSUME(clk, disable_expr, test_expr, msg) \
             assume property (@(posedge clk) disable iff (disable_expr) test_expr);

 `define PROJ_COVER(clk, disable_expr, test_expr, msg) \
             cover property (@(posedge clk) disable iff (disable_expr) test_expr);

`endif


SVA Property Syntax

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

Commonly used properties in design