How to do LEC in RTL vs gating-clock netlist(power compiler)

[hgby2209]

verplex lec

I am using verplex lec to do formal check.
I have gating-clock gate level netlist which synthesized by DC+power complier.
But the formal check in RTL vs gate netlist have unmatch points, and when I used non-gating-clock netlist, the formal check was passed.

Could anyone can tell me how to do LEC in RTL vs gating-clock netlist using verplex lec ??

 

[horzonbluz]

gated clock in lec

I have use Verplex to do LEC many times. I think you may have not set right for your netlist. Please check your setting, i think you can pass. Clock gating not affect the LEC.

 

[galant]

set flatten model verplex

Is it reasonal that the result is different between the dynamic gate-level simulation and the static formal check? In some degree, i think, the answer should be yes.

 

[hgby2209]

conformal lec clock_gating

I had found out the command to fix this problem.
It is "set flatten model -gated_clock".