|
|
|
Языки описания свойств аппаратуры, PSL/Sugar, SystemVerilog, OVL |
|
|
|
Oct 9 2008, 07:01
|
тоже уже Гуру
Группа: Свой
Сообщений: 2 047
Регистрация: 13-06-05
Из: Кёлн - Санкт-Петербург
Пользователь №: 5 973
|
Цитата(warrior-2001 @ Oct 9 2008, 10:34) А проверил ли кто на практике утверждение о том, что после создания первого проекта средствами OVM дальнейшие проекты пойдут как по маслу? OVM не такая уж и большая бублиотека (несколько десятков достаточно простельких мониторов), так что единственная сложность в использовании - это привыкнуть вставлять эти мониторы в код, поэтому утверждение достаточно справедливо в плане освоения библиотеки. Цитата(warrior-2001 @ Oct 9 2008, 10:34) Может кто в курсе, планируется ли поддержка графики для SystemVerilog? что вы имеете в виду под графикой? что-то на подобие библиотеке графических интерфейсов Tk? было бы определённо реально нефигово! но это больше вопрос к производителям симуляторов, нежле к разработчикам стандарта, потому что Tk кросспатформенный.
--------------------
И снова на арене цирка - дрессированные клоуны!! Оказываем консультации по электронике за симпу круглосуточно.
|
|
|
|
|
Jan 21 2009, 19:12
|
Частый гость
Группа: Свой
Сообщений: 104
Регистрация: 11-11-05
Из: Москва
Пользователь №: 10 714
|
Maksya, в своей статье Вы ссылаетесь на книжку vhdl_cohen, нет ли у Вас ее в электронном виде и не могли бы вы ее выложить на фтп?
По поводу статьи, мне кажется в ней есть фактическая неточность - PSL состоит из 2х частей - базиса (LTL-логика), и т.н. Optional Branching Extensions (CTL).
Если сравнивать PSL и SVA, мне кажется в плане функционала выигрывают последние, т.к. позволяют использовать методологию coverage driven verification (т.е. когда определенная контрольная точка функционального покрытия выполнена, прекращаем формировать рандомные пакеты для заданного блока). Т.е имеем двунаправленную интеграцию формальные утверждения <-> тестбенч. В PSL можем гнать данные только в 1 конец.
Кто-то интересовался синтезом ассертов, если коротко любая LTL-формула может быть представлена в виде автомата Бюхи. Есть САПРы которые синтезируют ассерты в виде некоторого блока, вставляемого в RTL, что позволяет их использовать в FPGA любого производителя. Контроль идет через специальный отладочный порт а-ля JTAG и спецсофт компании-разработчика. Посмотрите например, Dialite от Temento Systems.
|
|
|
|
|
Dec 3 2012, 12:52
|
Гуру
Группа: Свой
Сообщений: 2 198
Регистрация: 23-12-04
Пользователь №: 1 640
|
Цитата(Poluektovich @ Dec 3 2012, 15:07) У меня по поводу тулов еще вопрос возник. Questa Formal (0-in formal) кто-нибудь использовал? В закромах этот пакет мне удалось найти... доступно formality от синопсиса. этот 0-in formal очень рекламируется Ментором, но чтоб его где-то использовали - не слышал пользуют либо формалити либо конформал от каденса. также попадались некие "университетские" тулзы, но там нет ввода на верилоге, ну и как-то все специфично - я не осилил, теоретически возможен даже синтез по асершинам а вообщето тулзы формальной верификации слегка не для этого http://www.synopsys.com/Tools/Verification.../Formality.aspxhttp://www.cadence.com/products/ld/equival...es/default.aspx
|
|
|
|
|
Dec 7 2012, 07:51
|
Местный
Группа: Свой
Сообщений: 375
Регистрация: 9-10-08
Из: Таганрог, Ростовская обл.
Пользователь №: 40 792
|
Цитата(Poluektovich @ Dec 3 2012, 15:07) У меня по поводу тулов еще вопрос возник. Questa Formal (0-in formal) кто-нибудь использовал? В закромах этот пакет мне удалось найти... Опыт работу есть. Что именно интересует? Такого рода формальная верификация подходит, если на нее затачиваться с самого начала. К примеру поддержку любого сложного интерфейса проверяют всегда в первую очередь. А для математических блоков использование данного подхода неэффективно.
--------------------
Глупцы игнорируют сложность. Прагматики терпят ее. Некоторые могут избегать ее. Гении ее устраняют.
|
|
|
|
|
|
1 чел. читают эту тему (гостей: 1, скрытых пользователей: 0)
Пользователей: 0
|
|
|