Методы анализа выполнимости булевых формул для современных задач систем автоматизации проектирования в микроэлектронике

Методы анализа выполнимости булевых формул для современных задач систем автоматизации проектирования в микроэлектронике

Методы анализа выполнимости булевых формул являются одним из эффективных подходов к решению задачи булевого сопоставления и проверки эквивалентности цифровых схем. В комбинации с классическими трассировочными алгоритмами и оптимизационными техниками данные методы показывают результаты, превосходящие классические алгоритмы трассировки по скорости работы и качеству получаемого результата. В работе выполнен анализ современной практики применения методов на основе задачи выполнимости булевых формул в системах автоматизации проектирования сверхбольших интегральных схем. Рассмотрены примеры подходов на основе задачи выполнимости булевых формул к задачам трассировки и формальной проверки эквивалентности описаний цифровых схем в рамках технологического отображения в составе маршрута проектирования ПЛИС. Разработан и представлен алгоритм детальной трассировки блоков коммутации ПЛИС с применением задачи выполнимости. Результаты его работы продемонстрированы на примере программируемого логического блока интегральной микросхемы российского производства 5400ТР094. Блок имеет островную архитектуру, т.е. малые программируемые логические блоки и блоки коммутации образуют регулярно повторяющуюся схемотехническую структуру. Свойства выбранной классической архитектуры позволяют расширить область применения предложенного алгоритма на весь класс ПЛИС островного типа. Тестирование алгоритма проведено на наборах проектных схем ISCAS-85, ISCAS-89 и LGSynth-89. Выполнено сравнение разработанного алгоритма на основе методов анализа выполнимости булевых формул с известным алгоритмом трассировки Pathfinder по критериям затраченного времени и достигнутой степени разводимости блоков коммутации. Установлено, что методы анализа выполнимости булевых формул для задачи трассировки способны к доказательству неразводимости рассматриваемой трассировочной задачи в отличие от алгоритма Pathfinder, результаты работы которого могут лишь косвенно свидетельствовать об этом. Показано, что применение более производительного решателя для задачи выполнимости существенно ускоряет работу предложенного алгоритма детальной трассировки.
Мария Андреевна Заплетина
Институт проблем проектирования в микроэлектронике Российской академии наук, г. Москва, Россия
Денис Владимирович Жуков
Институт проблем проектирования в микроэлектронике Российской академии наук, г. Москва, Россия
Сергей Витальевич Гаврилов
Институт проблем проектирования в микроэлектронике Российской академии наук, г. Москва, Россия
Поделиться