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

Formal Property Verification

This tickle file gives the steps to be followed while running FPV using Jasper tool

clear -all
set RTL_PATH /user/...
set BIND_PATH /user/...

set_property_compile_time_limit 15s
set_prove_time_limit 120h
set_proofgrid_pending_time_limit 102h

abvip -set_location /user/vtsw/Cadence/VIPP/VIPCAT11.30.043/tools.lnx86/abvip

check_cov -init -type coi -model {branch statement} -enable_proof_core -exclude_bind_hierarchies
check_superlint -lint

##hunt -config -strategy rahul -mode state_swarm -time_limit 2h

analyze +incdir+${RTL_PATH} \
             +define+ASSERT_ON \
             +define+RESTRICT_ON \
             +define+COVER_ON
             +define+COVER_GROUP_ON \
             -sv12 \
             ${RTL_PATH}/sub_module_1.v \
             ${RTL_PATH}/sub_module_2.v \
             ${RTL_PATH}/top_module.v \
             ${BIND_PATH}/const.v \
             ${BIND_PATH}/binding.v

set_capture_elaborated_design ON

config_rtlds -rule -disable -domain all
config_rtlds -rule -enable -tag {FSM_NO_TRRN FSM_NO_RCHB}

# Elaborate design and properties
elaborate -bbox_mul 128 \
                -bbox 1 \
                -bbox_a 100000 \
                -create_related_covers witness \
                -extract_covergroups \
                -top top_module


# Set up Clocks & Resets
clock clk
reset -expression ~n_reset

check_superlint -extract -task rahul_fsm_state

stopat -env {u_inst_name.sig_1}
stopat -env {u_inst_name.sig_2}

assume -env !signal
assume -disable <embedded>::top_module.u_sub_mod_1.u_sub_modul1_2.assume_grant
assume -from_assume <embedded>::top_module.u_sub_mod_1.u_sub_modul1_3.* -remove_original

assert {sig1 |=> u_sub_mod_1.u_sub_modul1_3.sig3};

# Checks whether assumption over-constrain the design
check_assumptions

set_proofgrid_mode shell
set_proofgrid_shell {/user/...../bsub -q jasper -K}
set_proofgrid_shell {/user/...../bsub -q jasper -K -n 8 - R span[hosts=1]}
set_proofgrid_per_engine_max_jobs 4

# Enable Functional coverage in DB
##check_cov -add_user_group *
check_cov -report -type {coi} -no_return -task {<embedded>} -exclude {reset waived}
prove -all -with_proven -bg
##check_cov -report -type {proof_core} -no_return -task {<embedded>} -exclude {reset waived}

##hunt -run -strategy rahul -max_jobs 2 -property <embedded>::property:1

# Report proof results
report

save -dir rahul_dir -elaborated_design rahul_file


******************************************************
To restore:
restore -db -dir rahul_dir -force
or
restore -elaborated_design rahul_file

$clog2 in Verilog

The $clog2 function returns the ceiling of the logarithm to the base 2.

Here is a sample Verilog code that depicts $clog2 function

function integer clog2;
input integer value;
begin
value = value-1;
for (clog2=0; value>0; clog2=clog2+1)
value = value>>1;
end
endfunction

module tb;
parameter A = $clog2(325);
parameter B = $clog2(64);
endmodule

The above piece of Verilog, it generates a value 9 for A.
The above piece of Verilog, it generates a value 6 for B.