# 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 constists of two-input nodes representing logical conjunction, terminal nodes labelled 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.
 Two structurally different AIGs for the function f(x1, x2, x3) = x2 * ( x1 + x3 )

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[1] 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.[2] and Smith et al.[3], 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.[4] Another recent work shows that efficient circuit compression techniques can be developed using AIGs.[5] 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[6]) and node flexibilities (such as don't-cares, resubstitutions, and SPFDs[7]). 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.[8]

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.

## References

1. ^ L. Hellerman (June 1963). "A catalog of three-variable Or-Inverter and And-Inverter logical circuits". IEEE Trans. Electron. Comput. EC-12: 198–223.
2. ^ A. Darringer, W. H. Joyner, Jr., C. L. Berman, L. Trevillyan (1981). "Logic synthesis through local transformations". IBM J. Of Research and Development 25 (4): 272–280.
3. ^ G. L. Smith, R. J. Bahnsen, H. Halliwell (1982). "Boolean comparison of hardware and flowcharts". IBM J. Of Research and Development 26 (1): 106–116.
4. ^ A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ganai (2002). "Robust boolean reasoning for equivalence checking and functional property verification". IEEE Trans. CAD 21 (12): 1377–1394.
5. ^ P. Bjesse and A. Boralv. "DAG-aware circuit compression for formal verification". Proc. ICCAD '04: 42–49.
6. ^ K.-H. Chang, I. L. Markov, V. Bertacco. "Post-placement rewiring and rebuffering by exhaustive search for functional symmetries". Proc. ICCAD '05`pages=56–63.
7. ^ A. Mishchenko, J. S. Zhang, S. Sinha, J. R. Burch, R. Brayton, and M. Chrzanowska-Jeske (May 2006). "Using simulation and satisfiability to compute flexibilities in Boolean networks". IEEE Trans. CAD 25 (5): 743–755..
8. ^ J. Baumgartner and A. Kuehlmann. "Min-area retiming on flexible circuit structures". Proc. ICCAD'01: 176–182.

Original text is available here.''
graph is the basic object of study in graph theory. Informally speaking, a graph is a set of objects called points, nodes, or vertices connected by links called lines or edges.
Digital electronics are electronics systems that use digital signals. Digital electronics are representations of Boolean algebra and are used in computers, mobile phones, and other consumer products.
In logic and/or mathematics, logical conjunction or and is a two-place logical operation that results in a value of true if both of its operands are true, otherwise a value of false!

## Definition

Logical conjunction

In logic and mathematics, negation or not is an operation on logical values, for example, the logical value of a proposition, that sends true to false and false to true.
A Boolean function describes how to determine a Boolean value output based on some logical calculation from Boolean inputs. These play a basic role in questions of complexity theory as well as the design of circuits and chips for digital computers.
data structure is a way of storing data in a computer so that it can be used efficiently. Often a carefully chosen data structure will allow the most efficient algorithm to be used. The choice of the data structure often begins from the choice of an abstract data type.
A logic gate performs a logical operation on one or more logic inputs and produces a single logic output. The logic normally performed is Boolean logic and is most commonly found in digital circuits.
The AND gate is a digital logic gate that implements logical conjunction - it behaves according to the truth table to the right. A HIGH output (1) results only if both the inputs to the AND gate are HIGH (1).
inverter is a logic gate which inverts the digital signal driven on its input. It is also called NOT gate. The truth table of the gate is as follows:

The truth table for inverter
input output
0 1
1 0

This represents perfect
A binary decision diagram (BDD), 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.
This article may be too technical for most readers to understand, and needs attention from an expert on its subject. Please [ expand] it to make it accessible to non-experts, without removing the technical details.

In boolean logic, a disjunctive normal form (DNF) is a standardization (or normalization) of a logical formula which is a disjunction of conjunctive clauses. As a normal form, it is useful in automated theorem proving.
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.

Public (NYSE:  IBM )
Founded 1889, incorporated 1911

Key people Samuel J.
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. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the

Electronic design automation (EDA) is the category of tools for designing and producing electronic systems ranging from printed circuit boards (PCBs) to integrated circuits. This is sometimes referred to as ECAD (electronic computer-aided design) or just CAD.
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. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the
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.
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. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the
In logic synthesis and logic simulation a don't care or X value is one value in a multi-valued logic system that denotes an unknown value, or a value that the designer (for whatever reason) does not care about.
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.
In digital circuit theory, sequential logic is a type of logic circuit whose output depends not only on the present input but also on the history of the input. This is in contrast to combinatorial logic, whose output is a function of, and only of, the present input.