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

    

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

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

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

Изменено пользователем warrior-2001

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


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

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

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

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

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


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

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

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


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

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

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

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


Ссылка на сообщение
Поделиться на другие сайты
помоему кто то перепутал OVM c OVL :beer:

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

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


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

 

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

 

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

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


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

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

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


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

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

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


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

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

 

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

 

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

 

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

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


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

Как на сегодняшний день обстоят дела с использованием ЯОСА и тулов для статической формальной верификации?

Появившиеся материалы:

SystemVerilog утверждения для верификации и имитационного моделирования

The Power of Assertions in SystemVerilog

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


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

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

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


Ссылка на сообщение
Поделиться на другие сайты
У меня по поводу тулов еще вопрос возник. 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

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


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

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

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


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

 

Опыт работу есть. Что именно интересует?

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

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


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

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

 

warrior-2001, делали ли вы оценку покрытия и какие цифры удавалось?

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

 

Платформой Questa мы не пользуемся, но он интересен наличием библиотеки QVL.

Cadence предлагает в своем портфолио ABVVIP для системных шин AMBA/OCP и контроллеров памятей, остальные VIP только для динамики. В библиотеке QVL имеется хороший набор последовательных интерфейсов.

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

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


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

Для публикации сообщений создайте учётную запись или авторизуйтесь

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

Создать учетную запись

Зарегистрируйте новую учётную запись в нашем сообществе. Это очень просто!

Регистрация нового пользователя

Войти

Уже есть аккаунт? Войти в систему.

Войти
Авторизация