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 Embedded PSL in VHDL
PSL is the IEEE Standard Property Specification Language (IEEE Std 1850). It allows specification of temporal properties of a model that can be verified either statically (using a formal proof tool) or dynamically (using simulation checkers). VHDL allows PSL code to be embedded as part of a VHDL model. This makes design for verification a much more natural activity, and simplifies development and maintenance of models. Since PSL is itself a significant language, we won’t describe all of its features in detail in this book. Instead, we will just describe the way in which PSL can be embedded in VHDL. For a full description of PSL and its use in verifying designs, the interested reader is referred to other published books on the subject. (See, for example, A Practical Introduction to PSL [4].)
In VHDL we can include PSL property, sequence, and default clock declarations in the declarative part of an entity, architecture, block statement (see Chapter 23), generate statement, or package declaration. We can then use the declared properties and sequences in PSL directives written in the corresponding statement parts.
Any properties that we write in PSL declarations and directives must conform to PSL’s simple subset rules. In practice, this means that we can only write properties in which time moves forward from left to right through the property. Two examples from the PSL standard illustrate this. First, the following property is in the simple subset:
always (a -> next[3] b)
This property states that if a is true, then three cycles later, b is true; that is, time moves
forward three cycles as we scan the property left to right. In contrast, the following property is not in the simple subset:
always ((a && next[3] b) -> c)
This property states that if a is true and b is true three cycles later, then c must have
been true at the time a was true. The problem with this property is that time goes backward from b being true to c being true. A tool to check such a property is much more
complex than one to check properties in the simple subset.
PSL directives require specification of a clock that determines when temporal expressions are evaluated. We can include a clock expression in a directive. However, since the same clock usually applies to all directives in a design, it is simpler to include a default clock declaration. If we write a default clock declaration in a region of a design, it applies to any PSL directives written in that region. We can include at most one default clock declaration in any given region.
EXAMPLE 18.8 Pipelined handshake assertion
In their book Assertion-Based Design [7], Foster et al. describe a verification pattern for a system in which handshaking is pipelined. In their example, a system can receive up to 16 requests before acknowledging any of them. The system counts the number of requests and acknowledgments and includes an assertion that, for every request with a given request count, there is an acknowledgment with the same count within 100 clock cycles. We can describe the system in VHDL as follows:
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;The counters for requests and acknowledgments are implemented using the signals
req_cntandack_cntand the processreq_ack_counter. We declare a property,all_requests_ackedthat expresses the verification condition for the design. We also include a default clock declaration for the architecture. It applies to the assert directive that we write in the statement part of the architecture, asserting that the verification condition holds.
There is one case where embedding of PSL within VHDL may lead to ambiguity. Both
PSL and VHDL include assert statements, but their meanings differ. If we write a statement
of the form
assert not (a and b) report "a and b are both true";
it could be interpreted as a regular VHDL concurrent assertion statement that is to be
checked whenever either of a or b changes value. Alternatively, it could be interpreted as
a PSL assert directive that requires the property not (a and b) to hold at time 0. In the
interest of backward compatibility with earlier versions of the language, VHDL interprets
such ambiguous statements as regular VHDL concurrent assertion statements. If we really
want to write a PSL assert directive of this form, we could modify the property so thatis unambiguously a PSL property, for example:
assert next[0] not (a and b) report "a and b are both true";
In PSL, verification code can be written in verification units (vunit, vprop and
vmode units) that are bound to instances of VHDL entities and architectures. VHDL considers such verification units as primary design units. Thus, they can be declared in VHDL design files and analyzed into VHDL design libraries.
A verification unit can include binding information that identifies a component instance to which directives apply. Alternatively, we can bind a verification unit as part of the configuration of a design. One place to do that is in a configuration declaration, introduced in Chapter 13. If we want to bind one or more verification units to the top-level entity in a configuration declaration, we include binding information according to the following synax rule:
configuration_declaration ⇐
configuration identifier of entity_name is
{ use vunit verification_unit_name { , ... } ; }
block_configuration
end [ configuration ] [ identifier ] ;
Whenever the configuration declaration is instantiated, either at the top-level of a design hierarchy or as a component instance within a larger design, the named verification units are bound to the instance of the named entity and architecture. That means the names used in the verification units are interpreted in the context of the entity instance.
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.
