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

[CaPpuCcino]

Лично у меня есть заинтересованность в применении языков описания свойств аппаратуры (ЯОСА) для проектирования на ПЛИС. Сам я несколько лет назад ознакомился с данными языками, но отсутствие доступных инструментов для их использования при проектировании и, как следствие, практических навыков применения, не позволило мне в полной мере овладеть данной технологией. Более того, существенная разница понятий языков описаний свойств и традиционных языков программирования и проектирования затрудняет понимание и корректное использование ЯОСА.

В последние годы с интеграцией данной технологии в наиболее популярные среды моделирования, а также объединение языков описания аппаратуры с верификационными и спецификационными языками (интеграция PSL в VHDL; свойства, утверждения и покрытие в SystemVerilog), этот экзотический инструмент(ЯОСА) стал доступен большому кругу разработчиков. В то же время в российском сегменте сети информация по данной технологии практически отсутствует, что препятствует популяризации оной в нашей стране. Хотелось бы исправить этот досадный недочёт и надеяться, что участники форума разделят моё желание.

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

[RHnd]

Если не сложно, то можно для совсем не понимающих, но учащихся, объяснить, о чем идет речь? Для затравки. Т.е. чем ЯОСА отличается от HDL?

[CaPpuCcino]

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

Языкам описания свойств присуще принципиально иной более абстрактный уровен определения поведения системы и её компонентов относительно друг-друга нежле языкам описания аппаратуры. Базовыми понятиями ЯОСА является последовательность (sequence), свойство(property), утверждение(assertion) и покрытие(coverage).

Последовательность - это описание последовательности систояний системы. Например: data_request ## 2 channel_grant ## 4 data_acknowledged описывает следующую посленовательность систояний - после того как выражение data_request истинно через 2 такта выражение channel_grant истинно после чего выражение data_acknowledged истенно через 4 такта, при этом временные отношения могут быть и плавающими (например ##[2:5] означает "от 2 до пяти", [*1:$] один и более раз до бесконечности(конца симуляции для динамический сред), и так далее). Последовательности могут быть произвольной длинны включая вложенные и единичные.

Свойство - это описание логических отношений между последовательностями. Так например: data_request |=> !data_grant[*4] описывает отношение "в случае установления сигнала(выражения) data_request, data_grant не может быть истинно в течение 4 циклов"; или request |-> ##[1:100] grant означает, что если request истина, то grant должен быть установлен не позднее чем через 100 циклов (в обоих примерах мы имеем свойство описывающее импликацию последовательностей единичной длинны).

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

Код

    property source_register_overwtire_before_cannel_forwarding;
        @(posedge clk) disable iff (!reset_n) (register_valid && !channel_grant) ##1 ( register_valid && !channel_grant ) |-> (data_registered==$past(data_registered));
    endproperty
            
    assret property source_register_overwtire_before_cannel_forwarding
                else $error("Данные в регистре были изменены до принятия их в канал данных");

Само свойство означает, что если установлен флаг действительности данных в регистре, но канал данных не подтверждает их захват и в следующем такте состояние системы не изменилось(комбинация флагов), то данные в регистре остаются неизменными по отношению с предыдущим тактом. Утверждение в свою очередь проверяет не были ли перезаписаны данные в регистре до того как они были продвинуты в канал данных. Если подобное произошло сообщаем об ошибке. Такая короткая запись свойства может сослужить хорошую службу при дальнейшей верификации системы. Ведь если запрос на запись в канал можно напрямую привязать к флагу register_valid, то логика записи в регистр может быть довольно сложной (например несколько источников с разными приоритетами), и правильность функционирования схемы записи в этот регистр может быть неочевидной. Если предположить, что подобная ошибка была допущена и наш канал используется как строительный блок большой системы, то на этапе её верификации будет очень сложно определит причину некорректного функционирования целой системы. Это потребует многие часы, а то и дни анализа проекта. В то же время использование свойств (ЯОСА) позволит мгновенно локализовать ошибку.

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

Синтаксис ЯОСА встроен в современные HDVSLи (Hardware Descriprion Verification and Specification Language) такие как SystemVerilog и новый VHDL.

NB: прошу не сильно критиковать за приведённые примеры, я ещё плохо пишу на ЯОСА и может что-то неправильно закодировал. однако исправления приветствуются

[des00]

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

Ну если уж на то пошло, то

1. нужно прикрепить тему к топу. что бы не уехала.

2. запостить туда линки на темы с уже рассмотренными вопросами.

