is ur register mapping correct? Check ur mapping and see if any unmatched registers exists between golden and revised. If there are, then you need to map them before u proceed for verification. u should also mimic the same synthesis env in ur formal verification env. if u r driving some ports/pins/nets to constant, u should do the same in FV . also at what stage are u doing FV? if after scan insertion, u have to tie the Scan eenable and test mode to "0". IF you are doing re-timing, check if ur FV tool has the same...if you ahve design ware multipliers in the code, then any FV tool will flunk..as synopsys recommends it can be verified using simulation...Most FV tools have the options which when used will create the same synthesis env. recently I have seen couple of bugs/false failures with formality. so check another version or Verplex or Quartz formal from magma..