[Maverick_ 15]

...

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

главное чтоб совесть не мучила, ну, и боязнь возможного судебного преследования. а то вдруг я обижусь. :)

правильно! А на форуме из постов можно книгу писать - полезной информации море! :)

PS Главное знать где взять или как искать...

[CaPpuCcino 0]

да, написан целый раздел, с примером, а пояснения к этому примеру (например объяснение термина динамическая верификация) дается много позднее.

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

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

[des00 25]

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

тогда считайте меня детским садом, впервые эти термины я встретил именно у вас. Если мне память не изменяет никто из Verification Guru не использует таких терминов.

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

ИМХО для тех кто пробовал и дальше не пошел, прочитав первоначальную версию, не захочет идти дальше %) Это как с тем же таймквестом, можно дать на простых примерах постепенно введя в глубину, а можно сразу вывалить тучу команд и сказать "Ну а теперь в дальний путь" и отрыв башни %)

[CaPpuCcino 0]

Если мне память не изменяет никто из Verification Guru не использует таких терминов.

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

и сразу наводящий вопрос: вы кого кроме Бергерона читали?(хотя это опционально, если не затруднит припомнить)

[CaPpuCcino 0]

У вас очень ограниченное понятие эталонной модели. Т.е. под эталонной моделью может пониматься всё что угодно, что используется для однозначной проверки функциональности модуля. И это не обязательно предварительно рассчитанный результат, что ему мешает вычисляться на лету? Т.е. стоит отлаженная идеалка какой либо системы и верифицируемый модуль должен давать точно такой ответ, идеалка в вашей системе терминов это не эталонная модель, тогда как это в корне не так.

 

А scoreboard есть всегда и везде, в любом автоматическом тестбенче, хоть с моделью, хоть без оной. И в нем рано или поздно, будет главный if вида if (pipa != popa) begin err_cnt++; bla bla bla end

я подумал над вашим замечанием - я действительно смешал классификацию инлайн/оффлай тестов с опорной моделью(при том у меня в раздле по моделированию у самого было написано о том, что модели более высокого уровня абстракции могут испоьзоваться при симуляции как опорные, а тут из-за того что использовал термин golden reference смешал ри переводе несколько понятий golden reference и reference model - я всегда интерпретровал golden reference как функциональную модель, которую обычно пишут на программистских языках для отладки разных реализаций алгоритма, результаты выполнения этих рограмм обчно используются как golden reference в офлайн режиме и в принципе golden reference является подмножеством в reference model, которые как класс могут использоваться как инлайн(монтор) так и оффлайн. а я инлайн reference model приравнял к scoreboarding-у. к scoreboarding же следует скоре относится как к возможности отложеной инлайн проверки, в частности внеочередного исполнения (out-of-order execution). в принципе в классификацию ещё нужно внести модели проверяюще пути данных и поток исполнения (то что сейчас assertion-ами констрейнят, хотя раньше тоже приходилось делать на HDL) - на мой взгляд это тоже отдельный тип. в общем буду этото продраздел переделывать - нужно только найти признаки для классификации. то что вы предлагали по поводу того чтобы свести всё к black-box/white-box, конечно заманчиво, но на мой взгляд не из той области - эта классификация основывается на отношении к прозрачности структуры, но ничего не говорит о качестве опорного преобразования.

в общем надо думать... два дня :) .

 

тогда считайте меня детским садом, впервые эти термины я встретил именно у вас. Если мне память не изменяет никто из Verification Guru не использует таких терминов.

на всякий случай отвечу предметно, чтобы закрыть тему:

конкретно о динамической и статической верификации: динамическая верификация - это синоним верификации на основе динамической симуляции; статическая верификация - синоним формальной верификации. правда с последним не всё так однозначно, потому как некоторые считают её не полным синонимом, так как формальная верификация включает и подход с полным покрытием всех состояний системы(используются assert и assume из PLS и SVA) например 0-in от Ментора(у синопсиса не знаю - не юзал, но точно должен быть), и верификацию на основе доказательства теорем с помощью солверов(а она в общем-то не статическая, т.е. требует участия оператора в интерактивном режиме. кстати, сейчас вещь, слава богу, экзотическая)

в общем-то я как-то уже однажды рассказывал об этой кижёнке, но думаю стоит повторить, так как вещь полезная, для того чтобы разговаривать на одном языке:

