Языки описания свойств аппаратуры в отличие от языков описания аппаратуры, которые описывают структуру цифровой системы, предназначены для описания отношения состояний системы во времени (в частности отношения сигналов в устройстве или внешнем интерфейсе). При проектировании системы языки описания свойств применяются как вспомогательный инструмент для локализации ошибок реализации и верификационного покрытия проектов.
Языкам описания свойств присуще принципиально иной более абстрактный уровен определения поведения системы и её компонентов относительно друг-друга нежле языкам описания аппаратуры. Базовыми понятиями ЯОСА является последовательность (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: прошу не сильно критиковать за приведённые примеры, я ещё плохо пишу на ЯОСА и может что-то неправильно закодировал. однако исправления приветствуются
И снова на арене цирка - дрессированные клоуны!! Оказываем консультации по электронике за симпу круглосуточно.