Процесс проверки формальной эквивалентности является частью автоматизации электронного проектирования (EDA), обычно используемой при разработке цифровых интегральных схем , чтобы формально доказать , что два представления проекта схемы демонстрируют совершенно одинаковое поведение.
В общем, существует широкий спектр возможных определений функциональной эквивалентности, охватывающих сравнения между разными уровнями абстракции и различной степенью детализации временных деталей.
Поведение цифрового чипа на уровне передачи регистров ( RTL) обычно описывается с помощью языка описания аппаратного обеспечения , такого как Verilog или VHDL . Это описание является золотой эталонной моделью, которая подробно описывает, какие операции будут выполняться в течение какого такта и какими аппаратными средствами. После того как разработчики логики с помощью моделирования и других методов проверки проверили описание передачи регистров, проект обычно преобразуется в список соединений с помощью инструмента логического синтеза . Эквивалентность не следует путать с функциональной корректностью, которая должна определяться путем функциональной проверки .
Первоначальный список соединений обычно подвергается ряду преобразований, таких как оптимизация, добавление структур Design For Test (DFT) и т. д., прежде чем он будет использован в качестве основы для размещения логических элементов в физическом макете . Современное программное обеспечение для физического проектирования иногда также вносит существенные изменения (например, заменяет логические элементы эквивалентными аналогичными элементами, имеющими более высокую или меньшую мощность привода и/или площадь) в список соединений. На каждом этапе очень сложной, многоэтапной процедуры необходимо сохранять исходную функциональность и поведение, описанное исходным кодом. Когда окончательная запись будет сделана на цифровом чипе, множество различных программ EDA и, возможно, некоторые ручные правки изменят список соединений.
Теоретически инструмент логического синтеза гарантирует, что первый список соединений логически эквивалентен исходному коду RTL. Все программы, которые позже вносят изменения в список соединений, теоретически также гарантируют, что эти изменения логически эквивалентны предыдущей версии.
На практике в программах есть ошибки, и было бы большим риском предполагать, что все шаги от RTL до окончательного списка соединений для записи на ленту были выполнены без ошибок. Кроме того, в реальной жизни проектировщики часто вносят ручные изменения в список соединений, широко известный как « Приказы на инженерные изменения » или ECO, тем самым внося серьезный дополнительный фактор ошибок. Следовательно, вместо того, чтобы слепо предполагать, что ошибок не было, необходим этап проверки для проверки логической эквивалентности окончательной версии списка соединений исходному описанию конструкции (золотой эталонной модели).
Исторически сложилось так, что одним из способов проверки эквивалентности было повторное моделирование с использованием окончательного списка соединений тестовых примеров, разработанных для проверки правильности RTL. Этот процесс называется логическим моделированием уровня вентиля . Однако проблема в том, что качество проверки зависит только от качества тестовых примеров. Кроме того, моделирование на уровне ворот выполняется крайне медленно, что является серьезной проблемой, поскольку размер цифровых проектов продолжает расти в геометрической прогрессии .
Альтернативный способ решить эту проблему — формально доказать, что код RTL и синтезированный на его основе список соединений ведут себя одинаково во всех (релевантных) случаях. Этот процесс называется формальной проверкой эквивалентности и представляет собой проблему, изучаемую в рамках более широкой области формальной проверки .
Формальная проверка эквивалентности может быть выполнена между любыми двумя представлениями проекта: RTL <> список соединений, список соединений <> список соединений или RTL <> RTL, хотя последнее встречается редко по сравнению с первыми двумя. Обычно инструмент проверки формальной эквивалентности также с большой точностью указывает, в какой момент существует разница между двумя представлениями.
Существуют две основные технологии, используемые для логических рассуждений в программах проверки эквивалентности:
Основными продуктами EDA в области проверки логической эквивалентности ( LEC ) являются: