Continue to Site

Welcome to EDAboard.com

Welcome to our site! EDAboard.com is an international Electronics Discussion Forum focused on EDA software, circuits, schematics, books, theory, papers, asic, pld, 8051, DSP, Network, RF, Analog Design, PCB, Service Manuals... and a whole lot more! To participate you need to register. Registration is free. Click here to register now.

Register Log in

problems of formal verification with conformal LEC(RTL VS resynthesis Netlist)

Status
Not open for further replies.
J

jayh

Newbie level 6
Newbie level 6
Joined
Dec 10, 2010
Messages
14
Helped
1
Reputation
2
Reaction score
1
Trophy points
1,283
Location
canada
Activity points
1,380
here is our flow
1. RTL
2. R2N netlist by synthesis(input: RTL/output: R2N)
3. a simple script to add some MUX on DFT clock path(input: R2N/output :R2N_DFT)
4. N2N netlist by resyntheis(input :R2N_DFT/output :N2N)

the problems is :
RTL LEC R2N: OK
RTL LEC R2N_DFT: OK
R2N_DFT LEC N2N : OK
RTL LEC N2N : NG
Test mode signal is kept inactive with LEC, so step 3 has no impact to logic(test path disabled) and just USER path verified.
i checked the umremap log, but it seems difficult to find hints

could anybody give me some hints or direction?

1 VS 2 OK and 2 VS 3 OK
can we judge 1 VS 3 OK?

thanks
 

Basically if 1==2 and 2==3 then 1==3 (if you use correct compare constraints).
Use GUI to locate and analyze mismatches.
During N2N synthesis you could make some optimization (ex. retiming) that needs additional constraints to LEC.
 
  • Like
Reactions: jayh

    J

    jayh

    Points: 2
    Helpful Answer Positive Rating
R u read in svf file when u execute "RTL LEC N2N" ?
 

svf……generated by DC for formality? i used RTL compiler and conformal LEC -_-
 

Status
Not open for further replies.

Similar threads

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Back
Top