Перейти к содержанию
    

Языки описания свойств аппаратуры

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

 

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

 

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

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

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

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

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

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

 

Языкам описания свойств присуще принципиально иной более абстрактный уровен определения поведения системы и её компонентов относительно друг-друга нежле языкам описания аппаратуры. Базовыми понятиями ЯОСА является последовательность (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: прошу не сильно критиковать за приведённые примеры, я ещё плохо пишу на ЯОСА и может что-то неправильно закодировал. однако исправления приветствуются :)

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

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

 

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

 

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

 

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

 

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

 

Удачи!

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

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

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

 

Очень интересует эта тема. Хотелось бы прочесть Ваше мнение о перспективах

использования различных языков и соответствующих программных средств в

практической работе. Может быть, будет возможность создать в разделе /doc

закромов коллекцию доступной документации и литературы по теме?

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Очень интересует эта тема. Хотелось бы прочесть Ваше мнение о перспективах

использования различных языков и соответствующих программных средств в

практической работе. Может быть, будет возможность создать в разделе /doc

закромов коллекцию доступной документации и литературы по теме?

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

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

 

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

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

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

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

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

 

Спасибо! Скажите, пожалуйста, какие программные средства

стоит использовать - Questa ,VCS , IUS или нет существенной

разницы?

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Спасибо! Скажите, пожалуйста, какие программные средства

стоит использовать - 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

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

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

 

по поводу построения тестбенчей на основе 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

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

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

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

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

Книги из вашего списка также обсуждаются там.

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

пара приятных ссылочек по SVA:

http://www.electrosofts.com/systemverilog/assertions1.html

http://www.doulos.com/knowhow/sysverilog/t...ial/assertions/

(в последней есть также и тьюториал по PSL)

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

неплохие видео тьюториалы

http://www.demosondemand.com/dod/indorgs/accellera.aspx

(регистрация не автоматическая, так что придётся некоторое время подождать)

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Собрал всю доступную информацию на ФТП по адресу /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

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

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

 

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

 

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

 

На моей памяти есть только одна статья, посвященная АБВ (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

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Присоединяйтесь к обсуждению

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

Гость
Ответить в этой теме...

×   Вставлено с форматированием.   Вставить как обычный текст

  Разрешено использовать не более 75 эмодзи.

×   Ваша ссылка была автоматически встроена.   Отображать как обычную ссылку

×   Ваш предыдущий контент был восстановлен.   Очистить редактор

×   Вы не можете вставлять изображения напрямую. Загружайте или вставляйте изображения по ссылке.

×
×
  • Создать...