Formality unmatched register

Hi all,
When I run formality between RTL and netlist after synthesis, there are some registers unmatched. Could anyone tell me some possible reasons?

Best Regards,
newcpu

perhaps your synthesis script allow DC eliminate some

unused registers, these registers has no relationship with

outputs.

best regards

newcpu said:

Hi all,
When I run formality between RTL and netlist after synthesis, there are some registers unmatched. Could anyone tell me some possible reasons?

Best Regards,
newcpu

Click to expand...

Hi,

The current generation of synthesis tool is very powerful; they can find FF that are redundant, and simplify the logic that lead to the removal of the FF. This is common in IP where the user do not use many of the modes.

Regards,
Eng Han

is there any book that focus on formality? I feel there are few material talk about formality debug practice.

just get funciton matched

Hi All,

The DesignCompiler from 2005.09 onwards giving a default file in work directory with name default.svf use that svf in the formality will resolve the above problem. the svf contains the guidense for the formality.

regards
Ramesh.s

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

agree with Ramesh.s.
the reasons of many problems can be found in .svf file .U can also observe the match results of FM and compare which parts r matched by name or signature analysis,and then go to find the reasons

During synthesis dc has removed those unused registers whatever has been written in RTL. Please save a .svf file during synthesis and read it out with formality. This problem will go away.
Sumit

i also want to know abt it