question about formal inconclusive

[jojo12520]

verification_set_undriven_signals

When I use synopsys's tool FORMALITY to do formal verification of a module's RTL2NL( the netlist is generated by DC's command "compile_ultra"),it have several aborted points, the reason is too complex to resolve. And it takes very long time to finish the verify. Is there any good resolution?

Thanks

 

[NITIN BHARDWAJ]

verification_verify_unread_compare_points true

Hi ,
Are you facing same problem even if reading SVF file from DC?

Regards;

 

[sunilbudumuru]

hdlin_warn_on_mismatch_message true

Hello Friends,

Even if we read the svf file there are chances of getting inconclusive results. I faced the same situation and got inconclusive results at some multipliers of the design.

Here my suggestion is, if u r having the DW components like Multipliers, check what king of multiplier(csa, csd, wallace etc.) ur synthesis tool has inferred during synthesis? Now guide ur formality tool with this information.

Here I am providing you the variables and the piece of my script developed for inconclusive results during formal verification.

#######################
set hdlin_ignore_translate true
set hdlin_ignore_dc_script true
set hdlin_warn_on_mismatch_message "FMR_ELAB-147"
set hdlin_error_on_mismatch_message false
set hdlin_ignore_parallel_case false
set hdlin_ignore_full_case false
set verification_set_undriven_signals 0
set verification_verify_unread_tech_cell_pins false
set verification_verify_unread_compare_points false
set verification_assume_reg_init liberal
set verification_use_partial_modeled_cells "true"
set verification_blackbox_match_mode "any"
set verification_auto_loop_break true
set verification_verify_unread_bbox_inputs "false"
set verification_verify_unread_compare_points "false"
set hdlin_dyn_array_bnd_check "none"
set verification_effort_level high
set verification_datapath_effort_level high
set svf_datapath true
set enable_multiplier_generation true
set hdlin_multiplier_architecture csa


set_svf ./icarus.svf
..
..
guide

### u will get "dwsvf***" during synthesis with "set_svf" command.

guide_architecture_db -file dwsvf_3726-0/dwarchs-0.db { gtech }
guide_architecture_db -file dwsvf_3694-0/dwarchs-0.db { gtech }
guide_multiplier -design math_pad \
-instance ref:/WORK/math_pad/mult_110 \
-arch csa

guide_multiplier -design math_pad -instance ref:/WORK/math_pad/mult_86 -arch csa
...
...
..
..

#### If u want to verify that particular module where u r getting the inconclusive results #####
set verification_failing_point_limit 30000
set_architecture ref:/WORK/math_pad/mult_110 csa
set_architecture ref:/WORK/math_pad/mult_86 csa
...
...
...

match -datapath
set verification_datapath_effort_level unlimited
...
...
...
#####################

Good luck and pls. update the results.

Sunil Budumuru

 

[jojo12520]

formality inconclusive

yes

 

[sunilbudumuru]

formality gtech multiplier

hi jojo12520,

is tht working?

 

[vid31]

Hi sunilbudumuru,

I was also getting the similar kind of problem for DW multipliers.
I used these variables and problem got solved.

set hdlin_ignore_parallel_case false
set hdlin_ignore_full_case false

My question is why we have to ignore these variables. Already DC has dumped the netlist based on verilog directive. So, don't we have to use the directive in FV also?


Please clarify the doubts?

Regards,
Vid31