кстати про формалити - как-то ни разу не удалось сравнить им 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.

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

у нас сравнение полного 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 или другую программу для анализа.