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;
In addition to binding verification units directly in their declaration or indirectly in configurations, VHDL allows a tool to bind additional verification units through implementation-defined means. That might include command-line options, script commands, or selection using a graphical user interface.
There are a couple of further points to make about PSL embedded in VHDL. First, PSL has a rich set of reserved words, some of which may conflict with VHDL identifiers. The following PSL keywords are VHDL reserved words, and cannot be used as identifiers:
assert assume assume_guarantee cover default fairness property restrict restrict_guarantee sequence strong vmode vprop vunit
Other PSL reserved words are only recognized as such within VHDL code when they occur in PSL declarations and directives. They can be used as VHDL identifiers, but such identifiers are hidden within PSL declarations and directives. For example, we can legally write the following declaration:
function rose ( x : boolean ) return boolean is ...;
But if we then declare a sequence:
sequence cover_fifo_empty is
{reset_n && rose(cnt = 0)};
The reference to rose in the sequence declaration is to the PSL built-in function, not to
the declaration written in VHDL.
Second, PSL includes features for declaring and instantiating macros, and allows for preprocessor directives. These features can only be used in PSL verification units, not in other VHDL design units.
VHDL-87, -93, and -2002
These versions of VHDL do not allow PSL to be embedded within VHDL models. PSL code must be written in separate verification units and bound to the VHDL design us- ing tool-defined means.
