Formal Logic Equivalent Check (LEC)

[Davy]

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

 

[Thomas Stanka]

Hi,

Davy schrieb:

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?

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

And is gated clock one form of re-timing?

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

bye Thomas

 

[ABC]

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:

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