Formal equivalence checking

Last updated April 26, 2024

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.

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 designers use equivalence checking to compare the functions specified for the instruction set architecture (ISA) with a register transfer level (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 SystemC 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 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 similar elements that have a higher or lower drive strength and/or area) 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 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 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 assignment 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 Graphics
Questa SLEC by Mentor Graphics
Conformal by Cadence
Jasper by Cadence
Formality by Synopsys
VC Formal by Synopsys
360 EC by OneSpin Solutions
ATEC by ATEC

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.

Related Research Articles

VHDL is a hardware description language that can model the behavior and structure of digital systems at multiple levels of abstraction, ranging from the system level down to that of logic gates, for design entry, documentation, and verification purposes. The language was developed for the US military VHSIC program in the 1980s, and has been standardized by the Institute of Electrical and Electronics Engineers (IEEE) as IEEE Std 1076; the latest version of which is IEEE Std 1076-2019. To model analog and mixed-signal systems, an IEEE-standardized HDL based on VHDL called VHDL-AMS has been developed.

In computer engineering, a hardware description language (HDL) is a specialized computer language used to describe the structure and behavior of electronic circuits, most commonly to design ASICs and program FPGAs.

Electronic design automation (EDA), also referred to as electronic computer-aided design (ECAD), is a category of software tools for designing electronic systems such as integrated circuits and printed circuit boards. The tools work together in a design flow that chip designers use to design and analyze entire semiconductor chips. Since a modern semiconductor chip can have billions of components, EDA tools are essential for their design; this article in particular describes EDA specifically with respect to integrated circuits (ICs).

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

In digital circuit design, register-transfer level (RTL) is a design abstraction which models a synchronous digital circuit in terms of the flow of digital signals (data) between hardware registers, and the logical operations performed on those signals.

In computer engineering, logic synthesis is a process by which an abstract specification of desired circuit behavior, typically at register transfer level (RTL), is turned into a design implementation in terms of logic gates, typically by a computer program called a synthesis tool. Common examples of this process include synthesis of designs specified in hardware description languages, including VHDL and Verilog. Some synthesis tools generate bitstreams for programmable logic devices such as PALs or FPGAs, while others target the creation of ASICs. Logic synthesis is one step in circuit design in the electronic design automation, the others are place and route and verification and validation.

In electronic design, a semiconductor intellectual property core, IP core or IP block is a reusable unit of logic, cell, or integrated circuit layout design that is the intellectual property of one party. IP cores can be licensed to another party or owned and used by a single party. The term comes from the licensing of the patent or source code copyright that exists in the design. Designers of system on chip (SoC), application-specific integrated circuits (ASIC) and systems of field-programmable gate array (FPGA) logic can use IP cores as building blocks.

In semiconductor design, standard-cell methodology is a method of designing application-specific integrated circuits (ASICs) with mostly digital-logic features. Standard-cell methodology is an example of design abstraction, whereby a low-level very-large-scale integration (VLSI) layout is encapsulated into an abstract logic representation.

SystemVerilog, standardized as IEEE 1800, is a hardware description and hardware verification language used to model, design, simulate, test and implement electronic systems. SystemVerilog is based on Verilog and some extensions, and since 2008, Verilog is now part of the same IEEE standard. It is commonly used in the semiconductor and electronic design industry as an evolution of Verilog.

<span class="mw-page-title-main">Integrated circuit design</span> Engineering process for electronic hardware

Integrated circuit design, semiconductor design, chip design or IC design, is a sub-field of electronics engineering, encompassing the particular logic and circuit design techniques required to design integrated circuits, or ICs. ICs consist of miniaturized electronic components built into an electrical network on a monolithic semiconductor substrate by photolithography.

An EDA database is a database specialized for the purpose of electronic design automation. These application specific databases are required because general purpose databases have historically not provided enough performance for EDA applications.

