dc_shell and formalpro

[billyc59]

hi,

I'm trying to put my synopsys design compiler generated netlists through formalpro for LEC, but the netlists infer an unknown module "atbl_3"

Firstly, what is it?
secondly, what is the corresponding library that it appeared in?
lastly, will this library be recognized by formalpro?


-thanks

 

[ljxpjpjljx]

you use which tool ?

 

[billyc59]

Synthesis tool: SYNOPSYS DESIGN COMPILER
Formal Verification tool: MENTOR GRAPHICS FORMALPRO

I am using the synthesis tool to generate gate level netlists.
I am using the formal verification too l to verify the netlists to the RTL design. My problem is cross-compatability as the netlists require a library that the formal verification tool cannot recognize.

 

[kornukhin]

DC uses some_synthesis_library.lib for synthesis.
FP uses some_synthesis_library.v for verification.

There is no problems with using DC's netlist with FP, as netlist written using standard.

If netlist contain unknown module "atbl_3" then:
- not all *.v files used by FP
- there are differences between *.lib and *.v

 

[billyc59]

Thanks for your help again!

I've decided to stop using design compiler at the moment as I was unable to find the correcy library files. I am currently trying to use Precision RTL with some success. I opened another thread detailing my other problem with Precision.