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
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
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:
Have something to add? Share your thoughts — no account required.
Ask the community — no account required