Языки описания свойств аппаратуры, PSL/Sugar, SystemVerilog, OVL Опции

[CaPpuCcino]

Кроме того, в ближайшее время в КиТе выйдет результат моих собственных изысканий на тему PSL под рабочим названием "Проектирование в условиях временных ограничений: верификация проектов".

ждем с нетерпением. пожалуйста, сообщите о наступлении ближайшего времени.

На моей памяти есть только одна статья, посвященная АБВ (ABV): Долинский М. Assertion Based Verification – верификация, основанная на утверждениях // Компоненты и технологии. № 9. 2004.

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

[des00]

2 maksya

с удовольствием ознакомлюсь с вашими статьями, иногда приятного быть рецензором %)) (ломать не строить).

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

Сложилось впечатление что человек сам не работал с данными технологиями, а надергал общих фраз из различных материалов(причем ИМХО не очень хороших). Те же SVA хорошо и более понятно расписаны в самом стандарте на который он ссылается, причем с примерами и рисунками.

ИМХО статья для манагеров, а не для разработчиков.

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


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

Насчет источников рассмотрите еще книгу
Ben Cohen, Srinivasan Venkataramanan, Ajeetha Kumari, "SystemVerilog Assertions
Handbook … for Formal and Dynamic Verification", Vhdlcohen Publishing.

К сожалению в моей коллекции ее нет, может быть кто нибудь поделиться ?

[maksya]

пожалуйста, сообщите о наступлении ближайшего времени.

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

Не подскажите "Проектирование на ПЛИС. Курс молодого бойца." в электроном виде где можно взять посмотреть ?

Я брал здесь - http://mirknig.com/2007/09/01/proektirovan...ogo_bojjca.html
Если возникнут сложности с пропиской (или просто лениво регистрироваться), то могу перезалить на FTP.

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

По мне, так книга ценна именно системным подходом к проблеме. А приставка "Курс молодого бойца" как раз и указывает на целевую аудиторию.

[Doka]

а вот на счёт мнения о перспективах использования я не понял. вы именно о языках свойств говорите? тогда тут совершенно определённо PSL и SV, т.к. OVL себя уже изжил.

OVL == OpenVera Language
или
OVL == Open Verification Library
???



(последнее я так понимаю довольно активтино развивает Accellera)

[CaPpuCcino]

OVL == OpenVera Language
или
OVL == Open Verification Library
???
(последнее я так понимаю довольно активтино развивает Accellera)

Open Verification Library. Здесь вы меня поставили в тупик. Дело в том, что изначально OVL (абревиатура настолько приелась, что её никто не произносил полностью, хотя расшифровывается точно так же) была библиотекой мониторов написаной на языке Verilog (со всеми недостатками такого подхода). Я слышал о современной Open Verification Library (как высокоуровневой библиотеке чекеров), но думал что это случайное совпадение названий, а сейчас посмотрел и увидел, что это продолжение преждней идеи.
В общем, извините. Спасибо, что обратили внимание.

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

Сложилось впечатление что человек сам не работал с данными технологиями, а надергал общих фраз из различных материалов(причем ИМХО не очень хороших). Те же SVA хорошо и более понятно расписаны в самом стандарте на который он ссылается, причем с примерами и рисунками.

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

[maksya]

На правах саморекламы =)

Сегодня окончательно согласовали верстку. Статья по PSL должна появиться в пятом номере журнала "Компоненты и технологии". В силу обязательств перед редакцией, выложить в общий доступ электронную версию пока к сожалению не могу...

[des00]

На правах саморекламы =)

Сегодня окончательно согласовали верстку. Статья по PSL должна появиться в пятом номере журнала "Компоненты и технологии". В силу обязательств перед редакцией, выложить в общий доступ электронную версию пока к сожалению не могу...

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

Меня интересует вот какой вопрос : затрагиваете ли вы, в ваших статьях, вопросы синтеза ассертов ? После курения раздела VMM -> CHAPTER 7 ASSERTIONS FOR FORMAL TOOLS и описания техники разработки синтезируемых ассертов я и как то потерялся в этой теме.

Хотелось бы внести ясность.

Что происходит с синтезируемыми ассертами, после того как мы проходим формальные проверки ? Они остаются в коде ? Если да, то тогда как все это влияет на ресурс и производительность результирующего кода ? Ведь макросами/тегам синтеза тут уже не отделаешься.

Спасибо.

[maksya]

Меня интересует вот какой вопрос : затрагиваете ли вы, в ваших статьях, вопросы синтеза ассертов ? После курения раздела VMM -> CHAPTER 7 ASSERTIONS FOR FORMAL TOOLS и описания техники разработки синтезируемых ассертов я и как то потерялся в этой теме.

Боюсь Вас разочаровать, но статья носит скорее ознакомительный характер, нежели описание результатов практического применения... На данном этапе ставилась цель привлечь интерес к PSL. Что касается синтезируемости утверждений, то данный вопрос еще не в полной мере мной изучен. Думаю в ближайшее время можно будет обсудить эту тему в данном форуме.

[CaPpuCcino]

тьюториал по SVA на asic-world
http://www.asic-world.com/systemverilog/assertions.html