как-то давным-давно в конце прошлого века была такая ассоциация Virtual Socket Interface Alliance(VSIA) и занималась она очень полезной деятельностью до 2008 года, пока её участники в конец не рассорились из-за того что никак не могли поделить "кто из них папа". включала она ни много ни мало, а с сотню компаний по разработке аппаратуры и тулзов к ним. может там конечно не все были Verification Guru, но такие компании как Synopsys, Mentor, Cadence, Magma в ней активно участвовали. занимались они в частности тм, что пытались договорится на каком языке им друг с другом разговаривать за разработческую жизнь и в '99 всё-таки договорились выпустить стандарт по терминам, прелесть его в том, что это не просто english-english, а достаточно Толковый(в прямом смысле слова) словарь с подробными обсуждениями основных идей и концепций.

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

он, как я уже говорил, появился на шарах. думаю имеет смысл загрузить его в сельский элеватор, пока его не потёрли.

http://electronix.ru/forum/index.php?showt...st&p=761775

[SergeyF 0]

формальная верификация включает и подход с полным покрытием всех состояний системы(используются assert и assume из PLS и SVA) например 0-in от Ментора(у синопсиса не знаю - не юзал, но точно должен быть), и верификацию на основе доказательства теорем с помощью солверов(а она в общем-то не статическая, т.е. требует участия оператора в интерактивном режиме. кстати, сейчас вещь, слава богу, экзотическая)

Можно поинтересоваться, почему "слава богу"? Считаете, что у этого направления нет перспектив? В других областях, в том же управлении сложными техническими объектами, с формальным доказательством корректности системы управления все в порядке.

 

Относительно статьи. Присоединяюсь к замечаниям про тяжелый язык и отсутствие примеров. Из моих студентов ее смогли бы понять в степени, достаточной для практического применения, не более 20% студентов. А те 20%, которые поняли бы, в большинстве своем были бы склонны больше к теоретической работе. Получается противоречие, так как статья о сугубо инженерной задаче.

 

Cтатья подразумевает широкую эрудицию читателя. Например, далеко не каждый разработчик ПЛИС знаком с функциональными языками. Я знаком, но фраза о схожести с функциональными языками декларативных синтаксических конструкций для реализации механизма управления рандомизацией поставила меня в тупик. Такие экскурсы "вширь" стоит убирать, упрощать или пояснять.

[CaPpuCcino 0]

Можно поинтересоваться, почему "слава богу"?

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

 

все видели как программерам трудно переключить мозг на HDL (все когда-то были сначала немного программерами). многие видели как тем избранным, которые смогли перестроить свой мозг на параллельное мышление HDL, тяжело давались ещё более высокая абстракция PSL или SVA(с этим ещё не все пока справились) - мне например было достаточно трудно, долго и упорно переключить свой мозг на PSL(кстати труднее даже, чем на HDL мышление). теперь представьте как же нужно не любить людей, чтобы заставить их ещё раз перевернуть своё сознание на 540 градусов, чтобы сначала понять например ML, а потом сказать, что железка - это на самом деле набор аксиом, а свойства - это предпосылки, которые нужно доказать или опровергнуть с помощью формальной логики.

т.е. в самих функциональных языках ещё нет ничего особо сложного, главное к ним привыкнуть. но научится с их помощью общаться с солверами - вот на это сложно переключиться.

на мой взглд гораздо удобнее пользоваться PSL/SVA для покрытия путей графа состояний, самое главное, что те же утверждения можно использовать в динамической верификации или в смешанной (т.е. спецификация свойств намного универсальней)

В других областях, в том же управлении сложными техническими объектами, с формальным доказательством корректности системы управления все в порядке.

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

 

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

строго говоря это в общем-то и не справедливо(можно говорить скорее о классических идеях ФЯ), просто функциональные языки - самое близкое с чем можно сравнить. если написать, что это просто декларативный язык, то тоже плохо, потому что декларативные языки - слишком широкое понятие - HDL это тоже декларативный язык, но трансфрмация данных там описывается императивными конструкциями. а для тестбенчей это в прямом смысле слова императивные языки, т.е. описывают поток управления тестбенчем. HTML тоже декларативный(хотя с трудом язык :) ).

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

[SergeyF 0]

 

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

Я сам этой темой тоже не занимаюсь. Ссылки как раз недавно просил у заведующего лабораторией в ИПУ, но пока еще не получил. В частности, я имел в виду представление систем сетями Петри и анализ их свойств в рамках имитационного моделирования технологических процессов (дискретно-событийные системы и т.д.).

 

