formal verification of Latch-based and DFF-based netlist

[archillios]

hi all,
I am using formality in equivalence checking,it's about gate-to-gate checking.
My ref design is a netlist in which sequential cells are usual DFF,while the implementation design netlist consist sequential cells all made of 2-level latch.

Matching is OK,but in verification phase,almost all sequential compare points failed.
When I debug the failure pattern ,I found that it seems the tools is trying to verify between DFF/Q (ref)and level one latch of 2-Level DFF (imp).

how can I get through this ?
thanks.

 

[eddsos]

Re: formal verification of Latch-based and DFF-based netli

There is a setup parameter, which could make the tools recoginize the situation automatically. I don't remember it now. you can see the reference manual.

 

[AlexWan]

Hi archillios,

Normally, formal tools will make the DFFs and black-box as the key points during the comparing. It will analyse the functonality of logic block between the key points. So if it can't find the according key point, it will not check the functionlity between the two designs.