RTL vs. netlist verification failed using formality. I checked the report and netlist, RTL code. Some registers and logics gates are reduced because the register was always '0' or '1'. The reduction didn't affect the function.
How do I write the script to make Formality give a correct answer?
It is not clear from your description whether reference (Golden) or implementation (revised ) has the less number of registers. The reason those registers are optimized away is because of constant propagation . Most synthesis tool optimize the circuit away by propagating constants either at top level alone or hierarchically if enabled . But formal tools are not that agressive . Check ur formality userguide to turn on the constant propagation and/or options where u can force the tool to tie undriven logic to 0 or 1. Also make sure whatever your synthesis tool env is it matches with ur formal environment...check this link for quick formal verification debugging primer
you can use the options available in the synthesis tool to match those things.ask tool to write the SVF file while doing the synthesis such that you can read the same in the formality tool such that it can under stand those netlist changes very well.