Functional verification is the task of verifying that the logic design conforms to specification. Functional verification attempts to answer the question "Does this proposed design do what is intended?" This is complex and takes the majority of time and effort in most large electronic system design projects. Functional verification is a part of more encompassing design verification, which, besides functional verification, considers non-functional aspects like timing, layout and power.

Design Closure is a part of the digital electronic design automation workflow by which an integrated circuit design is modified from its initial description to meet a growing list of design constraints and objectives.

The Layout Versus Schematic (LVS) is the class of electronic design automation (EDA) verification software that determines whether a particular integrated circuit layout corresponds to the original schematic or circuit diagram of the design.

<span class="mw-page-title-main">And-inverter graph</span> Graph representing an implementation of the logical functionality of a network

An and-inverter graph (AIG) is a directed, acyclic graph that represents a structural implementation of the logical functionality of a circuit or network. An AIG consists of two-input nodes representing logical conjunction, terminal nodes labeled with variable names, and edges optionally containing markers indicating logical negation. This representation of a logic function is rarely structurally efficient for large circuits, but is an efficient representation for manipulation of boolean functions. Typically, the abstract graph is represented as a data structure in software.

An engineering change order (ECO), also called an engineering change notice (ECN), engineering change (EC), or engineering release notice(ERN), is an artifact used to implement changes to components or end products. The ECO is utilized to control and coordinate changes to product designs that evolve over time.

Logic optimization is a process of finding an equivalent representation of the specified logic circuit under one or more specified constraints. This process is a part of a logic synthesis applied in digital electronics and integrated circuit design.

<span class="mw-page-title-main">Physical design (electronics)</span>

In integrated circuit design, physical design is a step in the standard design cycle which follows after the circuit design. At this step, circuit representations of the components of the design are converted into geometric representations of shapes which, when manufactured in the corresponding layers of materials, will ensure the required functioning of the components. This geometric representation is called integrated circuit layout. This step is usually split into several sub-steps, which include both design and verification and validation of the layout.

High-level synthesis (HLS), sometimes referred to as C synthesis, electronic system-level (ESL) synthesis, algorithmic synthesis, or behavioral synthesis, is an automated design process that takes an abstract behavioral specification of a digital system and finds a register-transfer level structure that realizes the given behavior.

High-level verification (HLV), or electronic system-level (ESL) verification, is the task to verify ESL designs at high abstraction level, i.e., it is the task to verify a model that represents hardware above register-transfer level (RTL) abstract level. For high-level synthesis, HLV is to HLS as functional verification is to logic synthesis.

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.
Sequential equivalence checking for RTL models. Nikhil Sharma, Gagan Hasteer and Venkat Krishnaswamy. EE Times.

External links

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

v t e Digital electronics
Components	Transistor Resistor Inductor Capacitor Printed electronics Printed circuit board Electronic circuit Flip-flop Memory cell Combinational logic Sequential logic Logic gate Boolean circuit Integrated circuit (IC) Hybrid integrated circuit (HIC) Mixed-signal integrated circuit Three-dimensional integrated circuit (3D IC) Emitter-coupled logic (ECL) Erasable programmable logic device (EPLD) Macrocell array Programmable logic array (PLA) Programmable logic device (PLD) Programmable Array Logic (PAL) Generic Array Logic (GAL) Complex programmable logic device (CPLD) Field-programmable gate array (FPGA) Field-programmable object array (FPOA) Application-specific integrated circuit (ASIC) Tensor Processing Unit (TPU)
Theory	Digital signal Boolean algebra Logic synthesis Logic in computer science Computer architecture Digital signal Digital signal processing Circuit minimization Switching circuit theory Gate equivalent
Design	Logic synthesis Place and route Placement Routing Transaction-level modeling Register-transfer level Hardware description language High-level synthesis Formal equivalence checking Synchronous logic Asynchronous logic Finite-state machine Hierarchical state machine
Applications	Computer hardware Hardware acceleration Digital audio radio Digital photography Digital telephone Digital video cinematography television Electronic literature
Design issues	Metastability Runt pulse