[maksya]

С небольшой задержкой, но все-же =) Статья посвящена открытой библиотеке верификации OVL. Опубликована в журнале "Компоненты и Технологии" (www.kit-e.ru).

Любые конструктивные замечания или комментарии приветствуются!

Прикрепленные файлы

 OVL__part_1_.pdf ( 340.34 килобайт ) Кол-во скачиваний: 537
 OVL__part_2_.pdf ( 170.3 килобайт ) Кол-во скачиваний: 495

 

[maksya]

Prequel about PSL:

Прикрепленные файлы

 PSL.pdf ( 113.74 килобайт ) Кол-во скачиваний: 388

 

[des00]

С небольшой задержкой, но все-же =) Статья посвящена открытой библиотеке верификации OVL. Опубликована в журнале "Компоненты и Технологии" (www.kit-e.ru).

Любые конструктивные замечания или комментарии приветствуются!

Если вам интересно мое мнение, то :

часть 1 мне показалась излишне перегруженной кодом. Отрадно конечно что вы не копируете верилоговские описания примеров, а делаете свои собственные на вхдл, но 2 из 5 ти страниц статьи занятых кодом ИМХО это слишком. Лучше дайте тогда уж ссылки на вашу вхдл версию, а в статье оставьте только ключевые моменты. Ну и на сайте верилог пример бы не помешал.

часть 2 мне понравилось как написана, кроме последнего раздела "Некоторые современные тенденции развития языков описания и верификации аппаратуры". Этот раздел дан как то скомкано и сильно поверхностно, особенно что касается верификационых возможностей System Verilog.

Prequel about PSL:

Статья про PSL хорошо написана, но начиная со страницы №3, параграф "Определения и структура языка" текст стал "резать меня по ушам".

Насколько я помню из курса в универе и прочитанных книг раздел математики называется
"Булева алгебра", а не "Булевская алгебра". И многочисленные фразы в тексте вида "булевских выражений", звучат как то не так. Да при топорном переводе с английского "boolean equation", так и подмывает сказать булевское выражение но ИМХО это не верно и не должно идти в печатные издания.

Возможно я ошибаюсь и более опытные товарищи меня поправят.

И чем вам не угодило слово "логический", в том же перечислении уровней :

Структурно язык PSL разбит на 4 четко выраженных уровня:
булевский уровень (boolean layer);
временной уровень (temporal layer);
уровень верификации (verification layer);
уровень моделирования (modeling layer).

ИМХО тут более красиво и правильно было бы использовать "логический уровень", "уровень описания логики" и т.д.

потом вы сначала называете третий уровень как "уровень верификации", а потом описываете его в разделе "Верификационный уровень". Такие явные косяки ИМХО подчеркивают неаккуратность и спешку в подготовке материала.

Удачи!!!

[maksya]

Такие явные косяки ИМХО подчеркивают неаккуратность и спешку в подготовке материала.

Про спешку это Вы верно подметили. Написание статей не является моим основным занятием. А та часть свободного времени, которая обычно отводится для журналистских практик, не всегда соответствует установленным редакцией срокам =) Про неаккуратность позволю себе не согласиться, т.к. я весьма добросовестно отношусь к любой выполняемой работе.

Насколько я помню из курса в универе и прочитанных книг раздел математики называется
"Булева алгебра", а не "Булевская алгебра". И многочисленные фразы в тексте вида "булевских выражений", звучат как то не так. Да при топорном переводе с английского "boolean equation", так и подмывает сказать булевское выражение но ИМХО это не верно и не должно идти в печатные издания.

Я готов компетентно вести беседу о правилах написания фамилии "Михайлов" во всех ее склонениях, а также последующих словообразованиях. Однако не возьмусь обсуждать лингвистическую корректность названия систем созданных Булем. Хотя некоторые размышления на эту тему пожалуй опубликую здесь.

Есть такая порода собак - питбуль (pit bull). По стечению обстоятельств слово "буль" в собачей породе совпадает и по написанию и по звучанию с фамилией математика (после руссификации). И мне кажется что, например, выражение "питбулевский хвост" окажется более жизнеспособным нежели "питбулев хвост". Почему правила языка трактуют иначе в случае Буля - для меня вопрос.

На ум приходит также, например, выражение "пулитцеровская премия", основой для пораждения которого являлась фамилия Пулитцер. "Пулицерова премия" возможно тоже будет резать слух журналистам =)

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

Скорее всего Вы правы в том, что выражение "булева" алгебра более распространено, чем "булевская". Интернет-поисковики подтверждают это. В дальнейшем пожалуй буду придерживаться мнения большинства в этом вопросе, дабы скрыть свою безграмотность. А точность перевода пускай останется на совести составителей курсов и книг по математике, а также выпускающих их редакторов.

потом вы сначала называете третий уровень как "уровень верификации", а потом описываете его в разделе "Верификационный уровень".

Фразы "уровень верификации" и "верификационный уровень" считаю синонимичными.

Большое спасибо за замечания!

[CaPpuCcino]

Скорее всего Вы правы в том, что выражение "булева" алгебра более распространено

