Formal equivalence checking process is a part of Electronic Design Automation, commonly used during the development of digital integrated circuits, to formally prove that two representations of a circuit design exhibit exactly the same behavior. Electronic design automation (EDA) is the category of tools for designing and producing electronic systems ranging from printed circuit boards (PCBs) to integrated circuits. ... Digital circuits are electric circuits based on a number of discrete voltage levels. ... Integrated circuit showing memory blocks, logic and input/output pads around the periphery A monolithic integrated circuit (also known as IC, microchip, silicon chip, computer chip or chip) is a miniaturized electronic circuit (consisting mainly of semiconductor devices, as well as passive components) which has been manufactured in the surface... Usually considered in the context of the applied arts, engineering, architecture, and other such creative endeavours, design is used as both a noun and a verb. ...

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. It has been suggested that this article or section be merged into Abstraction layer. ...

• 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.

A synchronous circuit is a circuit in which the parts are synchronized by means of a clock subcircuit. ... Microprocessors, including an Intel 80486DX2 and an Intel 80386. ... An instruction set, or instruction set architecture (ISA), describes the aspects of a computer architecture visible to a programmer, including the native datatypes, instructions, registers, addressing modes, memory architecture, interrupt and exception handling, and external I/O (if any). ... Register transfer level description (RTL), also called register transfer logic is a description of a digital electronic circuit in terms of data flow between registers, which store information between clock cycles in a digital circuit. ... // Description SystemC is a often thought of as a hardware description language like VHDL and Verilog, but is more aptly described as a system description language, since it exhibits its real power at the behaviour level of modelling. ...

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 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. Equivalence is not to be confused with functional correctness, which must be determined by functional verification. Register transfer level description (RTL), also called register transfer logic is a description of a digital electronic circuit in terms of data flow between registers, which store information between clock cycles in a digital circuit. ... In electronics, a hardware description language or HDL is any language from a class of computer languages for formal description of electronic circuits. ... Verilog is a hardware description language (HDL) used to model electronic systems. ... VHDL or VHSIC Hardware Description Language, is commonly used as a design-entry language for FPGAs and ASICs in electronic design automation of digital circuits. ... In synchronous digital electronics, such as most computers, a clock signal is a signal used to coordinate the actions of two or more circuits. ... Hardware is the general term that is used to describe physical artifacts of a technology. ... The word netlist can be used in several different domains, but perhaps the most popular is in the electronic design domain. ... Logic synthesis is a process by which an abstract form of desired circuit behavior (typically register transfer level (RTL) or behavioral) is turned into a design implementation in terms of logic gates. ... Functional verification, in electronic design automation, is the task of verifying that the logic design conforms to specification. ...

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. The word netlist can be used in several different domains, but perhaps the most popular is in the electronic design domain. ... Design-for-Test Design for Test (also known as Design for Testability, or DFT for short) is a methodology commonly employed during the design of integrated circuits. ... Integrated circuit layout, also known IC layout or IC mask layout is the representation of an integrated circuit in terms of planar geometric shapes that correspond to shapes actually drawn on photomasks used in semiconductor device fabrication. ... In electronics, tape-out is the name of the final stage of the design of an integrated circuit such as a microprocessor; the point at which the description of a circuit is sent for manufacture. ... EDA can mean: electronic design automation in arms trade it means excess defense articles in statistics it means exploratory data analysis in computer science it means event-driven architecture in computer science it means enterprise-driven architecture in European Union politics it means European Defence Agency Eating Disorders Association Estimation...

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 exponentionally. Logic simulation is the use of a computer program to simulate the operation of a digital circuit. ... In mathematics, exponentiation is a process generalized from repeated multiplication, in much the same way that multiplication is a process generalized from repeated addition. ...

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. In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. ...

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.

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.

A binary decision diagram (BDD) is a data structure that is used to represent a Boolean function. ... The Boolean satisfiability problem (SAT) is a decision problem considered in complexity theory. ...

Commercial softwares for equivalency checking

Major products in the LEC area of EDA are:

• Conformal by Cadence
• Formality by Synopsys

Look up Cadence in Wiktionary, the free dictionary Cadence has the following meanings. ... Synopsys, Inc. ...

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.

References

• Electronic Design Automation For Integrated Circuits Handbook, by Lavagno, Martin, and Scheffer, ISBN 0849330963 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.

See also

Formal methods In computer science, formal methods refers to mathematically based techniques for the specification, development and verification of software and hardware systems (Foldoc:formalmethods). ...