3.5 Formal Verification

When synthesis is completed, designers will perform a formal verification on the synthesized netlist. This process compares the synthesized netlist and the RTL code to ensure that the synthesized circuit matches the RTL code, using equivalence checking techniques.

If a mismatch occurs during formal verification, the designer must look into the synthesis process as well as the RTL code to debug the source of the mismatch. The mismatch may be caused by nonsynthe-sizable verilog code in the design, or by errors introduced during the synthesis process. Figure 3.32 shows a flow used for formal verification.

Figure 3.32: Diagram showing flow for formal verification.

There are many formal verification tools used in the industry, including Incisive, Formality, and FormalPro.