formality and SVF rejected problem

[toobad365]

formality failing points

Hi All,
1. RTL vs Netlist comparation with Formality. I read SVF file successfully, but some svf operations rejected. Is verification OK for formality ?

2. There are some failing point when i do verification with formality. I analyze one of the failing point, and formality reports the failing point exists because of the rejected svf operation and recommend to do reg_merging. When I open scahematics logic cone, DFF is very strange ( D showed with simulation value 1, and Q showed with simulation value 0) .
Is something wrong with formality modeling the DFF and this datapath?
confused....

 

[raju3295]

failling point formality

there could be problem with svf creation, try to do one more time compile, and turn off the svf before quiting the dc shell and do the lec check with new svf,
generally formality should't reject the svf.