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.
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.
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.
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 .