ЗЫ. сделать еще можно пару статей, но вот кто это будет делать вопрос......

Удачи!

[Кнкн]

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

Очень интересует эта тема. Хотелось бы прочесть Ваше мнение о перспективах
использования различных языков и соответствующих программных средств в
практической работе. Может быть, будет возможность создать в разделе /doc
закромов коллекцию доступной документации и литературы по теме?

[CaPpuCcino]

Очень интересует эта тема. Хотелось бы прочесть Ваше мнение о перспективах
использования различных языков и соответствующих программных средств в
практической работе. Может быть, будет возможность создать в разделе /doc
закромов коллекцию доступной документации и литературы по теме?

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

ЗЫ. сделать еще можно пару статей, но вот кто это будет делать вопрос......

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

[Кнкн]

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

Спасибо! Скажите, пожалуйста, какие программные средства
стоит использовать - Questa ,VCS , IUS или нет существенной
разницы?

[CaPpuCcino]

Спасибо! Скажите, пожалуйста, какие программные средства
стоит использовать - Questa ,VCS , IUS или нет существенной
разницы?

у меня например, выбора нет - использую лицензионную Questa

кое-что из литературы:
1) http://electronix.ru/forum/index.php?showtopic=43844 (больше концепция использования)
2) "Asserton-Based Design" Х.Фостер Ф.Крольник 2004 (PSL,SV,OVL; в закромах)
3) очень хорошо свойства описаны в самом стандарте SV
4) mentorpaper_20860 сравнение PSL и SV
5) mentorpaper_23353 сравнение OpenVera и SV

[Кнкн]

кое-что из литературы:

Спасибо!

[lotorev]

Извините, если не в тему.

по поводу построения тестбенчей на основе SV, SystemC.
1. По данной теме есть бесплатная книга от Mentor AVM Cookbook for SystemVerilog & SystemC 3.0-Update-3. ( http://www.mentor.com/products/fv/_3b715c/index.cfm )
2. http://www.ovmworld.org/ - mentor (Advanced Verification Methodology (AVM) ) объединились с cadence (Universal Reuse Methodology (URM)) для построения новых принципов построения тестбенчей. совсем недавно January 9. 2008 вышла первая версия пакета классов. Тоже бесплатно, по лицензии apache2.0.
2.1. простенький туториал по ovm можно найти здесь http://www.doulos.com/knowhow/sysverilog/ovm/

OVM, кстати, ссылается только на IEEE 1800 SystemVerilog и следующие проги Cadence’s Incisive и Mentor Graphics’ Questa Verification Platform

Личные комментарии отсутствуют, т.к. только начал активно изучать.

По systemverilog имеются следующие книги. Могу выложить....
* Janick Bergeron - Writing Testbenches using SystemVerilog - Bergeron.pdf
* Chris Spear - SystemVerilog for Verification.Guide to testbenches.pdf
* Stuart Sutherland - SystemVerilog For design - A guide to using SystemVerilog for Hardware design and modeling, 2nd Edition.pdf
* Janick Bergeron - Verification Methodology Manual for SystemVerilog - Bergeron 2005.pdf
* SystemVerilog_3.1a - LRM.pdf
* Stuart Sutherland - SystemVerilog For design - A guide to using SystemVerilog for Hardware design and modeling.pdf

Сообщение отредактировал lotorev - Mar 7 2008, 20:24

[CaPpuCcino]

Извините, если не в тему.
по поводу построения тестбенчей на основе SV, SystemC.

действительно немного промазали эти вопросы обсуждаются в соседней ветке в шапке подфорума "Языки проектирования на ПЛИС" (перейти в топик Документация на SystemVerilog)
Книги из вашего списка также обсуждаются там.

[CaPpuCcino]

пара приятных ссылочек по SVA:
http://www.electrosofts.com/systemverilog/assertions1.html
http://www.doulos.com/knowhow/sysverilog/t...ial/assertions/
(в последней есть также и тьюториал по PSL)

[CaPpuCcino]

неплохие видео тьюториалы
http://www.demosondemand.com/dod/indorgs/accellera.aspx
(регистрация не автоматическая, так что придётся некоторое время подождать)

[makc]

Собрал всю доступную информацию на ФТП по адресу /pub/DOC/Books/Assertion Based Verification, а именно:

Assertion_Based_design.pdf
Esperan_PSL
Foster_Krolnik_Creating_Assertion_Based_IP.pdf
PSL By Example.pdf
PSL-v1.1.pdf
PSL_quickrefvhdl.pdf
psl_vs_sva.pdf

./Esperan_PSL:
esperan_introduction_to_psl.pdf
esperan_psl_1-1_tutorial.pdf
esperan_psl_tutorial.pdf

[maksya]

Попробую внести свою лепту в борьбу за построение электротехнического коммунизма =)

