formal verification of Latch-based and DFF-based netlist

Status
Not open for further replies.
A

archillios

Full Member level 1
Joined
Jun 29, 2005
Messages
97
Helped
5
Reputation
10
Reaction score
1
Trophy points
1,288
Activity points
1,910
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.
 

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.
 

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.
 

Status
Not open for further replies.

Similar threads

Menu
Log in
Register
Cookies are required to use this site. You must accept them to continue using the site. Learn more…