Еще недавно одним из заметных пробелов open-source EDA был полноценный инструмент для Equivalence Checking (как LEC так и SEQ), а теперь появился и такой инструмент.
Почему вообще SEC настолько полезен в реальной разработке?
Например, у нас есть уже верифицированный блок, но после timing analysis обнаружилась проблема. Мы вносим RTL-изменения, чтобы исправить критический путь: переписываем часть логики, добавляем или переносим регистры. После этого возникает вопрос, а не сломали ли мы при этом функциональность блока?
Конечно, можно снова прогонять весь regression set, но это долго и не всегда дает достаточную уверенность. SEC позволяет формально проверить, что старая и новая реализации сохраняют требуемое функциональное поведение.
Особенно интересно, что такие инструменты постепенно появляются и в open source. Коммерческим решениям пока, конечно, есть куда расти в плане возможностей и зрелости, но сам факт появления подобных инструментов - хороший показатель развития open-source EDA.
Пост написал, осталось на досуге посмотреть насколько вообще тул работоспособен🥲
Но я уверен кто-то из читателей поделится фидбеком
