反相图（AIG）是一种有向无环图，代表电路或网络逻辑功能的结构实现。AIG由表示逻辑合取的两个输入节点、标有变量名的终端节点和可选地包含表示逻辑否定的标记的边组成。逻辑函数的这种表示对于大电路来说在结构上很少是有效的，但是对于布尔函数的操作来说却是有效的表示。通常，抽象图在软件中表示为数据结构。
从逻辑门网络到AIg的转换是快速且可扩展的。它只要求每个门都用与门和反相器来表示。这种转换不会导致内存使用和运行时的不可预测的增加。与二进制决策图(BDD)或“乘积和”(o)形式相比，这使得AIG成为一种有效的表示，即齐墩代数中的典范形式，称为析取范式(DNF)。BDD和DNF也可以被视为电路，但它们涉及到形式约束，剥夺了它们的可扩展性。例如，ΣoΠs是最多具有两个电平的电路，而BDDs是规范的，也就是说，它们要求输入变量在所有路径上以相同的顺序被评估。
电路由简单的门组成，包括AIg，是一个“古老”的研究课题。对AIg的兴趣始于艾伦·图灵（Alan Turing）1948年关于神经网络的开创性论文[1]，他在论文中描述了一个可随机训练的与非门网络。兴趣一直持续到1950年代末[2]，并在1970年代继续，当时各种地方变革已经发展起来。这些转换是在几个逻辑合成和验证系统中实现的，例如Darringer等人[3]和Smith等人[4]，它们减少了电路以改善合成期间的面积和延迟，或者加速形式等价性检查。IBM早期发现了一些重要的技术，例如组合和重用多输入逻辑表达式和子表达式，现在称为结构散列。
最近，人们对AIg作为综合和验证中各种任务的功能表示重新产生了兴趣。这是因为在20世纪90年代流行的表示(如BDD)在他们的许多应用中已经达到了可伸缩性的极限。另一个重要的发展是最近出现了更有效的布尔可满足性(SAT)求解器。当与AIg结合作为电路表示时，它们在解决各种布尔问题时会显著加快速度。
AIG在各种EDA应用中获得了成功的应用。AIg和布尔可满足性的良好组合对形式验证产生了影响，包括模型检查和等价性检查[5]。最近的另一项研究表明，使用AIg可以开发出有效的电路压缩技术[6]。越来越多的人认识到，逻辑和物理综合问题可以通过模拟和布尔可满足性以计算功能属性(如对称性)[7]和节点灵活性(如无关项、结果结构和SPFDs)来解决。[8][9][10]Mishchenko等人表明AIg是一个有前途的统一表示，它可以桥接逻辑合成、技术映射、物理合成和形式验证。这在很大程度上是由于AIg的简单而统一的结构，允许重写、模拟、映射、放置和验证共享相同的数据结构。
除了组合逻辑之外，AIg还被应用于顺序逻辑和顺序变换。具体来说，结构散列法被扩展到适用于具有存储元件的AIg(例如具有初始状态的D型触发器，通常是未知的)，从而产生了专门为与重定时相关的应用定制的数据结构。[11]
正在进行的研究包括实现完全基于AIg的现代逻辑综合系统。这个名为ABC的原型有一个AIG包，几个基于AIG的合成和等价性检查技术，以及一个顺序合成的实验实现。一种这样的技术在一个优化步骤中结合了技术映射和重定时。这些优化可以使用由任意门组成的网络来实现，但是AIg的使用使它们更具可伸缩性并且更容易实现。
^图灵1948年的论文被重新印刷成图灵调幅。智能机械。作者:因斯·DC，编辑。AM图灵全集——机械智能。埃尔塞维尔科学出版社，1992年。.
^L. Hellerman (June 1963). "A catalog of three-variable Or-Inverter and And-Inverter logical circuits". IEEE Trans. Electron. Comput. EC-12 (3): 198–223. doi:10.1109/PGEC.1963.263531..
^A. Darringer; W. H. Joyner, Jr.; C. L. Berman; L. Trevillyan (Jul 1981). "Logic synthesis through local transformations". IBM Journal of Research and Development. 25 (4): 272–280. CiteSeerX 10.1.1.85.7515. doi:10.1147/rd.254.0272..
^G. L. Smith; R. J. Bahnsen; H. Halliwell (Jan 1982). "Boolean comparison of hardware and flowcharts". IBM Journal of Research and Development. 26 (1): 106–116. CiteSeerX 10.1.1.85.2196. doi:10.1147/rd.261.0106..
^A. Kuehlmann; V. Paruthi; F. Krohm; M. K. Ganai (2002). "Robust boolean reasoning for equivalence checking and functional property verification". IEEE Trans. CAD. 21 (12): 1377–1394. CiteSeerX 10.1.1.119.9047. doi:10.1109/tcad.2002.804386..
^Per Bjesse; Arne Borälv (2004). "DAG-aware circuit compression for formal verification" (PDF). Proc. ICCAD '04. pp. 42–49..
^K.-H. Chang; I. L. Markov; V. Bertacco (2005). "Post-placement rewiring and rebuffering by exhaustive search for functional symmetries" (PDF). Proc. ICCAD '05. pp. 56–63..
^A. Mishchenko; J. S. Zhang; S. Sinha; J. R. Burch; R. Brayton; M. Chrzanowska-Jeske (May 2006). "Using simulation and satisfiability to compute flexibilities in Boolean networks" (PDF). IEEE Trans. CAD. 25 (5): 743–755. CiteSeerX 10.1.1.62.8602. doi:10.1109/tcad.2005.860955..
^S. Sinha; R. K. Brayton (1998). "Implementation and use of SPFDs in optimizing Boolean networks". Proc. ICCAD. pp. 103–110. CiteSeerX 10.1.1.488.8889..
^S. Yamashita; H. Sawada; A. Nagoya (1996). "A new method to express functional permissibilities for LUT based FPGAs and its applications" (PDF). Proc. ICCAD. pp. 254–261..
^J. Baumgartner; A. Kuehlmann (2001). "Min-area retiming on flexible circuit structures" (PDF). Proc. ICCAD'01. pp. 176–182..
暂无