Jump to content

    

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

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

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

Edited by warrior-2001

Share this post


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

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

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

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

Share this post


Link to post
Share on other sites

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

Share this post


Link to post
Share on other sites

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

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

Share this post


Link to post
Share on other sites
помоему кто то перепутал OVM c OVL :beer:

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

Share this post


Link to post
Share on other sites
Для этой же цели интересуют рабочие проекты с приминением методологии OVM.

 

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

 

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

Share this post


Link to post
Share on other sites

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

Share this post


Link to post
Share on other sites

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

Share this post


Link to post
Share on other sites

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

 

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

 

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

 

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

Share this post


Link to post
Share on other sites

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

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

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

The Power of Assertions in SystemVerilog

Share this post


Link to post
Share on other sites

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

Share this post


Link to post
Share on other sites
У меня по поводу тулов еще вопрос возник. 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

Share this post


Link to post
Share on other sites

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

Share this post


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

 

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

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

Share this post


Link to post
Share on other sites

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

 

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

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

 

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

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

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

Share this post


Link to post
Share on other sites

Create an account or sign in to comment

You need to be a member in order to leave a comment

Create an account

Sign up for a new account in our community. It's easy!

Register a new account

Sign in

Already have an account? Sign in here.

Sign In Now
Sign in to follow this