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.
EXAMPLE 18.9 Binding a verification unit in a configuration declaration
Suppose we have a verification unit that ensures two outputs named Q and Q_n are complementary when sampled on rising edges of a signal named clk. The verification unit isvunit complementary_outputs { assert always Q = not Q_n; }We can bind this verification unit to various parts of a design. For example, a gatelevel model of a D flipflop might be described as follows:
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;A configuration declaration for the D flipflop can bind the verification unit to the top-level entity as follows:
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;We could then instantiate the configuration in a design, and for each instance, the verification unit
complementary_outputswould be bound to the instantiated entity and architecture.
We can also bind verification units to component instances that are configured bycomponent configuration nested within a configuration declaration. The augmented form
of component configuration, assuming the components are bound to an entity and archi-
tecture, and the architecture is further configured, is
component_configuration ⇐
for component_specification
binding_indication ;
{ use vunit verification_unit_name { , ... } ; }
[ block_configuration ]
end for ;
In this case, the named verification units are bound to the instances specified in the component configuration.
EXAMPLE 18.10 Binding a verification unit in a component configuration
Suppose we instantiate a parallel-in/serial-out shift register within an RTL design:
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;We can write a configuration declaration that binds an entity and architecture to the component instance and that also binds the complementary_outputs verification unit shown in Example 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;In this case, the assertion in the verification unit applies to the Q and Q_n outputs of the shift register entity bound to the serializer component instance.
The third place in which we can bind verification units in a VHDL design is in a con- figuration specification in the architecture where components are instantiated. The aug- mented syntax rule for a configuration specification, again assuming components are bound to an entity and architecture, is
configuration_specification ⇐
for component_specification
binding_indication ;
{ use vunit verification_unit_name { , ... } ; }
end for ;
This is similar to the form in a component configuration, but without the nested configuration for the architecture.
EXAMPLE 18.11 Binding a verification unit in a configuration specification
We can revise the architecture of Example 18.10 to include the binding information directly, rather than in a separate configuration. The revised architecture is
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;
Since a verification unit may include binding information as part of its declaration, there is potential for that information to conflict with binding information we write inconfiguration. VHDL prevents such conflict by making it illegal to bind a verification unit in a configuration if the declaration of the unit already includes binding information. Hence, we would normally only write verification bindings in configurations for general-purpose verification units, and not for those written with particular instances in mind. In any case, it would be an error if we wrote a verification unit binding for a component instance that had no bound entity and architecture.
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.
