Formal Equivalence Checking Development Service


Formal equivalence checking can consist of two phases as depicted below.






Phase 1 - Preparation for Equivalence Checking
The first phase is one of preparation that is best carried out in the project when synthesis is beginning to take place as a netlist will be required, and hopefully the RTL will be stabilizing.

The major netlist release stages in the customer's flow must be identified, and in some cases stages must be created. For example, hold fixes to a scan chain cannot be verified if a pre-hold fix netlist is not written to disk by the synthesis script. Verifying the post-hold fix netlist against RTL will not check the scan chain hold fixes, as the scan chains are not in the RTL.

Inputs for the preparation phase are the RTL for the whole chip (this does not need to be bug free) the first netlist from synthesis and the technology library verilog description. The RTL, netlist and technology library must be compiled into FormalPro libraries. Pads, RAMs, ROMs, analogue modules, etc must be identified and handled appropriately.

Name matching of targets (registers and ports) need rules developing for the synthesis names used in the netlist. The specification of the different modes of the chip need to be understood so that constraints can be applied correctly.

Note, Equivalence Checking can be performed on a sub-block of the chip if desired, e.g. if the integration is not yet complete, but module synthesis has been performed. Much of Phase 1 can be completed if only sub-blocks are available in fact, e.g. setting up the environment, technology library compilation and pipe-cleaning the synthesis and formal equivalence checking flow.

See Formal Equivalence Checking Example Flow here.




Phase 2 - Monitoring of Functional Equivalence
The second phase in one of monitoring the RTL and various stages of the netlist to ensure functional equivalence is maintained between the stages. The flow varies depending on the DFT insertion and layout flows of the customer. An example flow is given on the next page.

During development of a particular netlist (e.g. the STA fixing stage) only the previous stage of the equivalence checking flow needs to be carried out whenever the netlist is regenerated.

Whenever the netlist is completely regenerated from the RTL, or from any intermediate stage, a regression run of equivalence checking is required for each stage of the equivalence checking flow. Only by running each equivalence checking comparison will logic inserted at the stages of netlist development (e.g. DFT logic) be verified unchanged functionally by later modifications to the netlist (e.g. by STA fixing).

A final check of the released post-layout netlist should be performed against the RTL and against each of the major netlist stage releases.



Obtain a quotation here