Formal equivalence checking
Encyclopedia
Formal equivalence checking process is a part of electronic design automation
(EDA), commonly used during the development of digital
integrated circuit
s, to formally prove that two representations of a circuit design
exhibit exactly the same behavior.
(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 common for designers to make manual changes to a netlist, commonly known as Engineering Change Order
s, 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 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.
Electronic design automation
Electronic design automation is a category of software tools for designing electronic systems such as printed circuit boards and integrated circuits...
(EDA), commonly used during the development of digital
Digital circuit
Digital electronics represent signals by discrete bands of analog levels, rather than by a continuous range. All levels within a band represent the same signal state...
integrated circuit
Integrated circuit
An integrated circuit or monolithic integrated circuit is an electronic circuit manufactured by the patterned diffusion of trace elements into the surface of a thin substrate of semiconductor material...
s, to formally prove that two representations of a circuit design
Design
Design as a noun informally refers to a plan or convention for the construction of an object or a system while “to design” refers to making this plan...
exhibit exactly the same behavior.
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 designSynchronous circuitA synchronous circuit is a digital circuit in which the parts are synchronized by a clock signal.In an ideal synchronous circuit, every change in the logical levels of its storage components is simultaneous. These transitions follow the level change of a special signal called the clock...
specifications functionally equivalent if, clock by clock, they produce exactly the same sequence of output signals for any valid sequence of input signals. - MicroprocessorMicroprocessorA microprocessor incorporates the functions of a computer's central processing unit on a single integrated circuit, or at most a few integrated circuits. It is a multipurpose, programmable device that accepts digital data as input, processes it according to instructions stored in its memory, and...
designers use equivalence checking to compare the functions specified for the instruction setInstruction setAn instruction set, or instruction set architecture , is the part of the computer architecture related to programming, including the native data types, instructions, registers, addressing modes, memory architecture, interrupt and exception handling, and external I/O...
architecture (ISA) with a register transfer levelRegister transfer levelIn integrated circuit design, register-transfer level is a level of abstraction used in describing the operation of a synchronous digital circuit...
(RTL) 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 SystemCSystemCSystemC is a set of C++ classes and macros which provide an event-driven simulation kernel in C++ . These facilities enable a designer to simulate concurrent processes, each described using plain C++ syntax...
and its corresponding RTL specification. Such a check is becoming of increasing interest in a system- on-a-chip (SoC) design environment.
Synchronous machine equivalence
The register transfer levelRegister transfer level
In integrated circuit design, register-transfer level is a level of abstraction used in describing the operation of a synchronous digital circuit...
(RTL) behavior of a digital chip is usually described with a hardware description language
Hardware description language
In electronics, a hardware description language or HDL is any language from a class of computer languages, specification languages, or modeling languages for formal description and design of electronic circuits, and most-commonly, digital logic...
, such as Verilog
Verilog
In the semiconductor and electronic design industry, Verilog is a hardware description language used to model electronic systems. Verilog HDL, not to be confused with VHDL , is most commonly used in the design, verification, and implementation of digital logic chips at the register-transfer level...
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
Hardware
Hardware is a general term for equipment such as keys, locks, hinges, latches, handles, wire, chains, plumbing supplies, tools, utensils, cutlery and machine parts. Household hardware is typically sold in hardware stores....
. Once the logic designers, by simulations and other verification methods, have verified register transfer description, the design is usually converted into a netlist
Netlist
The word netlist can be used in several different contexts, but perhaps the most popular is in the field of electronic design. In this context, a "netlist" describes the connectivity of an electronic design....
by a logic synthesis
Logic synthesis
In electronics, logic synthesis is a process by which an abstract form of desired circuit behavior, typically register transfer level , is turned into a design implementation in terms of logic gates. Common examples of this process include synthesis of HDLs, including VHDL and Verilog...
tool. Equivalence is not to be confused with functional correctness, which must be determined by functional verification
Functional verification
Functional verification, in electronic design automation, is the task of verifying that the logic design conforms to specification. In everyday terms, functional verification attempts to answer the question "Does this proposed design do what is intended?" This is a complex task, and takes the...
.
The initial netlist
Netlist
The word netlist can be used in several different contexts, but perhaps the most popular is in the field of electronic design. In this context, a "netlist" describes the connectivity of an electronic design....
will usually undergo a number of transformations such as optimization, addition of Design For Test
Design For Test
Design for Test is a name for design techniques that add certain testability features to a microelectronic hardware product design. The premise of the added features is that they make it easier to develop and apply manufacturing tests for the designed hardware...
(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
Tape-out
In electronics design, tape-out or tapeout is the final result of the design cycle for integrated circuits or printed circuit boards, the point at which the artwork for the photomask of a circuit is sent for manufacture....
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
Logical equivalence
In logic, statements p and q are logically equivalent if they have the same logical content.Syntactically, p and q are equivalent if each can be proved from the other...
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 common for designers to make manual changes to a netlist, commonly known as Engineering Change Order
Engineering Change Order
Engineering Change Orders are used for changes in components, assemblies, or documents such as processes and work instructions. They may also be used for changes in specifications....
s, 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
Logic simulation
Logic simulation is the use of a computer program to simulate the operation of a digital circuit. Logic simulation is the primary tool used for verifying the logical correctness of a hardware design. In many cases logic simulation is the first activity performed in the process of taking a hardware...
. 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
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
.
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 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.
Methods
There are two basic technologies used for boolean reasoning in equivalence checking programs:- Binary decision diagramBinary decision diagramIn the field of computer science, a binary decision diagram or branching program, like a negation normal form or a propositional directed acyclic graph , is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed...
s, 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: SATBoolean satisfiability problemIn computer science, satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE...
solvers returns an assignment to the variables of a propositional formulaPropositional formulaIn propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value...
that satisfies it if such an assignments exists. Almost any boolean reasoning problem can be expressed as a SAT problem.
Commercial applications for equivalence checking
Major products in the Logic Equivalence Checking (LEC) area of EDA are:- FormalPro by Mentor GraphicsMentor GraphicsMentor Graphics, Inc is a US-based multinational corporation dealing in electronic design automation for electrical engineering and electronics, as of 2004, ranked third in the EDA industry it helped create...
- Conformal by CadenceCadence Design SystemsCadence Design Systems, Inc is an electronic design automation software and engineering services company, founded in 1988 by the merger of SDA Systems and ECAD, Inc...
- Formality by SynopsysSynopsysSynopsys, Inc. is one of the largest companies in the Electronic Design Automation industry. Synopsys' first and best-known product is Design Compiler, a logic-synthesis tool. Synopsys offers a wide range of other products used in the design of an application-specific integrated circuit...
- SLEC by Calypto
- Quartz Formal by Magma Design AutomationMagma Design AutomationMagma Design Automation is a software company in the electronic design automation industry. The company was founded in 1997 and maintains headquarters in San Jose, California, with facilities throughout North America, Europe, Japan, Asia and India....
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 its 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.
See also
- Formal methodsFormal methodsIn computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
- CADP - provides equivalence checking tools for asynchronous designs