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

[CaPpuCcino]

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

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

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

[Poluektovich]

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

warrior-2001, делали ли вы оценку покрытия и какие цифры удавалось?
Математический блок внутри контроллера жизнь тоже осложнил в таком подходе, здесь эталонная поведенческая модель нужна.

Платформой Questa мы не пользуемся, но он интересен наличием библиотеки QVL.
Cadence предлагает в своем портфолио ABVVIP для системных шин AMBA/OCP и контроллеров памятей, остальные VIP только для динамики. В библиотеке QVL имеется хороший набор последовательных интерфейсов.
Если проверяли последовательные интерфейсы каких усилий стоит получение статусных состояний по всему набору утверждений? Использовалась ли гибридная верификация (формальный анализ + динамическая симуляция)?

[warrior-2001]

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

warrior-2001, делали ли вы оценку покрытия и какие цифры удавалось?
Математический блок внутри контроллера жизнь тоже осложнил в таком подходе, здесь эталонная поведенческая модель нужна.

Платформой Questa мы не пользуемся, но он интересен наличием библиотеки QVL.
Cadence предлагает в своем портфолио ABVVIP для системных шин AMBA/OCP и контроллеров памятей, остальные VIP только для динамики. В библиотеке QVL имеется хороший набор последовательных интерфейсов.
Если проверяли последовательные интерфейсы каких усилий стоит получение статусных состояний по всему набору утверждений? Использовалась ли гибридная верификация (формальный анализ + динамическая симуляция)?

Если честно - мне результаты не понравились. И проблема именно в трудозатратах. Дело в том, что для формальной проверки проект должен быть изначально на это ориентирован. И когда в компании уже есть большое кол-во СФ блоков, разработанных и отлаженных ранее, то когда они вставляются в проект - они выпадают из области покрытия и результирующие цифры уж очень не красивые. Если же тестировать отдельно СФ блок - то в большинстве случаев удается проверить его работу так сказать по полному графу. То есть перебрать весь набор входных воздействия и сравнить с эталоном.
На мой взгляд - использование формальной верификации оправдано, если разработка ведется с системного уровня.
По поводу гибридной верификации - мы пишем тестовые окружения на SV и занимаемся верификаций в QuestaSim. Отдельно моделировать проекты смысла нет.