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