Formality stops, never finish

[ywguo]

Hi,

I ran rtl vs. netlist formal verification using formality. It had never finished. It always stopped at status verifying. The design contains many multipliers and adders. I had even set some blocks as black box to reduce the complexity. It stopped at status verifying after more than 10 hours. It made me frustrated.

Any comments/advices are very appreciated.


Thanks
Yawei

 

[jkfoo]

try running a very stable version of Formality, 2004.06-SP3, to see if it's ok.

 

[zeese]

Check the timeout limit. Since you said, after 10 hours, it stopped, that means, your timeout limit is 10 hours. You can set it to any number of minutes/hours or even unlimited.
I can't remember what's the command. Check the solvnet or manual.

 

[stormwolf]

Check you constriant , major about you defined naming rule.

 

[newcpu]

You have mentioned many multipliers and adders. Have you used DC ultra for synthesis? If you used ultra feature, that means multipliers and adders might be divieded and re-combined. Then formality might stopped because some uncertain mismatches.

 

[stormwolf]

I have use comform before, if like what newcpu said, it need some new feature to do this , you can read you document about multiplies and adder compare use which feature .