And-inverter graph

And-inverter graph

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.

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 gates and inverters. 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 (BDD) or the "sum-of-product" (ΣoΠ) form, that is, the canonical form in Boolean algebra known as the disjunctive normal form (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 in the late 1950s [cite journal|author=L. Hellerman|title=A catalog of three-variable Or-Inverter and And-Inverter logical circuits|journal=IEEE Trans. Electron. Comput.|volume=EC-12|month=June | year=1963|pages=198–223|doi=10.1109/PGEC.1963.263531] and continued in the 1970s when various local transformations have been developed. These transformations were implemented in severallogic synthesis and verification systems, such as Darringer et al. [cite journal|author=A. Darringer, W. H. Joyner, Jr., C. L. Berman, L. Trevillyan|title=Logic synthesis through local transformations|journal=IBM J. Of Research and Development|volume=25|issue=4|year=1981|pages=272–280] and Smith et al. [cite journal|author=G. L. Smith, R. J. Bahnsen, H. Halliwell|title=Boolean comparison of hardware and flowcharts|journal=IBM J. Of Research and Development|volume=26|issue=1|year=1982|pages=106–116] , which reduce circuits to improve area and delay during synthesis, or to speed up formal equivalence checking. 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 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 (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 applications. A well-tuned combination of "AIGs" and boolean satisfiability made an impact on formal verification, including both model checking and equivalence checking. [cite journal|author=A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ganai|title=Robust boolean reasoning for equivalence checking and functional property verification|journal=IEEE Trans. CAD|volume=21|issue=12|year=2002|pages=1377–1394] Another recent work shows that efficient circuit compression techniques can be developed using AIGs. [cite conference|author=P. Bjesse and A. Boralv|title=DAG-aware circuit compression for formal verification|booktitle=Proc. ICCAD '04|pages=42–49] There is a growing understanding that logic and physical synthesis problems can be solved using AIGs simulation and boolean satisfiability compute functional properties (such as symmetries [cite conference|author=K.-H. Chang, I. L. Markov, V. Bertacco|title=Post-placement rewiring and rebuffering by exhaustive search for functional symmetries|booktitle=Proc. ICCAD '05`pages=56–63] ) and node flexibilities (such as don't-cares, resubstitutions, and SPFDs [cite journal|author=A. Mishchenko, J. S. Zhang, S. Sinha, J. R. Burch, R. Brayton, and M. Chrzanowska-Jeske|title=Using simulation and satisfiability to compute flexibilities in Boolean networks|journal=IEEE Trans. CAD|volume=25|issue=5|month=May | year=2006|pages=743–755.] ). This work shows that AIGs are a promising "unifying" representation, which can bridge logic synthesis, technology mapping, 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 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. [cite conference|author=J. Baumgartner and A. Kuehlmann|title=Min-area retiming on flexible circuit structures|booktitle= Proc. ICCAD'01|pages=176–182]

Ongoing research includes implementing a modern logic synthesis system completely based on AIGs. The prototype called [ 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. It should be noted that these optimizations can be implemented using networks composed of arbitrary gates, but the use of AIGs makes them more scalable and easier to implement.


* Logic Synthesis and Verification System [ ABC]
* [ OpenAccess Gear]


ee also

* Binary decision diagram
* Logical conjunction

----"This article is adapted from a column in the ACM [ SIGDA] [ e-newsletter] by [ Alan Mishchenko]
Original text is available [ here] ."

Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Inverter (logic gate) — INPUT A OUTPUT NOT A 0 1 1 0 Traditional NOT Gate (Inverter) symb …   Wikipedia

  • Logic gate — A logic gate is an idealized or physical device implementing a Boolean function, that is, it performs a logical operation on one or more logic inputs and produces a single logic output. Depending on the context, the term may refer to an ideal… …   Wikipedia

  • Binary decision diagram — In the field of computer science, a binary decision diagram (BDD) or branching program, like a negation normal form (NNF) or a propositional directed acyclic graph (PDAG), is a data structure that is used to represent a Boolean function. On a… …   Wikipedia

  • List of Boolean algebra topics — This is a list of topics around Boolean algebra and propositional logic. Contents 1 Articles with a wide scope and introductions 2 Boolean functions and connectives 3 Examples of Boolean algebras …   Wikipedia

  • Logical conjunction — ∧ redirects here. For exterior product, see exterior algebra. Venn diagram of …   Wikipedia

  • Beaver Bit-vector Decision Procedure — Beaver is a Satisfiability Modulo Theories (SMT) decision procedure for the theory of quantifier free finite precision bit vector arithmetic ( [ BV.smt QF BV] ). Its prototype implementation… …   Wikipedia

  • AIG (disambiguation) — AIG is American International Group, a major American insurance corporation.AIG may also refer to: *And inverter graph, a concept in computer theory *Answers in Genesis, a creationist organization in the U.S. *Arta Industrial Group in Iran… …   Wikipedia

  • Glossary of fuel cell terms — The Glossary of fuel cell terms lists the definitions of many terms used within the fuel cell industry. The terms in this glossary may be used by fuel cell industry associations, in education material and fuel cell codes and standards to name but …   Wikipedia

  • Compact fluorescent lamp — Low energy light bulb redirects here. For other low energy bulbs, see LED lamp. The tubular type compact fluorescent lamp is one of the most popular types in Europe …   Wikipedia

  • Multijunction photovoltaic cell — Multi junction solar cells or tandem cells are solar cells containing several p n junctions. Each junction is tuned to a different wavelength of light, reducing one of the largest inherent sources of losses, and thereby increasing efficiency.… …   Wikipedia