Formal Logic Equivalent Check (LEC)

Hi all,

When do Formal Equivalent Check (RTL and Gate Level) , I remember that the tool compare the comb logic between D-FF .

But when synthesis use re-timing and gated clock, can LEC tool compare RTL and Gate?

And is gated clock one form of re-timing?

I am reading a paper from SNUG about gated clock (How to successfully use gated clock...) but I cannot understand the waveform...

Best regards, Davy

Reply to
Davy
Loading thread data ...

Hi,

Davy schrieb:

LEC is the tool from Cadence(former Verplex). AFAIK is this tool able to handle retiming (or better: is able to support the user to handle retiming).

IMHO no. Gated clock is another problem for formal verification.

bye Thomas

Reply to
Thomas Stanka

Hi Davy, Yes, LEC can compare RTL and GLN with retiming. Command is analyze retiming... For gated clock, it is not part of retiming. LEC has limited default gated clock structure recognition but you still can use LEC to perform formal verification on GLN with your gated clock netlist.

Best regards, ABC

Davy wrote:

Reply to
ABC

ElectronDepot website is not affiliated with any of the manufacturers or service providers discussed here. All logos and trade names are the property of their respective owners.