Formal equivalence checking

Formal equivalence checking is a process, used commonly during the development of digital integrated circuits, to formally prove that two representations of a circuit design exhibit exactly the same behavior.

The register transfer level (RTL) behavior of a digital chip is usually described with a hardware description language, such as Verilog or VHDL. This description is the golden reference model that describes in detail which operations will be executed during which clock cycle and by which pieces of hardware. Once the register transfer description has been verified by the logic designers by simulations and other verification methods, the design is usually converted into a netlist by a logic synthesis tool. The initial netlist will usually undergo a number of transformations, like, optimization of parts of the netlist, addition of design for test (DFT) structures, etc., before it is used as the basis for the placement of the logic elements into a physical layout. Contemporary physical design software will occasionally also make small modifications (such as replacing logic elements with equivalent elements that have a higher or lower driving strength ) to the netlist. When, at the end of the day, a tape-out is made of a digital chip, a lot of different programs will have touched the netlist.

In theory, a logic synthesis tool guarantees that the first netlist is logically equivalent to the RTL source code. And all the programs later in the process that make changes to the netlist have to make sure that these changes are logically equivalent to a previous version.

In practice, programs have bugs and it would be a major bet to assume that all steps from RTL all the way to the final tape-out netlist have been performed without error. Also, in real life, it is not uncommon for designers to make manual changes to a netlist, thereby introducing a major additional error factor.

Instead of blindly assuming that no mistakes were made, a verification step is needed to check the logical equivalence of the final version of the netlist to the RTL source code (golden reference model).

In the past, the way to check the equivalence was to run the test cases that were developed for verifying the correctness of the RTL code on the netlist. This process is called gate-level simulation . However, the problem with this is that the quality of the check is only as good as the quality of the test cases. Also, gate-level simulations are notoriously slow to execute, which is a major problem as the size of digital designs continues to grow exponentionally.

An alternative way to solve this is to formally prove that the RTL code and the netlist synthesized from it are the same. This process is called formal equivalence checking and is a problem that is studied under the broader area of formal verification.

A formal equivalence check can be performed between any two representations of a design: RTL <> netlist, netlist <> netlist or RTL <> RTL, though the latter is relatively rare compared to the first two. Typically, a formal equivalence checking tool will also indicate with great precision at which point there exists a difference between two representations.