реклама на сайте
подробности

 
 
4 страниц V   1 2 3 > »   
Reply to this topicStart new topic
> Языки описания свойств аппаратуры, PSL/Sugar, SystemVerilog, OVL
CaPpuCcino
сообщение Mar 5 2008, 12:35
Сообщение #1


тоже уже Гуру
******

Группа: Свой
Сообщений: 2 047
Регистрация: 13-06-05
Из: Кёлн - Санкт-Петербург
Пользователь №: 5 973



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

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

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


--------------------
И снова на арене цирка - дрессированные клоуны!! Оказываем консультации по электронике за симпу круглосуточно.
Go to the top of the page
 
+Quote Post
RHnd
сообщение Mar 5 2008, 16:35
Сообщение #2


Знающий
****

Группа: Свой
Сообщений: 518
Регистрация: 12-04-07
Из: Санкт-Петербург
Пользователь №: 26 997



Если не сложно, то можно для совсем не понимающих, но учащихся, объяснить, о чем идет речь? Для затравки. smile.gif Т.е. чем ЯОСА отличается от HDL?
Go to the top of the page
 
+Quote Post
CaPpuCcino
сообщение Mar 5 2008, 18:44
Сообщение #3


тоже уже Гуру
******

Группа: Свой
Сообщений: 2 047
Регистрация: 13-06-05
Из: Кёлн - Санкт-Петербург
Пользователь №: 5 973



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

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


--------------------
И снова на арене цирка - дрессированные клоуны!! Оказываем консультации по электронике за симпу круглосуточно.
Go to the top of the page
 
+Quote Post
des00
сообщение Mar 6 2008, 05:15
Сообщение #4


Вечный ламер
******

Группа: Модераторы
Сообщений: 7 222
Регистрация: 18-03-05
Из: Томск
Пользователь №: 3 453



Цитата(CaPpuCcino @ Mar 5 2008, 07:35) *
Предлагаю сосредоточить в данной теме все вопросы связанные с этими языками, включая обсуждение литературы, синтаксиса, применения.


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

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

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

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

Удачи!


--------------------
Go to the top of the page
 
+Quote Post
Кнкн
сообщение Mar 6 2008, 06:46
Сообщение #5


Знающий
****

Группа: Свой
Сообщений: 633
Регистрация: 21-06-04
Пользователь №: 71



Цитата(CaPpuCcino @ Mar 5 2008, 15:35) *
Предлагаю сосредоточить в данной теме все вопросы связанные с этими языками, включая обсуждение литературы, синтаксиса, применения.
Знаю, что на форуме есть специалисты использующие данные языки в своих проектах. Надеюсь они смогут помочь начинающим в данной области.


Очень интересует эта тема. Хотелось бы прочесть Ваше мнение о перспективах
использования различных языков и соответствующих программных средств в
практической работе. Может быть, будет возможность создать в разделе /doc
закромов коллекцию доступной документации и литературы по теме?
Go to the top of the page
 
+Quote Post
CaPpuCcino
сообщение Mar 6 2008, 13:56
Сообщение #6


тоже уже Гуру
******

Группа: Свой
Сообщений: 2 047
Регистрация: 13-06-05
Из: Кёлн - Санкт-Петербург
Пользователь №: 5 973



Цитата(Кнкн @ Mar 6 2008, 09:46) *
Очень интересует эта тема. Хотелось бы прочесть Ваше мнение о перспективах
использования различных языков и соответствующих программных средств в
практической работе. Может быть, будет возможность создать в разделе /doc
закромов коллекцию доступной документации и литературы по теме?

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

Цитата(des00 @ Mar 6 2008, 08:15) *
ЗЫ. сделать еще можно пару статей, но вот кто это будет делать вопрос......

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


--------------------
И снова на арене цирка - дрессированные клоуны!! Оказываем консультации по электронике за симпу круглосуточно.
Go to the top of the page
 
+Quote Post
Кнкн
сообщение Mar 6 2008, 14:52
Сообщение #7


Знающий
****

Группа: Свой
Сообщений: 633
Регистрация: 21-06-04
Пользователь №: 71



Цитата(CaPpuCcino @ Mar 6 2008, 16:56) *
так не вопрос. несколько книжек я уже вешал, они где-то в закромах болтаются, Gate на днях выкладовал неплохую книжку.
а вот на счёт мнения о перспективах использования я не понял. вы именно о языках свойств говорите? тогда тут совершенно определённо PSL и SV, т.к. OVL себя уже изжил.


