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

[CaPpuCcino]

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

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

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

[radigast]

Приветствую коллег в этой ветке!

С момента последнего сообщения прошло уже 4 года, за это время тулы и методики формальной верификации заметно подросли. В этой связи позволю себе освежить тему вопросом по статусу практического опыта использования формальных методов верификации.
Если использованием ABV в динамике сейчас никого не удивишь (SVA/OVL активно используются), то вот про опыт промышленного применения формальных подходов слышно не так часто.
Последний раз, когда мы пробовали на базе ABV формально верифицировать блоки сложнее АЛУ натыкались на логичную проблему комбинаторного взрыва. Чтобы процесс сошёлся при жизни запускающего его инженера требовалось задавать слишком уж жёсткие ограничения, что негативно сказывается на достигаемом покрытии.
Собственно вопрос (если не секрет): именно в «боевых» проектах блоки какой сложности удавалось проверить формально на базе ABV/model checking, какие тулы при этом использовались (может у кого есть опыт работы с теми же ABVVIP от Cadene?)