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