Спасибо за комментарий по PSL/SVA. С PSL я не работал, только с SVA. Конечно, так удобно описывать требования к системе. И я все равно не понимаю, зачем нам функциональные языки, если по сути свойства, задекларированные свойства можно рассматривать как утверждения в рамках временной логики, которые и надо доказать над нашим описанием. То есть, хотелось бы прояснить в данном случае границу между статической верификацией в виде того же 0-in и солверами. :)

 

Замечу, что в данном случае я не эксперт, а скорее любопытствующий, которому хочется прояснить терминологию. Специально прочитал указанный документ с терминологией, в частности, вот это: "Some consider static functional verification to be a subset of formal verification; others consider them equivalent". И далее разделы с определением Property/model Checking и Theorem Proving - я не вижу настолько большой разницы, чтобы нельзя было привести все к анализу свойств.

 

[CaPpuCcino 0]

Замечу, что в данном случае я не эксперт, а скорее любопытствующий, которому хочется прояснить терминологию. Специально прочитал указанный документ с терминологией, в частности, вот это: "Some consider static functional verification to be a subset of formal verification; others consider them equivalent". И далее разделы с определением Property/model Checking и Theorem Proving - я не вижу настолько большой разницы, чтобы нельзя было привести все к анализу свойств.

там подход разный: в случае со статической верификацией(та которая на основе языков спецификации свойств) создаётся дерево всевозможных переходов, т.е. граф состояний-переходов который обычно связный типа описания машины состояний(FSM) разворачивается в древовидную структуру (например модель(граф) Крипке) от какого-то конкретного состояния в следующие возможные, за ними следующие возможные уже из новых состояний и т.д., это дерево переходов и покрывается свойствами описанными грамматикой временной логики(temporal logic, например LTL, CTL, CTL*), как только какой-то путь совпадает с шаблоном свойства описанным на PSL/SVA, свойство удовлетворено и дальнейшая трассировка не нужна.

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

[CaPpuCcino 0]

господа, подскажите пожалуйста по терминологии. мне нужно для перевода. задал вопрос в разделе для новичков (вот здесь http://electronix.ru/forum/index.php?showt...st&p=764748 ), но боюсь, что консультации я там не получу, потому как аудитория у этого подфорума ограниченная.

[LV26 0]

господа, подскажите пожалуйста по терминологии. мне нужно для перевода. задал вопрос в разделе для новичков (вот здесь http://electronix.ru/forum/index.php?showt...st&p=764748 ), но боюсь, что консультации я там не получу, потому как аудитория у этого подфорума ограниченная.

 

может так:

 

-- системы с быстрым откликом (низкой латентностью)

и

-- системы с гарантированной производительностью

[Leka 1]

Экспертные системы к какому типу отнести?

[CaPpuCcino 0]

-- системы с быстрым откликом (низкой латентностью)

и

-- системы с гарантированной производительностью

1) что-то вроде того

2) не подойдёт, т.к. не понятно что именно считать производительностью (количество откликов за единицу времени тоже можно считать производительностью)

 

Экспертные системы к какому типу отнести?

экспертные системы не нужно ни к какому типу относить, потому как это тип приложения, а не тип вычислительной системы (всё будет зависеть от способа реализации)

 

PS: хочу попросить постить советы по control/data-domnated systems в топике указанном по ссылке, иначе мешанина получится

[avesat 0]

... Verification_RUS.pdf

Если статья еще дорабатывается, хотелось бы увидеть общий рисунок к ней :rolleyes:

[CaPpuCcino 0]

Если статья еще дорабатывается, хотелось бы увидеть общий рисунок к ней :rolleyes:

вы имеете ввиду план всей статьи?

Методология проектирования систем на ПЛИС

1.Общий взгляд на процесс проектирования: моделирование, имплементация, верификация (3 стр.)

2.Моделирование

2.1 Статические и динамические модели (1 стр)

2.2 Уровни абстракции моделей (1 стр)

2.3 Уточнение моделей (0,5 стр)

2.4 Моделирование на уровне транзакций TLM (1 стр)

2.5 Анализ моделей (1 стр)

3. Имплементация (3 стр)

4. Верификация

4.1 Функциональная верификация (2 стр)

4.2 Верификационный план (2 стр)

4.3 Формальная верификация (0,5 стр)

4.4 Динамическая верификация (3 стр)

4.5 Спецификация свойств (1 стр)

4.6 Инфраструктура верификационной среды (2 стр)

4.7 Открытые верификационные библиотеки (0,5 стр)

4.7 Временная верефикация (0,5 стр)

5. Языки спецификации, описания и верификации аппаратуры(1 стр)

 

ЗЫ: вообще не понял, что такое "общий рисунок к ней"