Формальная проверка эквивалентности

Процесс проверки формальной эквивалентности является частью автоматизации электронного проектирования (EDA), обычно используемой при разработке цифровых интегральных схем , чтобы формально доказать , что два представления проекта схемы демонстрируют совершенно одинаковое поведение.

Проверка эквивалентности и уровни абстракции

В общем, существует широкий диапазон возможных определений функциональной эквивалентности, охватывающих сравнения между различными уровнями абстракции и различной степенью детализации временных деталей.

• Наиболее распространенный подход заключается в рассмотрении проблемы машинной эквивалентности, которая определяет две синхронные спецификации проекта, функционально эквивалентные, если они такт за тактом создают точно такую ​​же последовательность выходных сигналов для любой допустимой последовательности входных сигналов.
• Разработчики микропроцессоров используют проверку эквивалентности для сравнения функций, указанных для архитектуры набора команд (ISA), с реализацией уровня передачи регистров (RTL), гарантируя, что любая программа, выполняемая на обеих моделях, приведет к идентичному обновлению содержимого основной памяти. Это более общая проблема.
• Процесс проектирования системы требует сравнения модели уровня транзакций (TLM), например, написанной на SystemC , и соответствующей спецификации RTL. Такая проверка вызывает все больший интерес в среде проектирования систем на кристалле (SoC).

Эквивалентность синхронных машин

языка описания Поведение цифрового чипа на уровне передачи регистров (RTL) обычно описывается с помощью аппаратного обеспечения , такого как Verilog или VHDL . Это описание является золотой эталонной моделью, которая подробно описывает, какие операции будут выполняться в течение какого такта и какими аппаратными средствами. После того как разработчики логики с помощью моделирования и других методов проверки проверили описание передачи регистров, проект обычно преобразуется в список соединений с помощью инструмента логического синтеза . Эквивалентность не следует путать с функциональной корректностью, которая должна определяться путем функциональной проверки .

Первоначальный список соединений обычно подвергается ряду преобразований, таких как оптимизация, добавление структур Design For Test (DFT) и т. д., прежде чем он будет использован в качестве основы для размещения логических элементов в физическом макете . Современное программное обеспечение для физического проектирования иногда также вносит существенные изменения (например, заменяет логические элементы эквивалентными аналогичными элементами, имеющими более высокую или меньшую мощность и/или площадь привода ) в список соединений. На каждом этапе очень сложной, многоэтапной процедуры необходимо сохранять исходную функциональность и поведение, описанное исходным кодом. Когда окончательная запись будет сделана на цифровом чипе, множество различных программ EDA и, возможно, некоторые ручные правки изменят список соединений.

Теоретически инструмент логического синтеза гарантирует, что первый список соединений логически эквивалентен исходному коду RTL. Все программы, вносящие изменения в список соединений на более позднем этапе процесса, также теоретически гарантируют, что эти изменения логически эквивалентны предыдущей версии.

На практике в программах есть ошибки, и было бы большим риском предполагать, что все шаги от RTL до окончательного списка соединений для записи на ленту были выполнены без ошибок. Кроме того, в реальной жизни проектировщики часто вносят ручные изменения в список соединений, широко известный как « Приказы на инженерные изменения » или ECO, тем самым внося серьезный дополнительный фактор ошибок. Следовательно, вместо того, чтобы слепо предполагать, что ошибок не было, необходим этап проверки для проверки логической эквивалентности окончательной версии списка соединений исходному описанию конструкции (золотой эталонной модели).

Исторически сложилось так, что одним из способов проверки эквивалентности было повторное моделирование с использованием окончательного списка соединений тестовых примеров, разработанных для проверки правильности RTL. Этот процесс называется логическим моделированием уровня вентиля . Однако проблема в том, что качество проверки зависит только от качества тестовых примеров. Кроме того, моделирование на уровне ворот, как известно, выполняется медленно, что является серьезной проблемой, поскольку размер цифровых проектов продолжает расти в геометрической прогрессии .

Альтернативный способ решить эту проблему — формально доказать, что код RTL и синтезированный на его основе список соединений ведут себя одинаково во всех (релевантных) случаях. Этот процесс называется формальной проверкой эквивалентности и представляет собой проблему, изучаемую в рамках более широкой области формальной проверки .

Формальная проверка эквивалентности может быть выполнена между любыми двумя представлениями проекта: RTL <> список соединений, список соединений <> список соединений или RTL <> RTL, хотя последнее встречается редко по сравнению с первыми двумя. Обычно инструмент проверки формальной эквивалентности также с большой точностью указывает, в какой момент существует разница между двумя представлениями.

Методы

Существуют две основные технологии, используемые для логических рассуждений в программах проверки эквивалентности:

• Бинарные диаграммы решений , или BDD: специализированная структура данных, предназначенная для поддержки рассуждений о логических функциях. BDD стали очень популярны благодаря своей эффективности и универсальности.
• Выполнимость конъюнктивной нормальной формы: решатели SAT возвращают присвоение переменным пропозициональной формулы , которая удовлетворяет ей, если такое присвоение существует. Почти любую задачу логического рассуждения можно выразить как задачу SAT.

для

в области проверки логической эквивалентности ( LEC ) Основными продуктами EDA являются:

• FormalPro от Mentor Graphics
• Questa SLEC от Mentor Graphics
• Конформный от Cadence
• Джаспер от Каденс
• Формальность от Synopsys
• Официальный венчурный капитал от Synopsys
• 360 EC от OneSpin Solutions
• ATEC от ATEC

Обобщения

• Проверка эквивалентности схем с повторной синхронизацией. Иногда полезно переместить логику с одной стороны регистра на другую, и это усложняет задачу проверки.
• Последовательная проверка эквивалентности: иногда две машины совершенно различны на комбинационном уровне, но должны давать одинаковые выходные данные, если им предоставлены одинаковые входные данные. Классический пример — два одинаковых конечных автомата с разными кодировками состояний. Поскольку эту задачу нельзя свести к комбинационной задаче, требуются более общие методы.
• Эквивалентность программ, то есть проверка эквивалентности двух четко определенных программ, которые принимают N входных данных и производят M выходных данных. Концептуально вы можете превратить программное обеспечение в конечный автомат (это то, что делает комбинация компилятора, поскольку компьютер плюс его память образуют очень большой конечный автомат.) Тогда теоретически различные формы проверки свойств могут гарантировать, что они выдадут одинаковый результат. Эта проблема даже сложнее, чем последовательная проверка эквивалентности, поскольку выходные данные двух программ могут появляться в разное время; но это возможно, и исследователи работают над этим.

См. также

• Формальные методы

Ссылки

• Справочник по автоматизации проектирования электронных систем для интегральных схем , автор: Лаваньо, Мартин и Шеффер, ISBN   0-8493-3096-3 Обзор поля. Эта статья была взята с разрешения из тома 2, главы 4 «Проверка эквивалентности» . Фабио Соменци и Андреаса Кюльмана
• Р.Э. Брайант, Алгоритмы на основе графов для манипулирования булевыми функциями , IEEE Transactions on Computers., C-35, стр. 677–691, 1986. Оригинальная ссылка на BDD.
• Последовательная проверка эквивалентности моделей RTL. Нихил Шарма, Гаган Хастир и Венкат Кришнасвами. ЭЭ Таймс .

Внешние ссылки

• CADP – предоставляет инструменты проверки эквивалентности для асинхронных проектов.
• OneSpin 360 EC-FPGA – Функциональная корректность синтеза FPGA от кода RTL до конечного списка соединений