And-inverter graph
   HOME

TheInfoList



OR:

An and-inverter graph (AIG) is a directed, acyclic
graph Graph may refer to: Mathematics *Graph (discrete mathematics), a structure made of vertices and edges **Graph theory, the study of such graphs and their properties *Graph (topology), a topological space resembling a graph in the sense of discre ...
that represents a structural implementation of the logical functionality of a circuit or network. An AIG consists of two-input nodes representing
logical conjunction In logic, mathematics and linguistics, And (\wedge) is the truth-functional operator of logical conjunction; the ''and'' of a set of operands is true if and only if ''all'' of its operands are true. The logical connective that represents thi ...
, 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 function In mathematics, a Boolean function is a function whose arguments and result assume values from a two-element set (usually , or ). Alternative names are switching function, used especially in older computer science literature, and truth function ...
s. Typically, the abstract graph is represented as a data structure in software. Conversion from the network of logic gates to AIGs is fast and scalable. It only requires that every gate be expressed in terms of
AND gate The AND gate is a basic digital logic gate that implements logical conjunction (∧) from mathematical logic AND gate behaves according to the truth table. A HIGH output (1) results only if all the inputs to the AND gate are HIGH (1). If not al ...
s and
inverters A power inverter, inverter or invertor is a power electronic device or circuitry that changes direct current (DC) to alternating current (AC). The resulting AC frequency obtained depends on the particular device employed. Inverters do the opp ...
. This conversion does not lead to unpredictable increase in memory use and runtime. This makes the AIG an efficient representation in comparison with either the
binary decision diagram In computer science, a binary decision diagram (BDD) or branching program is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed representation of sets or relations. ...
(BDD) or the "sum-of-product" (ΣoΠ) form, that is, the
canonical form In mathematics and computer science, a canonical, normal, or standard form of a mathematical object is a standard way of presenting that object as a mathematical expression. Often, it is one which provides the simplest representation of an ...
in
Boolean algebra In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variables are the truth values ''true'' and ''false'', usually denoted 1 and 0, whereas i ...
known as the
disjunctive normal form In boolean logic, a disjunctive normal form (DNF) is a canonical normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or (in philosophical logic) a ''cluster c ...
(DNF). The BDD and DNF may also be viewed as circuits, but they involve formal constraints that deprive them of scalability. For example, ΣoΠs are circuits with at most two levels while BDDs are canonical, that is, they require that input variables be evaluated in the same order on all paths. Circuits composed of simple gates, including AIGs, are an "ancient" research topic. The interest in AIGs started with Alan Turing's seminal 1948 paper on neural networks, in which he described a randomized trainable network of NAND gates. Interest continued through the late 1950s and continued in the 1970s when various local transformations have been developed. These transformations were implemented in several logic synthesis and verification systems, such as Darringer et al. and Smith et al., which reduce circuits to improve area and delay during synthesis, or to speed up
formal equivalence checking 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 b ...
. Several important techniques were discovered early at IBM, such as combining and reusing multi-input logic expressions and subexpressions, now known as structural hashing. Recently there has been a renewed interest in AIGs as a
functional representation Function Representation (FRep or F-Rep) is used in solid modeling, volume modeling and computer graphics. FRep was introduced in "Function representation in geometric modeling: concepts, implementation and applications" as a uniform representation ...
for a variety of tasks in synthesis and verification. That is because representations popular in the 1990s (such as BDDs) have reached their limits of scalability in many of their applications. Another important development was the recent emergence of much more efficient
boolean satisfiability In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
(SAT) solvers. When coupled with ''AIGs'' as the circuit representation, they lead to remarkable speedups in solving a wide variety of boolean problems. AIGs found successful use in diverse
EDA EDA or Eda may refer to: Computing * Electronic design automation * Enterprise Desktop Alliance, a computer technology consortium * Enterprise digital assistant * Estimation of distribution algorithm * Event-driven architecture * Exploratory ...
applications. A well-tuned combination of ''AIGs'' and
boolean satisfiability In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
made an impact on
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 met ...
, including both model checking and equivalence checking. Another recent work shows that efficient circuit compression techniques can be developed using AIGs. There is a growing understanding that logic and physical synthesis problems can be solved using simulation and
boolean satisfiability In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...
to compute functional properties (such as symmetries) and node flexibilities (such as
don't-care term In digital logic, a don't-care term (abbreviated DC, historically also known as ''redundancies'', ''irrelevancies'', ''optional entries'', ''invalid combinations'', ''vacuous combinations'', ''forbidden combinations'', ''unused states'' or ''l ...
s, resubstitutions, and SPFDs). Mishchenko et al. shows that AIGs are a promising ''unifying'' representation, which can bridge
logic synthesis 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 com ...
,
technology mapping Technology is the application of knowledge to reach practical goals in a specifiable and reproducible way. The word ''technology'' may also mean the product of such an endeavor. The use of technology is widely prevalent in medicine, science, ...
, physical synthesis, and formal verification. This is, to a large extent, due to the simple and uniform structure of AIGs, which allow rewriting, simulation, mapping, placement, and verification to share the same data structure. In addition to combinational logic, AIGs have also been applied to
sequential logic In automata theory, sequential logic is a type of logic circuit whose output depends on the present value of its input signals and on the sequence of past inputs, the input history. This is in contrast to ''combinational logic'', whose output i ...
and sequential transformations. Specifically, the method of structural hashing was extended to work for AIGs with memory elements (such as D-type flip-flops with an initial state, which, in general, can be unknown) resulting in a data structure that is specifically tailored for applications related to
retiming Retiming is the technique of moving the structural location of latches or registers in a digital circuit to improve its performance, area, and/or power characteristics in such a way that preserves its functional behavior at its outputs. Retiming ...
.{{cite conference, author1=J. Baumgartner , author2=A. Kuehlmann , title=Min-area retiming on flexible circuit structures, book-title= Proc. ICCAD'01, pages=176–182, date=2001, url=http://public.dhe.ibm.com/software/es/info/iwls01_ret.pdf Ongoing research includes implementing a modern logic synthesis system completely based on AIGs. The prototype calle
ABC
features an AIG package, several AIG-based synthesis and equivalence-checking techniques, as well as an experimental implementation of sequential synthesis. One such technique combines technology mapping and retiming in a single optimization step. These optimizations can be implemented using networks composed of arbitrary gates, but the use of AIGs makes them more scalable and easier to implement.


Implementations

* Logic Synthesis and Verification Syste
ABC
* A set of utilities for AIG


OpenAccess Gear
* Gin
logic library


References


See also

*
Binary decision diagram In computer science, a binary decision diagram (BDD) or branching program is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed representation of sets or relations. ...
*
Logical conjunction In logic, mathematics and linguistics, And (\wedge) is the truth-functional operator of logical conjunction; the ''and'' of a set of operands is true if and only if ''all'' of its operands are true. The logical connective that represents thi ...
---- ''This article is adapted from a column in the AC
SIGDA
b
Alan Mishchenko

Original text is availabl
here
'' Application-specific graphs Diagrams Electrical circuits Electronic design automation Formal methods