Formality RTL vs. netlist

[ywguo]

compile_seqmap_propagate_constants

Hi, Guys,

RTL vs. netlist verification failed using formality. I checked the report and netlist, RTL code. Some registers and logics gates are reduced because the register was always '0' or '1'. The reduction didn't affect the function.

How do I write the script to make Formality give a correct answer?


Thanks
Yawei

 

[kbulusu]

formality undriven

It is not clear from your description whether reference (Golden) or implementation (revised ) has the less number of registers. The reason those registers are optimized away is because of constant propagation . Most synthesis tool optimize the circuit away by propagating constants either at top level alone or hierarchically if enabled . But formal tools are not that agressive . Check ur formality userguide to turn on the constant propagation and/or options where u can force the tool to tie undriven logic to 0 or 1. Also make sure whatever your synthesis tool env is it matches with ur formal environment...check this link for quick formal verification debugging primer

https://www.srikiran.net/blog/2007/01/22/debugging-formal-verification-fv-problems-fv-primer/

 

[ywguo]

formality rtl

Hi, Kiran,

Yes, the implementation has less registers because some registers are always assigned a constant in the RTL code.

How do I set a contstant propagation?


Thanks
Yawei

 

[kbulusu]

formality user guide

Yawei ,

I'm sorry,I dont have the formality user guide, but it is should be relatively easy..ur user guide should help you with it...

 

[rsrinivas]

formality tool

set compile_seqmap_propagate_constants false

put this before u give tha analyze command in DC

good luck
srinivas

 

[rameshsuthapalli]

logicvision formal verification formality

Hi All,

you can use the options available in the synthesis tool to match those things.ask tool to write the SVF file while doing the synthesis such that you can read the same in the formality tool such that it can under stand those netlist changes very well.

BR,
ramesh.s

 

[sumit_techkgp]

formality constant propagation

save a .svn file and read it with formality. This will make this error to go.
sumit