Спасибо! Скажите, пожалуйста, какие программные средства
стоит использовать - Questa ,VCS , IUS или нет существенной
разницы?
Go to the top of the page
 
+Quote Post
CaPpuCcino
сообщение Mar 6 2008, 15:53
Сообщение #8


тоже уже Гуру
******

Группа: Свой
Сообщений: 2 047
Регистрация: 13-06-05
Из: Кёлн - Санкт-Петербург
Пользователь №: 5 973



Цитата(Кнкн @ Mar 6 2008, 17:52) *
Спасибо! Скажите, пожалуйста, какие программные средства
стоит использовать - 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


--------------------
И снова на арене цирка - дрессированные клоуны!! Оказываем консультации по электронике за симпу круглосуточно.
Go to the top of the page
 
+Quote Post
Кнкн
сообщение Mar 7 2008, 07:06
Сообщение #9


Знающий
****

Группа: Свой
Сообщений: 633
Регистрация: 21-06-04
Пользователь №: 71



Цитата(CaPpuCcino @ Mar 6 2008, 18:53) *
кое-что из литературы:


Спасибо!
Go to the top of the page
 
+Quote Post
lotorev
сообщение Mar 7 2008, 20:19
Сообщение #10


Участник
*

Группа: Свой
Сообщений: 60
Регистрация: 25-11-05
Пользователь №: 11 388



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

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

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

По 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
Go to the top of the page
 
+Quote Post
CaPpuCcino
сообщение Mar 7 2008, 21:10
Сообщение #11


тоже уже Гуру
******

Группа: Свой
Сообщений: 2 047
Регистрация: 13-06-05
Из: Кёлн - Санкт-Петербург
Пользователь №: 5 973



Цитата(lotorev @ Mar 7 2008, 23:19) *
Извините, если не в тему.
по поводу построения тестбенчей на основе SV, SystemC.

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


--------------------
И снова на арене цирка - дрессированные клоуны!! Оказываем консультации по электронике за симпу круглосуточно.
Go to the top of the page
 
+Quote Post
CaPpuCcino
сообщение Mar 9 2008, 00:51
Сообщение #12


тоже уже Гуру
******

Группа: Свой
Сообщений: 2 047
Регистрация: 13-06-05
Из: Кёлн - Санкт-Петербург
Пользователь №: 5 973



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


--------------------
И снова на арене цирка - дрессированные клоуны!! Оказываем консультации по электронике за симпу круглосуточно.
Go to the top of the page
 
+Quote Post
CaPpuCcino
сообщение Mar 9 2008, 16:08
Сообщение #13


тоже уже Гуру
******

Группа: Свой
Сообщений: 2 047
Регистрация: 13-06-05
Из: Кёлн - Санкт-Петербург
Пользователь №: 5 973



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


--------------------
И снова на арене цирка - дрессированные клоуны!! Оказываем консультации по электронике за симпу круглосуточно.
Go to the top of the page
 
+Quote Post
makc
сообщение Apr 18 2008, 13:23
Сообщение #14


Гуру
******

Группа: Админы
Сообщений: 3 531
Регистрация: 18-10-04
Из: Москва
Пользователь №: 904



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


--------------------
BR, Makc
В недуге рождены, вскормлены тленом, подлежим распаду. (с) У.Фолкнер.
Go to the top of the page
 
+Quote Post
maksya
сообщение May 5 2008, 20:41
Сообщение #15


Местный
***

Группа: Свой
Сообщений: 253
Регистрация: 28-08-04
Из: Ленинград
Пользователь №: 562



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

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

Цитата(des00 @ Mar 6 2008, 09:15) *
ЗЫ. сделать еще можно пару статей, но вот кто это будет делать вопрос......


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


--------------------
Лень - это не врожденное чувство русского человека, а средство борьбы с неуемной, но бестолковой энергией начальника.
Go to the top of the page
 
+Quote Post

4 страниц V   1 2 3 > » 
Reply to this topicStart new topic
6 чел. читают эту тему (гостей: 6, скрытых пользователей: 0)
Пользователей: 0

 


RSS Текстовая версия Сейчас: 17th October 2017 - 20:32
Рейтинг@Mail.ru


Страница сгенерированна за 0.01349 секунд с 7
ELECTRONIX ©2004-2016