Процесс формальной проверки эквивалентности является частью автоматизации проектирования электроники (EDA), обычно используемой при разработке цифровых интегральных схем , чтобы формально доказать, что два представления схемы демонстрируют совершенно одинаковое поведение.
Проверка эквивалентности и уровни абстракции
В общем, существует широкий диапазон возможных определений функциональной эквивалентности, охватывающих сравнения между различными уровнями абстракции и различную степень детализации деталей синхронизации.
- Наиболее распространенный подход заключается в рассмотрении проблемы машинной эквивалентности, которая определяет две синхронные проектные спецификации, функционально эквивалентные, если тактовый сигнал за тактовым сигналом они производят точно такую же последовательность выходных сигналов для любой допустимой последовательности входных сигналов.
- Разработчики микропроцессоров используют проверку эквивалентности для сравнения функций, указанных для архитектуры набора команд (ISA), с реализацией уровня передачи регистров (RTL), гарантируя, что любая программа, выполняемая на обеих моделях, вызовет идентичное обновление содержимого основной памяти. Это более общая проблема.
- Процесс проектирования системы требует сравнения между моделью уровня транзакции (TLM), например, написанной на SystemC, и соответствующей ей спецификацией RTL. Такая проверка вызывает все больший интерес в среде проектирования «система на кристалле» (SoC).
Эквивалентность синхронной машины
Уровень переноса регистра поведение (РТЛ) цифрового чипа, как правило , описывается с помощью языка описания аппаратных средств , таких как Verilog или VHDL . Это описание является золотой эталонной моделью, которая подробно описывает, какие операции будут выполняться в течение какого такта и с помощью каких аппаратных средств. После того как разработчики логики с помощью моделирования и других методов проверки проверили описание передачи регистров, проект обычно преобразуется в список соединений с помощью инструмента синтеза логики . Эквивалентность не следует путать с функциональной правильностью, которая должна определяться функциональной проверкой .
Первоначальный список соединений обычно подвергается ряду преобразований, таких как оптимизация, добавление структур Design For Test (DFT) и т. Д., Прежде чем он будет использован в качестве основы для размещения логических элементов в физическом макете . Современное программное обеспечение для физического проектирования иногда также вносит значительные изменения (такие как замена логических элементов эквивалентными аналогичными элементами, которые имеют более высокую или меньшую мощность и / или площадь привода ) в список соединений. На каждом этапе очень сложной, многоэтапной процедуры необходимо поддерживать исходную функциональность и поведение, описываемое исходным кодом. Когда окончательная запись на магнитную ленту сделана из цифрового чипа, множество различных программ EDA и, возможно, некоторые ручные правки изменят список соединений.
Теоретически инструмент логического синтеза гарантирует, что первый список соединений логически эквивалентен исходному коду RTL. Все программы позже в процессе, которые вносят изменения в список соединений, также теоретически гарантируют, что эти изменения логически эквивалентны предыдущей версии.
На практике в программах есть ошибки, и было бы серьезным риском предполагать, что все шаги от RTL до окончательного списка соединений на магнитной ленте были выполнены без ошибок. Кроме того, в реальной жизни проектировщики обычно вносят вручную изменения в список соединений, обычно известный как Engineering Change Orders , или ECO, тем самым вводя серьезный дополнительный фактор ошибки. Следовательно, вместо того, чтобы слепо предполагать, что ошибок не было, необходим этап проверки, чтобы проверить логическую эквивалентность окончательной версии списка соединений исходному описанию проекта (золотая эталонная модель).
Исторически сложилось так, что одним из способов проверки эквивалентности было повторное моделирование, используя окончательный список соединений, тестовых примеров, которые были разработаны для проверки правильности RTL. Этот процесс называется логическим моделированием на уровне вентилей . Однако проблема заключается в том, что качество проверки равно качеству тестовых примеров. Кроме того, моделирование на уровне ворот, как известно, выполняется медленно, что является серьезной проблемой, поскольку размер цифровых проектов продолжает расти в геометрической прогрессии .
Альтернативный способ решить эту проблему - формально доказать, что код RTL и синтезированный из него список соединений имеют абсолютно одинаковое поведение во всех (соответствующих) случаях. Этот процесс называется формальной проверкой эквивалентности и является проблемой, которая изучается в более широкой области формальной проверки .
Формальная проверка эквивалентности может выполняться между любыми двумя представлениями проекта: RTL <> список соединений, список соединений <> список соединений или RTL <> RTL, хотя последнее редко по сравнению с первыми двумя. Как правило, инструмент формальной проверки эквивалентности также с большой точностью указывает, в какой момент существует разница между двумя представлениями.
Методы
Есть две основные технологии, используемые для логических рассуждений в программах проверки эквивалентности:
- Диаграммы двоичных решений , или BDD: специализированная структура данных, предназначенная для поддержки рассуждений о логических функциях. BDD стали очень популярными благодаря своей эффективности и универсальности.
- Выполнимость конъюнктивной нормальной формы: решатели SAT возвращают присвоение переменным пропозициональной формулы, которое удовлетворяет ей, если такое присвоение существует. Практически любую проблему логического рассуждения можно выразить как задачу SAT.
Коммерческие приложения для проверки эквивалентности
Основными продуктами в области проверки логической эквивалентности ( LEC ) EDA являются:
- FormalPro от Mentor Graphics
- Questa SLEC от Mentor Graphics
- Conformal от Cadence
- JasperGold от Cadence
- Формальность от Synopsys
- VC Formal от Synopsys
- 360 EC от OneSpin Solutions
- ATEC от ATEC
Обобщения
- Проверка эквивалентности восстановленных схем: иногда полезно переместить логику с одной стороны регистра на другую, и это усложняет проблему проверки.
- Последовательная проверка эквивалентности: иногда две машины совершенно разные на комбинационном уровне, но должны выдавать одинаковые выходные данные, если им даны одинаковые входные данные. Классический пример - два идентичных конечных автомата с разными кодировками состояний. Поскольку это не может быть сведено к проблеме комбинаций, требуются более общие методы.
- Эквивалентность программ, то есть проверка того, эквивалентны ли две четко определенные программы, которые принимают N входов и производят M выходов: концептуально вы можете превратить программное обеспечение в конечный автомат (это то, что делает комбинация компилятора, поскольку компьютер плюс его память формируют очень большой конечный автомат.) Тогда, теоретически, различные формы проверки свойств могут гарантировать, что они производят одинаковый результат. Эта проблема даже сложнее, чем последовательная проверка эквивалентности, поскольку выходные данные двух программ могут появляться в разное время; но это возможно, и исследователи работают над этим.
Смотрите также
Рекомендации
- Руководство по автоматизации проектирования электроники для интегральных схем , Лаваньо, Мартин и Шеффер, ISBN 0-8493-3096-3 Обзор области. Эта статья была взята с разрешения Фабио Соменци и Андреаса Кюльмана из главы 4 тома 2 « Проверка эквивалентности» .
- RE Bryant, Алгоритмы на основе графов для манипулирования логическими функциями , IEEE Transactions on Computers., C-35, pp. 677–691, 1986. Первоначальный справочник по BDD.
- Последовательная проверка эквивалентности для RTL-моделей. Нихил Шарма, Гаган Хастир и Венкат Кришнасвами. EE Times .