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