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

[CaPpuCcino]

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

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

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

[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.