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

У нас в конторе, начиная с 0.35мкм уже не используем gate-level для тайминга. Только STA.

А gate-level + SDF используется (иногда) для функциональной верификации: бывает находятся ошибки невыявляемые при RTL моделировании (обычно в схемах где есть передачи между разными клоковскими доменами).

наш посредник (делают бэк-енд)
настаивает на прохождении как можно большего объема тестов по различным "углам", то есть sdf-ов полно

технологии модные - 90нм, 40нм

--------------------

ну и вообще предполагается, что это необходимый этап - синопсисы при продвижении своего VCS-а напирают на его шустрости при симуляции gate-level

--------------------

в принципе я могу найти логические объяснения для нашего конкретного флоу,
ну а вообще - если стоимость бага несколько лимонов баксов - почему бы не просимулировать?

Мы тоже гоняем симуляции (65nm). Слишком дорого баги исправлять, а прогнать симуляции - неделя или чуть больше.

ребята, указывайте, пожалуйста ещё и причину, по которой отдаётся предпочтение динамической верификации. мне просто показалось по публикациям, что методы STA стали довольно продвинутыми. какие причины? финансовые, функциональные, внедренческие...

Одно другого не отменяет. Даже если STA прошел, то это не значит что при написании констрейнов не ошиблись. Я думаю основная причина - человеческие ошибки.

У меня, например, был случай: в функциональном описании все работало, а в gate-level нет. Причиной было отсутствие сброса одного из регистров и в функциональном моделировании if давал false и все работало дальше, а в gate-level все разваливалось в X.

спасибо, человеческий фактор мне как-то в голову не приходил.
а с примером вы наверное немого ошиблись, всё-таки функциональное моделирование к STA относится также, как двухуровневый сигнал в вашем RTL описании, проинициализированный в начале симуляции 0, относится к 4-уровневому после синтеза, инициализированному симулятором в Х. не так ли?

Ну как сказать, вопрос был о том зачем использовать gate-level, если STA прошел. Вот такая ошибка и была бы пропущена.
А сигналы в RTL ровно такие же 4-х уровневые.

Многое уже было правильно написано выше.
Для собственного спокойствия и удовлетворения начальства : ) рекомендуется проводить симуляцию gate-level netlist-ов.
Позволяет
* адекватно оценить на желаемых тестах качественность latency, skew клоковых деревьев и деревьев сброса;
* убедиться, что все триггеры, нуждающиеся в сете/ресете, его действительно имеют - посмотреть на отсечение X-ов через мультиплексоры в схеме после синтеза;
* убедиться в максимальной частоте не только на этапе STA в топологии (например, неправильно описаны propagated clock, multicycle_path, false_path, ...). Если существуют специальным образом выравниваемые тракты данных - позволяет удостовериться, что в backend поняли и сделали всё правильно;
* убедиться в качественности/полноте требуемых у backend ограничений;
* позволяет оценить, что для всех углов процесс/температура/питание требования по setup, hold выполняются. Чем глубже технология, тем больше таких углов->вариантов задержек для схемы;
* вроде при проектировании с low-power методологией есть необходимость моделирования некоторых моментов;
* способствует общению моделировщиков с бэкэндерами, что всегда полезно и синергетично;
* для нормального анализа мощности и просадок питания (IR-drop) схемы очень неплохо предоставить backend-у данные по переключениям конкретной имплементации (VCD).

Вообще говоря, качественный STA + формальная верификация RTL против топологического нетлиста дает достаточно уверенности, что всё сделано правильно.
Слышал, что китайцы в погоне за сроками выхода очередной кальки не могут себе позволить роскоши моделировать нетлисты с задержками, ограничиваются STA + FV.

гранд мерси! очень красиво всё сформулировано.

Как и сказали выше формальная верификация + СТА заменяют гейт левел симуляцию (по слухам NXP так делает)
Походу гейтлевел пользуют в случае если не удалось косяк поймать предыдущими методами - очень затратно по времени ИМХО

Мне кажется, что в реалиях наших дизайн-центров стоимость провала/ограничения функционала чипа из-за недосмотра/недостатка опыта при STA+формальной верификации намного выше,
чем +неделя на прогон тестов на gate-level netlist. Кроме того, запуски нескольких таких тестов можно делать в параллель.
afaik минимум 2-3 дизайн-центра в Мск+Питере, делающих реальные чипы в кремнии, используют симуляцию на netlist.

У нас тоже нетлисты гоняют - но я говорил про nxp не знаю какой у вас объем микросхем - у нас на достаточно малые проекты, примено тоже неделя выходит - хуже когда несколько доменов питания.... сами понимаете что будет если начать гонять нетлист дизайна >1млн вентилей через разные корнеры напряжения и температуры и процесса - неделей никак не обойдешься

под человеческим фактором я бы подразумевал не возможность допустить ошибку, а нежелание рисковать, хотя это почти одно и то же
то есть менеджер проекта говорит : мы сделали N успешных тэйпаутов и всегда пользовались симуляцией нетлиста, что теперь, когда подготовко к производству стоит еще дороже мы будем рисковать уйти на респин????? это диверсия

также для качественного STA и FV нужно иметь достаточно дорогие PT и formality (ну или аналоги), а симулятор по любому покупать




но тут осуществима мечта производителей процессоров и тулзов - процесс паралелится : при количестве лицензий == количеству корнеров все замечательно , но стоит денег...

тот же менеджер тебе как комманде сегодня даст сделать один проект с временным лимитом в который ты едва едва влазишь а завтра в два раза сложнее и с тем же временным лимитом - и хочет он или не хочет а придется...
Кстати не только лицензии стоят денег но и машинное время - в какой то момент стоимость тулзов может сравняться с ним... Да и компьютеры на которых можно вести симуляцию нетлиста не всегда свободны...

