Граф and-inverter (AIG) — это направленный ациклический граф , представляющий структурную реализацию логической функциональности схемы или сети . AIG состоит из двухвходовых узлов, представляющих логическое соединение , терминальных узлов, помеченных именами переменных, и ребер, опционально содержащих маркеры, указывающие на логическое отрицание . Такое представление логической функции редко бывает структурно эффективным для больших схем, но является эффективным представлением для манипулирования булевыми функциями . Обычно абстрактный граф представляется в виде структуры данных в программном обеспечении.
Преобразование из сети логических вентилей в AIG выполняется быстро и масштабируемо. Требуется только, чтобы каждый вентиль был выражен в терминах вентилей AND и инверторов . Это преобразование не приводит к непредсказуемому увеличению использования памяти и времени выполнения. Это делает AIG эффективным представлением по сравнению с диаграммой бинарных решений (BDD) или формой «суммы произведения» (ΣoΠ), [ требуется ссылка ], то есть канонической формой в булевой алгебре, известной как дизъюнктивная нормальная форма (DNF). BDD и DNF также можно рассматривать как схемы, но они включают формальные ограничения, которые лишают их масштабируемости. Например, ΣoΠ — это схемы с максимум двумя уровнями, в то время как BDD являются каноническими, то есть они требуют, чтобы входные переменные оценивались в одном и том же порядке на всех путях.
Схемы, состоящие из простых вентилей, включая AIG, являются «древней» темой исследований. Интерес к AIG начался с основополагающей статьи Алана Тьюринга 1948 года [1] о нейронных сетях, в которой он описал рандомизированную обучаемую сеть вентилей NAND. Интерес продолжался до конца 1950-х годов [2] и продолжился в 1970-х годах, когда были разработаны различные локальные преобразования. Эти преобразования были реализованы в нескольких системах логического синтеза и проверки, таких как Darringer et al. [3] и Smith et al., [4], которые сокращают схемы для улучшения площади и задержки во время синтеза или для ускорения формальной проверки эквивалентности . Несколько важных методов были открыты рано в IBM , такие как объединение и повторное использование многовходовых логических выражений и подвыражений, теперь известных как структурное хеширование.
Недавно вновь возник интерес к AIG как к функциональному представлению для различных задач синтеза и верификации. Это связано с тем, что популярные в 1990-х годах представления (такие как BDD) достигли пределов масштабируемости во многих своих приложениях. [ необходима цитата ] Другим важным достижением стало недавнее появление гораздо более эффективных решателей булевой выполнимости (SAT). В сочетании с AIG как схемным представлением они приводят к значительному ускорению решения широкого спектра булевых задач . [ необходима цитата ]
AIG нашли успешное применение в различных приложениях EDA . Хорошо настроенное сочетание AIG и булевой выполнимости оказало влияние на формальную верификацию , включая как проверку моделей, так и проверку эквивалентности. [5] Другая недавняя работа показывает, что эффективные методы сжатия схем могут быть разработаны с использованием AIG. [6] Растет понимание того, что проблемы логического и физического синтеза могут быть решены с использованием моделирования и булевой выполнимости для вычисления функциональных свойств (таких как симметрии) [7] и гибкости узлов (таких как термины don't care , повторные замены и SPFD). [8] [9] [10] Мищенко и др. показывают, что AIG являются многообещающим объединяющим представлением, которое может объединить логический синтез , технологическое отображение, физический синтез и формальную верификацию. Это во многом связано с простой и единообразной структурой AIG, которая позволяет переписывать, моделировать, отображать, размещать и проверять, чтобы совместно использовать одну и ту же структуру данных.
В дополнение к комбинационной логике, AIG также применялись к последовательной логике и последовательным преобразованиям. В частности, метод структурного хеширования был расширен для работы с AIG с элементами памяти (такими как триггеры D-типа с начальным состоянием, которое, в общем случае, может быть неизвестным), что привело к структуре данных, которая специально предназначена для приложений, связанных с повторной синхронизацией . [11]
Текущие исследования включают внедрение современной системы логического синтеза, полностью основанной на AIG. Прототип под названием ABC включает пакет AIG, несколько методов синтеза и проверки эквивалентности на основе AIG, а также экспериментальную реализацию последовательного синтеза. Один из таких методов объединяет технологическое отображение и повторное синхронизирование в одном шаге оптимизации. Эти оптимизации могут быть реализованы с использованием сетей, состоящих из произвольных вентилей, но использование AIG делает их более масштабируемыми и простыми в реализации.