Gatecomp: Equivalence Checking of Digital Circuits in an Industrial Environment

This paper outlines formal verification in general and then introduces CVE's equivalence checking tool gatecomp, an equivalence checker developed in the formal verification group at Infineon, Germany. The basic verification tasks are described and the advanced features of the tool are discussed. The application of gatecomp to large industrial examples is reported. This demonstrates the power of the tool for various verification tasks, like netlist vs netlist comparison, RTL vs. netlist comparison or RTL vs. RTL comparison.