Formal equivalence checking
From Wikipedia, the free encyclopedia
Formal equivalence checking process is a part of Electronic Design Automation (EDA), commonly used during the development of digital integrated circuits, to formally prove that two representations of a circuit design exhibit exactly the same behavior.
Contents |
[edit] Equivalence checking and levels of abstraction
In general, there is a wide range of possible definitions of functional equivalence covering comparisons between different levels of abstraction and varying granularity of timing details.
- The most common approach is to consider the problem of machine equivalence which defines two synchronous design specifications functionally equivalent if, clock by clock, they produce exactly the same sequence of output signals for any valid sequence of input signals.
- Microprocessor design uses equivalence checking to compare the functionally of the specification of the instruction set architecture (ISA) with the register transfer level implementation, ensuring that any program executed on both models will cause an identical update of the main memory content. This is a more general problem.
- A system design flow requires comparison between a transaction level model (TLM), e.g., written in SystemC and its corresponding RTL specification. Such a check is becoming of increasing interest in a system- on-a-chip (SoC) design environment.
[edit] Synchronous machine equivalence
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 logic designers, by simulations and other verification methods, have verified register transfer description, the design is usually converted into a netlist by a logic synthesis tool. Equivalence is not to be confused with functional correctness, which must be determined by functional verification.
The initial netlist will usually undergo a number of transformations such as optimization, 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 significant modifications (such as replacing logic elements with equivalent elements that have a higher or lower drive strength) to the netlist. Throughout every step of a very complex, multi-step procedure, the original functionality and the behavior described by the original code must be maintained. When the final tape-out is made of a digital chip, many different EDA programs and possibly some manual edits will have altered the netlist.
In theory, a logic synthesis tool guarantees that the first netlist is logically equivalent to the RTL source code. All the programs later in the process that make changes to the netlist also, in theory, ensure that these changes are logically equivalent to a previous version.
In practice, programs have bugs and it would be a major risk to assume that all steps from RTL through 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, commonly known as Engineering Change Orders, or ECOs, thereby introducing a major additional error factor. Therefore, 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 original description of the design ( golden reference model).
Historically, one way to check the equivalence was to re-simulate, using the final netlist, the test cases that were developed for verifying the correctness of the RTL. This process is called gate level logic 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 exponentially.
An alternative way to solve this is to formally prove that the RTL code and the netlist synthesized from it have exactly the same behavior in all (relevant) cases. 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.
[edit] Methods
There are two basic technologies used for boolean reasoning in equivalence checking programs:
- Binary decision diagrams, or BDDs: A specialized data structure designed to support reasoning about boolean functions. BDDs have become highly popular because of their efficiency and versatility.
- Conjunctive Normal Form Satisfiability: SAT solvers returns an assignment to the variables of a propositional formula that satisfies it if such an assignments exists. Almost any boolean reasoning problem can be expressed as a SAT problem.
[edit] Commercial applications for equivalence checking
Major products in the Logic Equivalence Checking (LEC) area of EDA are:
[edit] Generalizations
- Equivalence Checking of Retimed Circuits: Sometimes it is helpful to move logic from one side of a register to another, and this complicates the checking problem.
- Sequential Equivalence Checking: Sometimes, two machines are completely different at the combinational level, but should give the same outputs if given the same inputs. The classic example is two identical state machines with different encodings for the states. Since this cannot be reduced to a combinational problem, more general techniques are required.
- Equivalence of Software Programs, i.e. checking if two well-defined programs that take N inputs and produce M outputs are equivalent: Conceptually, you can turn software into a state machine (that's what the combination of a compiler does, since a computer plus it's memory form a very large state machine.) Then, in theory, various forms of property checking can ensure they produce the same output. This problem is even harder than sequential equivalence checking, since the outputs of the two programs may appear at different times, but it is possible and researchers are working on it.
[edit] References
- Electronic Design Automation For Integrated Circuits Handbook, by Lavagno, Martin, and Scheffer, ISBN 0-8493-3096-3 A survey of the field. This article was derived, with permission, from Volume 2, Chapter 4, Equivalence Checking, by Fabio Somenzi and Andreas Kuehlmann.
- R.E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers., C-35, pp. 677–691, 1986. The original reference on BDDs.