Начнем с родного языка.

ЗЫ. сделать еще можно пару статей, но вот кто это будет делать вопрос......

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

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

Теперь по первоисточникам...

Помимо упомянутых в топике источников хотелось бы отметить книгу "The Design Warrior's Guide to FPGA" by Clive Maxfileld (тем, кому чужда аглицкая речь, можно прочитать то же самое на русском - "Проектирование на ПЛИС. Курс молодого бойца."). Книга достойна прочтения (IMHO) от корки до корки, но конкретно для рассматривамой темы будет интересен раздел "Формальная верификация" в главе 19.

Более специализированная литература - Ben Cohen, Srinivasan Venkataramanan, Ajeetha Kumari. Using PSL/Sugar for Formal and Dynamic Verification 2nd Edition. VHDLCOHEN Publishing, 2004. К сожалению, в отличии от предыдущего опуса, в электронном варианте видимо не распространяется =( Но некоторые страницы можно почитать на print.google.com

Кстати о старине Ben'е. Он состоит в гильдии по верификации под партийным псевдонимом vhdlcohen - www.verificationguild.com. Куда я советую вступить всем интересующимся. Членские взносы отсутствуют =)

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

 Assertion_Based_Verification.pdf ( 119.7 килобайт ) Кол-во скачиваний: 720

 

[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(хотя конечно и здесь не всё так безоблачно - о проблемах новых стандартов можно посмотреть в сообв. ветках нашего форума)/)

с уважением

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

[warrior-2001]

Доброго времени суток. Возникли вопросы: А проверил ли кто на практике утверждение о том, что после создания первого проекта средствами OVM дальнейшие проекты пойдут как по маслу? Примеры есть?
Может кто в курсе, планируется ли поддержка графики для SystemVerilog? Ведь без графики тяжело работать с масштабными проектами. Если кто даст ссылку на серьёзные проекты, собранные согласно OVM буду признателен.

Сообщение отредактировал warrior-2001 - Oct 9 2008, 06:35

[CaPpuCcino]

А проверил ли кто на практике утверждение о том, что после создания первого проекта средствами OVM дальнейшие проекты пойдут как по маслу?

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

Может кто в курсе, планируется ли поддержка графики для SystemVerilog?

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

[des00]

помоему кто то перепутал OVM c OVL

[warrior-2001]

OVL может быть и небольшая библиотека, а вот методологию менторс каденс завернули приличную, не уступаем VMM. Ситуация такова, что работать приходится в среде FPGA advantage, а работу с OVM поддерживает только questa. Посему и вопрос - как бы взаимно интегрировать questa и FPGA advantage так, чтобы все эти чеккеры, мониторы и секвенсоры из OVM работали в HDL Designer.
Для этой же цели интересуют рабочие проекты с приминением методологии OVM.

[CaPpuCcino]

помоему кто то перепутал OVM c OVL

извините - не выспался

[des00]

Для этой же цели интересуют рабочие проекты с приминением методологии OVM.

эта тема все таки про языки описания свойств (PSL, SVA, OVL и т.д.) обсуждение OVM идет в другом месте

http://electronix.ru/forum/index.php?showt...mp;#entry488929

[CaPpuCcino]

тьюториал по SVA http://testbench.in/tAS_00_INDEX.html (не самый лучший, что я видел, но для начального ознакомления с концепцией пойдёт. внимание: на данный момент есть некоторые синтаксические ошибки, напр. в разделе Properties неправильно обозначено неперекрывающая импликация как ||->, вместо |=>)

[CaPpuCcino]

хотелось бы ещё отметить одну книжку напрямую не связанную с языками описания свойст, но дающую хорошие советы о том как нужно писать свойства и что самое главное как не нужно их писать. это материал не для начинающих так, что советую обратится к нему после того как вы уже попробовали на практике применять языки описания свойств. книга Бегрерона VerificationMethodology Manual for SystemVerilog Глава 3 Assertions (обратите внимание на раздел Assertion Coding Guidlines и далее до конца главы)

[Escorial]

Maksya, в своей статье Вы ссылаетесь на книжку vhdl_cohen, нет ли у Вас ее в электронном виде и не могли бы вы ее выложить на фтп?

По поводу статьи, мне кажется в ней есть фактическая неточность - PSL состоит из 2х частей - базиса (LTL-логика), и т.н. Optional Branching Extensions (CTL).

Если сравнивать PSL и SVA, мне кажется в плане функционала выигрывают последние, т.к. позволяют использовать методологию coverage driven verification (т.е. когда определенная контрольная точка функционального покрытия выполнена, прекращаем формировать рандомные пакеты для заданного блока). Т.е имеем двунаправленную интеграцию формальные утверждения <-> тестбенч. В PSL можем гнать данные только в 1 конец.

Кто-то интересовался синтезом ассертов, если коротко любая LTL-формула может быть представлена в виде автомата Бюхи. Есть САПРы которые синтезируют ассерты в виде некоторого блока, вставляемого в RTL, что позволяет их использовать в FPGA любого производителя. Контроль идет через специальный отладочный порт а-ля JTAG и спецсофт компании-разработчика. Посмотрите например, Dialite от Temento Systems.

[Poluektovich]

Как на сегодняшний день обстоят дела с использованием ЯОСА и тулов для статической формальной верификации?
Появившиеся материалы:
SystemVerilog утверждения для верификации и имитационного моделирования
The Power of Assertions in SystemVerilog

[Poluektovich]

У меня по поводу тулов еще вопрос возник. Questa Formal (0-in formal) кто-нибудь использовал? В закромах этот пакет мне удалось найти...

[yes]

У меня по поводу тулов еще вопрос возник. Questa Formal (0-in formal) кто-нибудь использовал? В закромах этот пакет мне удалось найти...

доступно formality от синопсиса. этот 0-in formal очень рекламируется Ментором, но чтоб его где-то использовали - не слышал
пользуют либо формалити либо конформал от каденса.

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

а вообщето тулзы формальной верификации слегка не для этого
http://www.synopsys.com/Tools/Verification.../Formality.aspx
http://www.cadence.com/products/ld/equival...es/default.aspx

[Poluektovich]

yes, приведенные вами примеры тулов используются для Logic Equivalence Checking.

Формальной верификацией еще называют статическую функциональную верификацию, которая ощуствляется c помощью эвристических алгоритмов без написания тестбенчей и динамического моделирования. Пишутся assertions, задаются constraints для снижения сложности анализа. По результатам выполнения assertions и анализу покрытия делаем вывод о правильности работы блока и полноте тестирования.

Тулы:
http://www.mentor.com/products/fv/0-in_fv/
http://www.synopsys.com/Tools/Verification...s/Magellan.aspx
http://www.cadence.com/products/fv/formal_...es/default.aspx

[warrior-2001]

У меня по поводу тулов еще вопрос возник. Questa Formal (0-in formal) кто-нибудь использовал? В закромах этот пакет мне удалось найти...

Опыт работу есть. Что именно интересует?
Такого рода формальная верификация подходит, если на нее затачиваться с самого начала. К примеру поддержку любого сложного интерфейса проверяют всегда в первую очередь. А для математических блоков использование данного подхода неэффективно.

[Poluektovich]

Доброе время суток.

warrior-2001, делали ли вы оценку покрытия и какие цифры удавалось?
Математический блок внутри контроллера жизнь тоже осложнил в таком подходе, здесь эталонная поведенческая модель нужна.

Платформой Questa мы не пользуемся, но он интересен наличием библиотеки QVL.
Cadence предлагает в своем портфолио ABVVIP для системных шин AMBA/OCP и контроллеров памятей, остальные VIP только для динамики. В библиотеке QVL имеется хороший набор последовательных интерфейсов.
Если проверяли последовательные интерфейсы каких усилий стоит получение статусных состояний по всему набору утверждений? Использовалась ли гибридная верификация (формальный анализ + динамическая симуляция)?

[warrior-2001]

Доброе время суток.

warrior-2001, делали ли вы оценку покрытия и какие цифры удавалось?
Математический блок внутри контроллера жизнь тоже осложнил в таком подходе, здесь эталонная поведенческая модель нужна.

Платформой Questa мы не пользуемся, но он интересен наличием библиотеки QVL.
Cadence предлагает в своем портфолио ABVVIP для системных шин AMBA/OCP и контроллеров памятей, остальные VIP только для динамики. В библиотеке QVL имеется хороший набор последовательных интерфейсов.
Если проверяли последовательные интерфейсы каких усилий стоит получение статусных состояний по всему набору утверждений? Использовалась ли гибридная верификация (формальный анализ + динамическая симуляция)?

Если честно - мне результаты не понравились. И проблема именно в трудозатратах. Дело в том, что для формальной проверки проект должен быть изначально на это ориентирован. И когда в компании уже есть большое кол-во СФ блоков, разработанных и отлаженных ранее, то когда они вставляются в проект - они выпадают из области покрытия и результирующие цифры уж очень не красивые. Если же тестировать отдельно СФ блок - то в большинстве случаев удается проверить его работу так сказать по полному графу. То есть перебрать весь набор входных воздействия и сравнить с эталоном.
На мой взгляд - использование формальной верификации оправдано, если разработка ведется с системного уровня.
По поводу гибридной верификации - мы пишем тестовые окружения на SV и занимаемся верификаций в QuestaSim. Отдельно моделировать проекты смысла нет.

[radigast]

Приветствую коллег в этой ветке!

С момента последнего сообщения прошло уже 4 года, за это время тулы и методики формальной верификации заметно подросли. В этой связи позволю себе освежить тему вопросом по статусу практического опыта использования формальных методов верификации.
Если использованием ABV в динамике сейчас никого не удивишь (SVA/OVL активно используются), то вот про опыт промышленного применения формальных подходов слышно не так часто.
Последний раз, когда мы пробовали на базе ABV формально верифицировать блоки сложнее АЛУ натыкались на логичную проблему комбинаторного взрыва. Чтобы процесс сошёлся при жизни запускающего его инженера требовалось задавать слишком уж жёсткие ограничения, что негативно сказывается на достигаемом покрытии.
Собственно вопрос (если не секрет): именно в «боевых» проектах блоки какой сложности удавалось проверить формально на базе ABV/model checking, какие тулы при этом использовались (может у кого есть опыт работы с теми же ABVVIP от Cadene?)

[Poluektovich]

НИИСИ использовали Jasper для проверки connectivity на системном уровне, регистрового пространства.
см JasperGold Applications Approach for Verification Workflow of SRISA Project

[radigast]

НИИСИ использовали Jasper для проверки connectivity на системном уровне, регистрового пространства.
см JasperGold Applications Approach for Verification Workflow of SRISA Project

Да, мы видели такое приложение (APP как они его называют). Но на мой скромный взгляд это самое тривиальное из того что можно доказать формально, собственно поэтому вопросов к работоспособности и масштабируемости именно этого приложения практически нет. А вот случаи посложнее, типа доказательства соответствия RTL реализации заданному протоколу для всех возможных воздействий, такой уверенности пока не вселяли. Подозреваю, что там есть множество ограничений.
Более того, приложение проверки коннективити, насколько я понял (если не прав - поправьте), использует сторонний файл с описанием требуемой карты связности (который создаётся ручками). В таком случае от двойной ошибки и в списке связности и в RTL вызванной непониманием особенностей взаимодействия блоков страховки все равно нет. Ещё один момент — текущий уровень автоматизации создания систем. Многие блоки сейчас поставляются с IP-XACT ( ссылка_ip_xact) описанием, в котором, в том числе возможно функциональное объединение пинов в интерфейсы, которые на системном уровне подключаются друг у другу автоматически. Современные средства сборки СнК позволяют задавать каркас будущей системы, её карту памяти и теоретически такая система в части связности должна быть корректна от рождения. Во всяком случае серьёзных проблем именно с картой памяти или подключением стандартных интерфейсов в таких системах я не помню. Т.е. приложение то рабочее, но не самое эффектное с точки зрения влияния формалки на маршрут верификации.

На прошедшей в 2016 году конференции МЭС была целая секция посвящённая функциональной верификации, на которой в том числе обсуждались и теоретические аспекты формальной верификации (МЭС. расписание секции функциональной верификации). Один из орг выводов — русскоязычного сообщества верификаторов пока нет, а в силу скорости развития этого направления лучше держаться вместе.
Данный форум — это площадка для живого обсуждения практических вопросов и обмена материалами и мнениями. Кроме того мы создали на FaceBook группу с пафосным названием «Российское сообщество верификаторов» (ссылка на группу). Пока она работает в режиме новостной ленты с информацией о научных и практических конференциях или событиях, связанных с функциональной верификацией. Если у кого есть интерес — подписывайтесь.

[Мур]

спешите!!!!
Вот учебник по параллельному программированию ПЛИС

https://arxiv.org/abs/1805.03648