И инвертор граф (АИГ) представляет собой ориентированный ациклический граф , представляющий собой структурную реализацию логической функциональности схемы или сети . AIG состоит из узлов с двумя входами, представляющих логическое соединение , оконечных узлов, помеченных именами переменных, и ребер, необязательно содержащих маркеры, указывающие логическое отрицание . Такое представление логической функции редко бывает структурно эффективным для больших схем, но является эффективным представлением для манипулирования булевыми функциями . Обычно абстрактный граф представляется в виде структуры данных в программном обеспечении.
Преобразование сети логических вентилей в AIG выполняется быстро и масштабируемо. Требуется только, чтобы каждый вентиль был выражен в терминах логических элементов И и инверторов . Это преобразование не приводит к непредсказуемому увеличению использования памяти и времени выполнения. Это делает 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] и гибкости узлов (например, безразличных терминов , повторных замен и СПФО ). [8] [9] [10] Мищенко и др. показывает, что AIG являются многообещающим объединяющим представлением, которое может объединить логический синтез , отображение технологий , физический синтез и формальную проверку. Это в значительной степени связано с простой и единообразной структурой AIG, которая позволяет переписывать, моделировать, отображать, размещать и проверять одну и ту же структуру данных.
Помимо комбинационной логики, AIG также применялись для последовательной логики и последовательных преобразований. В частности, метод структурного хеширования был расширен для работы с AIG с элементами памяти (такими как триггеры D-типа с начальным состоянием, которое, как правило, может быть неизвестным), в результате была получена структура данных, специально адаптированная для приложений. связанные с восстановлением синхронизации . [11]
Текущие исследования включают внедрение современной системы логического синтеза, полностью основанной на AIG. Прототип под названием ABC включает пакет AIG, несколько основанных на AIG методов синтеза и проверки эквивалентности, а также экспериментальную реализацию последовательного синтеза. Один из таких методов объединяет технологическое отображение и повторное синхронизацию на одном этапе оптимизации. Эти оптимизации могут быть реализованы с использованием сетей, состоящих из произвольных вентилей, но использование AIG делает их более масштабируемыми и более простыми в реализации.
Реализации
- Система логического синтеза и проверки ABC
- Набор утилит для AIGs AIGER
- OpenAccess Gear
- Библиотека логики Джини
Рекомендации
- ^ 1948 бумага Тьюринга была повторно напечатана в Тьюринга AM. Интеллектуальная техника. В: Ince DC, редактор. Собрание сочинений А. М. Тьюринга - Механический интеллект. Издательство Elsevier Science, 1992.
- ^ Л. Хеллерман (июнь 1963). «Каталог логических схем с тремя переменными или инверторами и инверторами». IEEE Trans. Электрон. Comput . ИС-12 (3): 198–223. DOI : 10,1109 / PGEC.1963.263531 .
- ^ А. Даррингер; WH Joyner, Jr .; С.Л. Берман; Л. Тревильян (июль 1981 г.). «Логический синтез через локальные преобразования». Журнал исследований и разработок IBM . 25 (4): 272–280. CiteSeerX 10.1.1.85.7515 . DOI : 10.1147 / rd.254.0272 .
- ^ Г. Л. Смит; RJ Bahnsen; Х. Холливелл (январь 1982 г.). «Логическое сравнение оборудования и блок-схем». Журнал исследований и разработок IBM . 26 (1): 106–116. CiteSeerX 10.1.1.85.2196 . DOI : 10.1147 / rd.261.0106 .
- ^ А. Кюльманн; В. Парути; Ф. Кром; М.К. Ганай (2002). «Надежные логические рассуждения для проверки эквивалентности и проверки функциональных свойств». IEEE Trans. CAD . 21 (12): 1377–1394. CiteSeerX 10.1.1.119.9047 . DOI : 10,1109 / tcad.2002.804386 .
- ^ Пер Бьессе; Арне Борулв (2004). «Сжатие схем с поддержкой DAG для формальной проверки» (PDF) . Proc. ICCAD '04 . С. 42–49.
- ^ К.-Х. Чанг; И.Л. Марков; В. Бертакко (2005). «Перенастройка и повторная буферизация после размещения путем исчерпывающего поиска функциональных симметрий» (PDF) . Proc. ICCAD '05 . С. 56–63.
- ^ А. Мищенко; JS Zhang; С. Синха; JR Burch; Р. Брайтон; М. Хшановска-Еске (май 2006 г.). «Использование моделирования и выполнимости для вычисления гибкости в булевых сетях» (PDF) . IEEE Trans. CAD . 25 (5): 743–755. CiteSeerX 10.1.1.62.8602 . DOI : 10,1109 / tcad.2005.860955 .
- ^ С. Синха; РК Брайтон (1998). «Внедрение и использование SPFD для оптимизации булевых сетей». Proc. ICCAD . С. 103–110. CiteSeerX 10.1.1.488.8889 .
- ^ С. Ямасита; Х. Савада; А. Нагоя (1996). «Новый метод выражения функциональной допустимости для ПЛИС на основе LUT и их приложений» (PDF) . Proc. ICCAD . С. 254–261.
- ^ Дж. Баумгартнер; А. Кюльманн (2001). «Восстановление минимальной площади на гибких схемах» (PDF) . Proc. ICCAD'01 . С. 176–182.
Смотрите также
- Диаграмма двоичного решения
- Логическое соединение
Эта статья взята из колонки в ACM Сигда электронный бюллетень по Alan Мищенко
Оригинальный текст доступен здесь .