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

[jayh]

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

 

[kornukhin]

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.

 

[airqqy]

R u read in svf file when u execute "RTL LEC N2N" ?

 

[jayh]

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

 

[kornukhin]

Use 'write_do_lec' for RTL Compiler.

 

[jayh]

i'll have a try, thank you