Временная верификация и статический анализ, частота и причины использования первой Опции

[CaPpuCcino]

скажите, плз, используется ли не практике вообще и для синхронного дизайна в частности gate-level симуляция для временного анализа, или STA полностью вытеснил DTA?
если используется, то в каких случаях?
спб!

[sleep]

Аналогично написанному сверху, у нас тоже формальная верификация встроена в backend-маршрут: синтез + топология (RTL против нетлистов, нетлист против нетлиста).
Проблемы с неосознаваемыми ошибками формальной верификации встречаются крайне редко.
Почти все вызваны некачественным RTL.
Вообще, формальная верификация RTL против нетлистов очень завязана на тулы синтеза, как мне кажется. С определенного времени в DC, например, стали внедряться алгоритмы оптимизаций, которые неочевидны для тулов формальной верификации.
Fоrmаlity с DС очень неплохо работает. Конечно, требуется использовать с .svf вместе с нетлистами.
Проводили сравнения качества LЕC и Fоrmаlity : )
Формалити умеет верифицировать библиотеки ( .lib против .v ), очень интересно иногда : )
afaik, они могут помогать при верификации RTL с использованием assertions.

Сообщение отредактировал sleep - Jun 3 2010, 12:06