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

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