Continue to Site

Welcome to EDAboard.com

Welcome to our site! EDAboard.com is an international Electronics Discussion Forum focused on EDA software, circuits, schematics, books, theory, papers, asic, pld, 8051, DSP, Network, RF, Analog Design, PCB, Service Manuals... and a whole lot more! To participate you need to register. Registration is free. Click here to register now.

Register Log in

Formality RTL vs. netlist

Status
Not open for further replies.
Y

ywguo

Junior Member level 2
Joined
Jan 9, 2005
Messages
20
Helped
1
Reputation
2
Reaction score
0
Trophy points
1,281
Activity points
198
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
 

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/
 
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
 

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...
 

formality tool

set compile_seqmap_propagate_constants false

put this before u give tha analyze command in DC

good luck
srinivas
 
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
 

formality constant propagation

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

Status
Not open for further replies.

Similar threads

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Back
Top