верно, там где есть устоявшаяся терминология лучше её придерживаться

Фразы "уровень верификации" и "верификационный уровень" считаю синонимичными.

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

[CaPpuCcino]

Статья посвящена открытой библиотеке верификации OVL.

несмотря на то, что всем известно, что форум - место выражения личных взглядов на тот или иной вопрос, хочу во избежании умаления значения труда авторов данной статьи ещё раз подчеркнуть, что выражаю своё видение данного вопроса и не претендую на безапеляционность моих высказываний.
сейчас наконец-то добрался до статьи по OVL и имею ряд возражений (как поверхностные, так и более принципиальные; - группировать их по данным критериям не буду, а изложу в хронологическом порядке).
№6 2008:
стр. 54. вступление: если говорить о библиотеках верификации, то OVL не единственная подобная библиотека
стр. 57 "Поддержка САПР": "Одним из доказательств простоты применения средств OVL в сравнении с языком PSL является поддержка САПР" - не стоит забывать, что OVL - это всего лишь библиотека предназначенная для верификации РТЛ-уровневых проектов. Так как наиболее популярными ЯОА являются VHDL и Verilog(SV), данная библиотека имеет интерфейс написаный на этих двух языках. Сама же библиотека реализована на нескольких языках(стандартах) - Verilog 1995, SV-2005, PSL-2005, VHDL-1993. При этом наименьшее число мониторов реализовано именно на VHDL-1993(20% от общего числа мониторов), затем Verilog-1995 (65%; OVL изначально писался на Verilog-e ещё во времена зараждения специализированных верификационных языков)и PSL-2005 (тоже 65%), и наконец SV-2005 (100%).
ЗЫ: стоит также отметить, что использование реализаций OVL не на языках с верификационной направленностью (т.е. реализации на VHDL и Verilog-95) существенно снижает производительность симулятора относительно верификационно заточеных языковых реализаций SV-2005,PSL-2005
№8 2008:
стр. 38 "Некоторые современные тенденции развития языков описания и верификации аппаратуры": "Поэтому и получили определённое распространение языки, специализирующиеся исключительно на проблемах верификации. Как уже отмечалось ранее, среди этих языков наибольшие шансы на выживание имел язык PSL" - вот как бы это сказать помягче... ... конечно это не суть принципиально, но дело в том, что PSL это всего лишь язык для формального описания свойств - это описание свойств конечно же служит инструментарием в процессе верификации, но это всего лишь один из инструментов и совершенно не универсальный. Вот например язык "Vera" и язык "e" - это HVLs (hardware verification languages), но они совершенно не претендуют быть языками утверждений(более того SystemVerilog=Vera+Verilog+"assertions", т.е. синтаксис Веры полностью и практически без изменений присутствует в SV: он туда просто влился). Более того PSL строго говоря не является HVL, а в чистом виде язык утверждений, поэтому он и не мог бы иметь наибольшие шансы на выживание среди языков "специализирующиеся исключительно на проблемах верификации".
стр.38-39. "... языка SystemVerilog. Первым необходимо признать включение в язык элементов объектно-ориентированного программирования и вторым - средств PSL. Включение в состав языка средств PSL..." - ну, во-первых, не включение элементов, а принятия концепции ООП - всё-таки SV - объектно-ориентированный язык (хоть и не программирования), а во-вторых никто в SV средства PSL не включал. SVA (SystemVerilog Assertions) использует концепцию утверждений и описание свойств как и PSL, но говорить о том что SVA=PSL не очень корректно (это сравнимо с сопоставлением Паскаль и Си, с одной стороны это одно и тоже если сравнивать их например с Prolog, но если не выходить за рамки класса императивных языков программирования, то различия между ними становятся существенными). строго говоря PSL обладает более широкими возможностями относительно SVA (статей сравнивающих эти два языка много - ну например http://www.pslsugar.org/papers/pslandsva.pdf, у Менторов вообще есть материалы с таблицами сравнений возможностей/залезьте к ним в библиотеку - регистрация свободная/; более того последующие стандарты имеют тенденцию к расхождению ветвей PSL - SVA, а не наоборот, как это предполагалось на ранних стадиях, хотя и имеют свойства заимствований у друг-друга)
стр. 39 "Однако после появления в 2007 году работы [5] стало понятным, что поистине революционные изменения уже не за горами и для языка VHDL." - ой как ещё и за горами - по сведениям, которые были у меня в начале лета согласия в коммитете так и нет и в 2008 году обновления стандарта ожидать не приходилось (хотя конечно пока я был в отпуске что-то координально и поменялось, но более того) ничего особо революционного в стандарте не намечалось (даже в источнике [5], если вы посмотрите на главу посвящённую тому что ещё предстоит сделать /,чтобы хотябы догнать SV образца 2005 года по возможностям; и даже при этом в 2009 году планируется обновление стандарта SV(хотя конечно и здесь не всё так безоблачно - о проблемах новых стандартов можно посмотреть в сообв. ветках нашего форума)/)

с уважением

ЗЫ: у меня возник ещё небольшой общий вопрос относительно политики журнала - а сколько человек обычно реферируют статью до печати? спасибо