кстати про формалити - как-то ни разу не удалось сравнить им RTL исходник и нетлист
да, для трансформации нетлистов - формалити говорит ОК (ну или теоретически не ОК),
а для нелист/RTL - ХЗ
может проблема в сложности и некоторой анти-линтовости наших исходников, но результата не достигли (этим не я занимался, но весьма квалифицированные товарищи)

вообще FV достаточно мутный, имхо, струмент в нынешних дизайн фловах, то есть ее назначение - проверка того, что синтез и всякие ин-плейс-импруверы не нарушили логику
типа, вместо того чтоб сделать хорошие дороги изобретают вездеход

я понимаю, что в теории можно сделать функциональное описание ( в виде специальных утверждений или еще как - вроде есть специальные языки) и по нему проверять дизайн - но хтож его будет делать?



ну это наверно только в больших компаниях, где за покупку оптом лицензий скидки большие - так комп с 200ГБ ОЗУ и 4-мя процами (каждый хоть 6-ти ядерный да еще и гиперсрединг) стоит 20к$ а минимальная лицензия на ncsim 30+k$
upd: и при этом со временем стоимость компов уменьшается, а лицензии растет

уж не знаю 50 человек это большая компания или нет но нормальных компов не так много

У нас всё всегда проверяется с помощью формальной верификации (RTL с нетлистом после синтеза и после трассировки). Проблемы с несравнением (из-за глупости САПР FV, а не из-за САПР синтеза) встречаются, но редко. Дизайны у нас большие, так что бъем их на куски, а потом сравниваем по-отдельности.

Вообще, мой опыт показывает, что вполне можно доверять результатам Ptime + FV. А gate-level моделирование с таймингом использовать как дополнительный (необязательный) инструмент только для выявления человеческих ошибок при написании констрэйнтов для Ptime. Из-за большого объма наших дизайнов, проверить хоть как-то функциональность не представляется возможным (моделирование шло бы месяцами).

об этом я и говорил в самом начале...

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

у нас сравнение полного RTL с нетлистом (и .svf) вызывает мильйоны (ладно, сотни тысяч) анчекабле поинтс, что с ними делать - не понятно. написать какой-то скрипт чтоб он их расчекал? а как - доки я не нашел, вразумительного ответа от разных саппортов не получил. ну и вопрос в достоверности такого результата. поэтому формалити как-то не прижилось у нас.

качество RTL - вопрос особый, два хороших примера - это открытые OpenSPARC и Gaisler GRLIB, первое в виде описания регистровых стэйджей и логики между ними, второе хуман-френдли высокоуровневое описание. первое хорошо синтезируется и (наверно) формально верифицируется, но "понять невозможно и не пытайтесь" (с), а второе очень много варнингов при синтезе генерит и в формальной верификации плохо подвергается (если кому-нибудь не лень - проверьте, может я не умею их готовить), зато можно очень быстро понять что и как устроено и кастомизировать как хочется
так как - тайм ту маркет, то второй вариант кажется более правильным в условиях ограниченных ресурсов (людей/времени и т.п.) вообще мне кажется, что современные подход к проектированию можно сформулировать - пишем говеный код, затем его хорошо верифицируем (и по моему это правильно)
поэтому мне бы хотелось внедрить формальную верификацию в наш флоу, но пока не получилось
upd : понятно, что в синтез отдается RTL, который верифицирован максимально полно и задача формальной верификации использовать этот RTL как golden reference, то есть независимо от качества самого описания (стиля RTL), полученный после RTL верификации результат является качественным RTL

а симуляция нетлиста проводится восновном для проверки соединения частей. это и по человеческим факторам самое слабое место и синтез/констрейны более хитрые. полную функциональную верификацию отдельных узлов на полном нетлисте есс-но не получается сделать.

Таки не понял netlist зачем моделировать, после определенных размеров чипа максимум что можно сделать это запустить 1-2 теста, т.е. работает не работает и все, ни о каком анализе задержек речь не идет в принципе.
Formal verification -> LINT -> Synthez + STA + Formality
........................... -> FPGA (all test)

Вы правы. При больших размерах чипа запускать много тестов на уровне вентилей слишком накладно по времени. Тем не менее делать это все таки есть смысл. Прежде всего потому, что тестовое покрытие лишним не бывает. Ведь не секрет, что абсолютно все проверить невозможно за разумный промежуток времени. Случай из практики. Два взаимоисключающих интерфейса были подключены к одним и тем же входам. К сожалению один из них не был полностью отключен, когда работал другой (ошибка в проектировании). В RTL моделировании это было не найдено, несмотря на довольно большую работу по верификации. Не будем сейчас обсуждать детали. В моделировании netlist, к счастью, произошла X-prop, что в конечном итоге спасло чип от неоправданного респина.
Еще одна причина зачем стоит делать gate-level sims столько, сколько это возможно в том, что STA программы не очень хорошо справляются с анализом асинхронных цепей. Если таковые имеются и даже если вам удалось к ним применить constraints, не моделировать netlist на мой взгляд верх легкомыслия.
Ну и еще одно, хотя наверно далеко не последнее в списке это то, что один из обязательных анализов для чипа является оценка потребляемой мощности. Для получения более менее реалистичной картины нам необходимы данные о статистике переключений для различных режимов работы. Ее мы можем получить из VCD от симуляции netlist и добавить как дополнительные исходные данные в PTPx или другую программу для анализа.