И-инверторный граф
 | Эта статья нуждается в дополнительных цитатах для проверки . ( июль 2014 г. ) |
И -инверторный граф (AIG) — это направленный ациклический граф , который представляет собой структурную реализацию логической функциональности схемы или сети . AIG состоит из узлов с двумя входами, представляющих логическое соединение , конечных узлов, помеченных именами переменных, и ребер, опционально содержащих маркеры, обозначающие логическое отрицание . Такое представление логической функции редко бывает структурно эффективным для больших схем, но является эффективным представлением для манипулирования логическими функциями . Обычно абстрактный граф представляется как структура данных в программном обеспечении .
Преобразование сети логических вентилей в AIG происходит быстро и масштабируемо. Требуется только, чтобы каждый вентиль был выражен через вентили И и инверторы . Это преобразование не приводит к непредсказуемому увеличению использования памяти и времени выполнения. Это делает AIG эффективным представлением по сравнению либо с диаграммой двоичных решений (BDD), либо с формой «суммы продуктов» (ΣoΠ), [ нужна ссылка ] то есть каноническая форма в булевой алгебре, известная как дизъюнктивная нормальная форма (ДНФ). BDD и DNF также можно рассматривать как схемы, но они связаны с формальными ограничениями, которые лишают их масштабируемости. Например, ΣoΠ — это схемы, имеющие не более двух уровней, тогда как BDD являются каноническими, то есть требуют, чтобы входные переменные оценивались в одном и том же порядке на всех путях.
Схемы, состоящие из простых вентилей, включая AIG, являются «древней» темой исследований. Интерес к AIG начался с основополагающей статьи Алана Тьюринга 1948 года. [1] по нейронным сетям, в котором он описал рандомизированную обучаемую сеть вентилей И-НЕ. Интерес продолжался до конца 1950-х годов. [2] и продолжалась в 1970-х годах, когда были разработаны различные местные преобразования. Эти преобразования были реализованы в несколькихсистемы логического синтеза и проверки, такие как Darringer et al. [3] и Смит и др., [4] которые уменьшают количество схем, чтобы уменьшить площадь и задержку во время синтеза или ускорить формальную проверку эквивалентности . Несколько важных методов были обнаружены рано в IBM , такие как объединение и повторное использование логических выражений и подвыражений с несколькими входами, теперь известных как структурное хеширование .
В последнее время возобновился интерес к AIG как к функциональному представлению для различных задач синтеза и проверки. Это связано с тем, что представления, популярные в 1990-х годах (такие как BDD), достигли предела масштабируемости во многих своих приложениях. [ нужна ссылка ] Еще одним важным событием стало недавнее появление гораздо более эффективных решателей логического выполнимости (SAT). В сочетании с AIG в качестве представления схемы они приводят к значительному ускорению решения широкого спектра логических задач . [ нужна ссылка ]
AIG нашли успешное применение в различных приложениях EDA . Хорошо настроенная комбинация AIG и логической выполнимости повлияла на формальную проверку , включая как проверку модели , так и проверку эквивалентности. [5] Другая недавняя работа показывает, что с использованием AIG можно разработать эффективные методы сжатия цепей. [6] Растет понимание того, что проблемы логики и физического синтеза можно решать с помощью моделирования и логической выполнимости для вычисления функциональных свойств (таких как симметрии). [7] и гибкие возможности узлов (такие как ненужные термины , повторные замены и SPFD ). [8] [9] [10] Мищенко и др. показывает, что AIG являются многообещающим объединяющим представлением, которое может соединить логический синтез , картографирование технологий , физический синтез и формальную проверку. Во многом это связано с простой и единообразной структурой AIG, которая позволяет перезаписывать, моделировать, отображать, размещать и проверять для использования одной и той же структуры данных.
Помимо комбинационной логики, AIG также применялись к последовательной логике и последовательным преобразованиям. В частности, метод структурного хеширования был расширен для работы с AIG с элементами памяти (такими как триггеры D-типа с начальным состоянием,что, как правило, может быть неизвестно), в результате чего получается структура данных, специально предназначенная для приложений, связанных с повторной синхронизацией . [11]
Текущие исследования включают внедрение современной системы логического синтеза, полностью основанной на AIG. Прототип под названием ABC включает пакет AIG, несколько методов синтеза и проверки эквивалентности на основе AIG, а также экспериментальную реализацию последовательного синтеза. Один из таких методов сочетает в себе картографирование технологий и изменение времени на одном этапе оптимизации. Эти оптимизации могут быть реализованы с использованием сетей, состоящих из произвольных вентилей, но использование AIG делает их более масштабируемыми и простыми в реализации.
Реализации
[ редактировать ]- Система логического синтеза и верификации ABC
- Набор утилит для AIG AIGER
- Механизм OpenAccess
- Джини Логическая библиотека
См. также
[ редактировать ]Ссылки
[ редактировать ]- ^ Статья Тьюринга 1948 года была переиздана как Turing AM. Интеллектуальная техника. В: Инс, округ Колумбия, редактор. Собрание сочинений А. М. Тьюринга — Механический интеллект. Издательство Elsevier Science, 1992.
- ^ Л. Хеллерман (июнь 1963 г.). «Каталог логических схем с тремя переменными ИЛИ-инвертор и И-инвертор». IEEE Транс. Электрон. Вычислить . EC-12 (3): 198–223. дои : 10.1109/PGEC.1963.263531 .
- ^ А. Дэрринджер; WH Джойнер-младший; К. Л. Берман; Л. Тревильян (июль 1981 г.). «Логический синтез посредством локальных преобразований». Журнал исследований и разработок IBM . 25 (4): 272–280. CiteSeerX 10.1.1.85.7515 . дои : 10.1147/rd.254.0272 .
- ^ Г.Л. Смит; Р. Дж. Бансен; Х. Холливелл (январь 1982 г.). «Логическое сравнение оборудования и блок-схем». Журнал исследований и разработок IBM . 26 (1): 106–116. CiteSeerX 10.1.1.85.2196 . дои : 10.1147/rd.261.0106 .
- ^ А. Кюльманн; В. Парути; Ф. Кром; МК Ганай (2002). «Надежные логические рассуждения для проверки эквивалентности и проверки функциональных свойств». IEEE Транс. CAD . 21 (12): 1377–1394. CiteSeerX 10.1.1.119.9047 . дои : 10.1109/tcad.2002.804386 .
- ^ Пер Бьессе; Арне Борэлв (2004). «Сжатие цепей с поддержкой DAG для формальной проверки» (PDF) . Учеб. ИККАД '04 . стр. 42–49.
- ^ К.-Х. Чанг; И. Л. Марков; В. Бертакко (2005). «Перемонтирование и повторная буферизация после размещения путем исчерпывающего поиска функциональных симметрий» (PDF) . Учеб. ИККАД '05 . стр. 56–63.
- ^ А. Мищенко; Дж. С. Чжан; С. Синха; Дж. Р. Берч; Р. Брайтон; М. Хшановска-Еске (май 2006 г.). «Использование моделирования и выполнимости для вычисления гибкости в логических сетях» (PDF) . IEEE Транс. CAD . 25 (5): 743–755. CiteSeerX 10.1.1.62.8602 . дои : 10.1109/tcad.2005.860955 . S2CID 13099806 .
- ^ С. Синха; РК Брайтон (1998). «Внедрение и использование SPFD при оптимизации логических сетей». Учеб. ИККАД . стр. 103–110. CiteSeerX 10.1.1.488.8889 .
- ^ С. Ямасита; Х. Савада; А. Нагоя (1996). «Новый метод выражения функциональных разрешений для ПЛИС на основе LUT и их приложений» (PDF) . Учеб. ИККАД . стр. 254–261.
- ^ Дж. Баумгартнер; А. Кюльманн (2001). «Ресинхронизация минимальной площади в гибких схемных структурах» (PDF) . Учеб. ICCAD’01 . стр. 176–182.