PSL/The designers guide to VHDL/18.3 Embedded PSL in VHDL
- Литература
- IEEE Std 1850-2010
- Embedded PSL in VHDL (en)
- 1. Introduction (en)
- 2. Basic Temporal Properties (en)
- 3. Some Philosophy (en)
- 4. Weak vs. Strong Temporal Operators (en)
- 5. SERE Style (en)
18.3 PSL встроенный в VHDL
PSL — это язык спецификации свойств стандарта IEEE (IEEE Std 1850). Это позволяет спецификацию временных свойств модели, которые могут быть верифицированы, как статические (используя формальный доказательный инструмент) или динамические (используя проверки моделирования). VHDL допускает встроенный PSL, как часть модели VHDL. Это делает проект верификации намного более естественным, и упрощает разработку и сопровождение моделей. Так как PSL довольно обширный язык, мы не будем описывать все его особенности в деталях. Мы опишем путь, по которому PSL может быть встроен в VHDL. Для полного описания PSL и его использования в проектах верификации, заинтересованный читатель может посмотреть другие публикации. (Например, A Practical Introduction to PSL [4].)
Мы можем включать в VHDL свойства PSL, последовательности, декларации времени в декларативной части entity, архитектуру, оператор block (смотрите главу 23), оператор generate или декларацию пакета. Далее мы можем использовать декларированные свойства и последовательности в директивах PSL, написанных в соответствующих операторных частях.
Любые свойства, которые мы пишем в PSL декларациях и директивах, должны соответствовать простому подмножеству правил PSL. На практике, это означает, что мы можем только писать свойства, в которых время движется вперед, слева направо через свойство. Два примера из стандарта PSL показывают это. Первый, следующее свойство в простом подмножестве:
always (a -> next[3] b)
Это свойство показывает, что если a имеет значение true, то через три цикла b примет такое же значение; это значит, что время идет вперед три цикла, если мы выполняем свойство слева направо. Следующее свойство не относиться к простому подмножеству:
always ((a && next[3] b) -> c)
Это свойство показывает, что если a имеет значение true и b принимает значение true через три цикла, то далее c должен принять значение true в то же время, что и a. Проблема в этом свойстве заключается в том, что время двигается в обратном направлении от принятия значения b до принятия значения c. Инструмент для проверки таких свойств куда, как более сложный, чем для простого подмножества.
Директивы PSL нуждаются в спецификации времени, которая определяется, когда временное выражение рассчитано. Мы можем включить выражение времени в директиву. Однако, в то время, как такое же время подходит для всех директив проекта, проще включить декларацию времени по-умолчанию. Если мы напишем деклрацию времени по-умолчанию в области проекта, это подойдет для любых директив PSL, написанных в данном регионе. Наибольшее, мы можем включить одну декларацию времени по-умолчанию в данную область.
ПРИМЕР 18.8 Конвейерный связанные утверждения
В своей книге Assertion-Based Design [7], Foster et al. описывает образец верификации для системы, в которой конвейерная связность. В этом примере, система может принимать до 16 запросов, при подтверждении любого из них. Система считает количество запросов, их подтверждение, и включает утверждение, что для каждого запроса с данным подсчетом запросов, существует подтверждение с таким же счетом в течение 100 временных циклов.
library ieee; context ieee.ieee_std_context; entity slave is port ( clk, reset : in std_ulogic; req : in std_ulogic; ack : out std_ulogic; ... ); end entity slave; architecture pipelined of slave is signal req_cnt, ack_cnt : unsigned(3 downto 0); default clock is rising_edge(clk); property all_requests_acked is forall C in {0 to 15}: always {req and req_cnt = C} |=> {[*0 to 99]; ack and ack_cnt = C}; begin req_ack_counter : process (clk) is begin if rising_edge(clk) then if reset = '1' then req_cnt <= "0000"; ack_cnt <= "0000"; else if req = '1' then req_cnt <= req_cnt + 1; end if; if ack = '1' then ack_cnt <= ack_cnt + 1; end if; end if; end if; end process req_ack_counter; ... assert all_requests_acked; end architecture pipelined;Счетчики запросов и подтверждения выполняются, используя сигналы
req_cntиack_cntи процессreq_ack_counter. Мы декларируем свойствоall_requests_acked, которое выражает условие верификации для проекта. Мы, также, включаем декларацию времени по-умолчанию для архитектуры. Это подходит для утверждения директив, которые мы писали в области деклараций архитектуры, утверждая, что условие верификации выполняется.
Существует один случай, где встроенный в VHDL PSL может привести к двусмысленности. И PSL, и VHDL включают в себя выражения утверждений, но их смысл разный. Если мы напишем выражение вида:
assert not (a and b) report "a and b are both true";
оно может быть интерпретирована, как регулярное параллельное выражение VHDL утверждения, которое проверяется, когда a или b меняют значение. Также, оно может быть интерпретировано, как директива утверждения PSL, которая предполагает свойство not (a and b), выполняющееся во времени 0. В интересах совместимости с более ранними версиями языка, VHDL интерпретирует такие двусмысленные выражения, как регулярные параллельные выражения VHDL утверждений. Если мы действительно хотим написать директиву PSL утверждения такого вида, мы можем модифицировать свойство, таким образом получить однозначное PSL свойство, например:
assert next[0] not (a and b) report "a and b are both true";
В PSL код верификации может быть написан в блоках верификации (vunit, vprop и
vmode блоки), которые связаны с экземплярами entity и архитектур VHDL. VHDL применяет такие блоки верификации, как первичные блоки проекта. Таким образом, они могут быть декларированы в файлах VHDL проекта и проанализированы в библиотеках VHDL проекта.
Блок верификации может включать в себя обязательную информацию, которая определяет компонент образца, для которого применяется директива. Также, мы можем связать блок верификации, как часть конфигураций проекта. Единственное место, для того чтобы сделать это - декларация конфигураций, представленных в главе 13. Если мы хотим связать один и более блоков верификации к головному entity в декларации конфигураций, мы подключаем связывающую информацию, в соответствии со следующим синтаксическим правилом:
configuration_declaration ⇐
configuration identifier of entity_name is
{ use vunit verification_unit_name { , ... } ; }
block_configuration
end [ configuration ] [ identifier ] ;
Всякий раз, когда в декларации конфигурации экземпляра, либо в головном уровне иерархии проекта или как экземпляра компонента в более большом проекте, названные блоки верификации интерпретируются в контексте entity и архитектуры. Это означает, что имена, используемые в блоках верификации интерпретируются в контексте entity.
Пример 18.9 Связанный блок верификации в декларации конфигураций
предположим, что у нас есть блок верификации, который обеспечивает два выхода Q и Q_n, которые дополняют друг друга при переднем фронте сигнала clk. Блок верификации:vunit complementary_outputs { assert always Q = not Q_n; }Мы можем связать этот блок верификации с различными частями проекта. Например, модель gatelevel триггера D может быть описана так:
entity D_FF is port ( clk, reset, D : in bit; Q, Q_n : out bit ); end entity D_FF; architecture gate_level of D_FF is component and2 is ... ... begin G1 : and2 ... ... end architecture gate_level;Декларация конфигураций для триггера D может связать блок верификации с головным entity:
configuration fast_sim of D_FF is use vunit complementary_outputs; for gate_level for all : and2 ... end for; ... end for; end configuration fast_sim;Далее мы можем подтвердить конфигурации в проекте и для каждого экземпляра, блок верификации
complementary_outputsбудет связан с экземпляром entity и архитектуры.
Мы, также, можем связать блок верификации с экземплярами компонентов, которые конфигурируются покомпонентной конфигурацией, вложенной в декларацию конфигураций. Полная форма конфигурации компонента предполагает компоненты, связанные с entity и архитектурой, и архитектура дополнительно конфигурируется:
component_configuration ⇐
for component_specification
binding_indication ;
{ use vunit verification_unit_name { , ... } ; }
[ block_configuration ]
end for ;
В этом случаи, блоки верификации связаны с экземплярами определенными в декларации компонентов.
Пример 18.10 Связанный блок верификации в конфигурации компонента
Предположим, мы создаем регистр сдвига parallel-in/serial-out внутри RTL описания:
entity system is ... end entity system; architecture RTL of system is component shift_reg is port ( clk, reset, D : in bit_vector; Q, Q_n : out bit ); end component shift_reg; ... begin serializer : shift_reg ...; ... end architecture RTL;Мы можем написать декларацию конфигураций, которая свяжет entity и архитектуру с экземпляром компонента, а также свяжет блок complementary_outputs верификации, Пример 18.9.
configuration verifying of system is for RTL for serializer : shift_reg use entity work.shift_reg(RTL); use vunit complementary_outputs; end for; end for; end configuration verifying;В этом случаи, утверждение в блоке верификации применяется для выходов Q и Q_n регистра сдвига связанного entity с сериализатором экземпляра компонента.
Третье место, в котором мы можем применить блок верификации в VHDL проекте, это в спецификации конфигураций в архитектуре, где подтверждаются компоненты. Дополненное правило синтаксиса для спецификации конфигураций, снова предполагает связь компонентов с entity и архитектурой:
configuration_specification ⇐
for component_specification
binding_indication ;
{ use vunit verification_unit_name { , ... } ; }
end for ;
Это похоже на форму конфигурации компонентов, но без вложенных конфигураций для архитектуры.
Пример 18.11 Использование блока верификации в спецификации конфигураций
Мы можем пересмотреть архитектуру из примера 18.10 для включения связанной информации напрямую, а не в отдельной конфигурации. Архитектура:
architecture RTL of system is component shift_reg is ... end component shift_reg; for serializer : shift_reg use entity work.shift_reg(RTL); use vunit complementary_outputs; end for; begin serializer : shift_reg ...; ... end architecture RTL;
В то время, как блок верификации может включать связанную информацию, как часть своей декларации, существует возможность того, что эта информация может конфликтовать со связанной информацией, которую мы написали в конфигурациях. VHDL предотвращает такие конфликты, делая не полноправным привязывание блока верификации к конфигурациям, если он уже содержит связанную информацию. Следовательно, нужно писать привязку верификации в конфигурациях для общих блоков верификации, но не для каких-либо конкретных. В любом случаи, появится ошибка, если мы привяжем блок верификации с экземпляром компонента, у которого нету связи в entity и архитектуре.
В дополнение к связанным блокам верификации напрямую или в конфигурациях, VHDL предоставляет средство для связи блоков верификации через исполнительно-определенные значения. Это может включать, опции командной строки, команды скриптов или выбор, используемого графического интерфейса.
Немного дополнительных аспектов для PSL встроенного в VHDL. Первое, у PSL есть богатый набор зарезервированных слов, некоторые из которых могут конфликтовать с идентификаторами VHDL. Следующие PSL слова зарезервированы VHDL, и не могут использоваться, как идентификаторы:
assert assume assume_guarantee cover default fairness property restrict restrict_guarantee sequence strong vmode vprop vunit
Другие зарезервированные PSL слова только считаются таковыми, если в VHDL коде, они появляются в PSL декларациях и директивах. Они могут использоваться, как VHDL идентификаторы, но такие идентификаторы скрыты для деклараций и директив PSL. Например, мы можем полноправно написать следующую декларацию:
function rose ( x : boolean ) return boolean is ...;
Но если мы декларируем последовательность:
sequence cover_fifo_empty is
{reset_n && rose(cnt = 0)};
Ссылка на rose в декларации последовательности является в PSL встроенной функции, а не к декларации, написанной в VHDL.
Второе, PSL включает особенности для декларирования и экземпляров макросов, и разрешение директив препроцессора. Эти особенности могут использоваться только в блоках верификации PSL.
VHDL-87, -93, и -2002
Эти версии VHDL не позволяют PSL встраиваться в VHDL модели. Код PSL должен быть написан в отдельном блоке верификации и иметь связь с проектом VHDL, который использует определенные инструментарием значения.
