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

[CaPpuCcino]

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

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

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

[RHnd]

Если не сложно, то можно для совсем не понимающих, но учащихся, объяснить, о чем идет речь? Для затравки. Т.е. чем ЯОСА отличается от HDL?

[CaPpuCcino]

Языки описания свойств аппаратуры в отличие от языков описания аппаратуры, которые описывают структуру цифровой системы, предназначены для описания отношения состояний системы во времени (в частности отношения сигналов в устройстве или внешнем интерфейсе). При проектировании системы языки описания свойств применяются как вспомогательный инструмент для локализации ошибок реализации и верификационного покрытия проектов.

Языкам описания свойств присуще принципиально иной более абстрактный уровен определения поведения системы и её компонентов относительно друг-друга нежле языкам описания аппаратуры. Базовыми понятиями ЯОСА является последовательность (sequence), свойство(property), утверждение(assertion) и покрытие(coverage).

Последовательность - это описание последовательности систояний системы. Например: data_request ## 2 channel_grant ## 4 data_acknowledged описывает следующую посленовательность систояний - после того как выражение data_request истинно через 2 такта выражение channel_grant истинно после чего выражение data_acknowledged истенно через 4 такта, при этом временные отношения могут быть и плавающими (например ##[2:5] означает "от 2 до пяти", [*1:$] один и более раз до бесконечности(конца симуляции для динамический сред), и так далее). Последовательности могут быть произвольной длинны включая вложенные и единичные.

Свойство - это описание логических отношений между последовательностями. Так например: data_request |=> !data_grant[*4] описывает отношение "в случае установления сигнала(выражения) data_request, data_grant не может быть истинно в течение 4 циклов"; или request |-> ##[1:100] grant означает, что если request истина, то grant должен быть установлен не позднее чем через 100 циклов (в обоих примерах мы имеем свойство описывающее импликацию последовательностей единичной длинны).

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

Код

    property source_register_overwtire_before_cannel_forwarding;
        @(posedge clk) disable iff (!reset_n) (register_valid && !channel_grant) ##1 ( register_valid && !channel_grant ) |-> (data_registered==$past(data_registered));
    endproperty
            
    assret property source_register_overwtire_before_cannel_forwarding
                else $error("Данные в регистре были изменены до принятия их в канал данных");

Само свойство означает, что если установлен флаг действительности данных в регистре, но канал данных не подтверждает их захват и в следующем такте состояние системы не изменилось(комбинация флагов), то данные в регистре остаются неизменными по отношению с предыдущим тактом. Утверждение в свою очередь проверяет не были ли перезаписаны данные в регистре до того как они были продвинуты в канал данных. Если подобное произошло сообщаем об ошибке. Такая короткая запись свойства может сослужить хорошую службу при дальнейшей верификации системы. Ведь если запрос на запись в канал можно напрямую привязать к флагу register_valid, то логика записи в регистр может быть довольно сложной (например несколько источников с разными приоритетами), и правильность функционирования схемы записи в этот регистр может быть неочевидной. Если предположить, что подобная ошибка была допущена и наш канал используется как строительный блок большой системы, то на этапе её верификации будет очень сложно определит причину некорректного функционирования целой системы. Это потребует многие часы, а то и дни анализа проекта. В то же время использование свойств (ЯОСА) позволит мгновенно локализовать ошибку.

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

Синтаксис ЯОСА встроен в современные HDVSLи (Hardware Descriprion Verification and Specification Language) такие как SystemVerilog и новый VHDL.

NB: прошу не сильно критиковать за приведённые примеры, я ещё плохо пишу на ЯОСА и может что-то неправильно закодировал. однако исправления приветствуются