Formal Verification doubt

[spauls]

formal verification lec

Suppose you have a circuit as below.


-----Invertor------ (d) F/F (q) -------Invertor (IN RTL)

And in net list both invertors are washed away so LEC fails, but logic is same as both i/p and o/p are inverted.

How to overcome this in LEC, as LEC will surely fail at the primary input (i.e. d of F/F).

Please advice.

 

[nand_gates]

This can only be solved by LEC peoples!
Contact ur LEC technical support! He may help you!
They are having so many undocumented commands and variables!

 

[luancao]

Could you describe the case in detail?

I used LEC alot. It should be equal for A--INV--DFF--INV--B, and A--DFF--B. LEC check what is called key points. ie prime input, prime output, latch, register, hardblock.

So in your case, it will definitely pass. Didyou compare the RTL and GTL? Just try a simple case of IN---DFF---OUT in RTL. You will get IN--DFF--BUF--OUT by add setting BUF the driving cell. If it could not pass. Check your LEC script. In fact, you could just use the sample script from LEC and change the RTL list and GTL file name. And set the hard block list in the script. It will work.

 

[spauls]

Hi ,
My problem is solved, it is regarding register retiming issue.