This chapter explains how to construct simple (i.e. non-sequential) assertions
using the layered structure of PSL.
Note this is a deliberately simplified description of PSL. Full details on the
language, coding styles; design guidelines and assertion methodologies can be found on the Esperan
Verification with PSL class
Boolean Layer
First we must decide if the assertion is an always or never property.
- Use always for checking a property is true or for conditional properties
- Use never for checking a simple property is never true
Then we construct a boolean expression (i.e. any expression allowed in an if
statement condition) to define the desired or undesired behavior. Enclose the expression in
curved brackets () and prefix with the PSL keyword
always or never:-
VHDL: never ((GNT and BUSY) = ’1’)
Verilog: always ((EN1 | EN2 ))
Note: PSL keywords like always
and never must be lower-case
Normal visibility and case-sensitivity rules apply for the expression, and any
subprograms etc allowed in a boolean expression can be used.
VHDL: always (unsigned(ASLV) <= 10)
Verilog: always (myfunction(B))
VHDL arithmetic package type-casting and
user-defined functions in either language are allowed
For a VHDL expression containing only std_logic values,
the equality operator (= ’1’ or = ’0’) may be
omitted as PSL interprets an expression evaluating to std_logic ’1’<
as true and std_logic ’0’ as false. PSL supports both forms:-
VHDL: never ((GNT and BUSY) = ’1’)
VHDL: never (GNT and BUSY)
For a VHDL expression containing mixed boolean and std_logic values, the equality is required as
VHDL logical operators cannot be used for combinations of boolean and std_logic types.
The following expression is OK - (boolean) and (boolean)
never ((ADDR = 0) and (REQ = ’1’))
This expressions is wrong - (boolean) and (std_logic)
never ((ADDR = 0) and REQ)
Also the VHDL rule on not reading output ports applies to PSL assertions as well.
Intermediate signals must be used if an output port is included in a property.
Implication
.
Conditional simple assertions can be built with the implication operation ->
VHDL: always(ACK -> not BUSY)
Verilog: always(ACK -> !BUSY)
when ACK is high, BUSY must be low.
ACK high is the enabling condition,
BUSY low is the fulfilling condition.
Note that this is the same as the following property:-
VHDL: always(not ACK or not BUSY)
Verilog: always(!ACK | !BUSY)
Think about it...
So what is the benefit of implication? Implication can be used to check
multi-cycle behavior using the next operator, i.e. if a condition is
true at the current evaluation point, then some condition must be true at a future evaluation point:-
VHDL: always(ACK -> next (not BUSY))
Verilog: always(ACK -> next (!BUSY))
when ACK is high, BUSY must be
low in the next evaluation point.
So how do we define evaluation points? The PSL Temporal Layer defines these:-
Temporal Layer
You should always define a clocking signal to control when the property is evaluated.
Clocks for individual assertions can be defined with the clock operator @. Any
boolean expression can be used as a clocking signal, but RTL clock expressions
(using Verilog posedge or negedge
and VHDL rising_edge or falling_edge functions or
’event expressions) are normally used:-
VHDL: never (GNT and BUSY)@falling_edge(CLK);
VHDL: always (EN1 or EN2)@(CLK’event and CLK = ’1’);
Verilog: always(ACK -> next (!BUSY))@(posedge CLK);
After the clock, the assertion must be terminated with a semi-colon.
Any signal can be used as a PSL clock. Properties can be greatly simplified by using signals
other then system clocks.
VHDL: always(ADDR /= 0)@falling_edge(WR_EN);
Verilog: always(ADDR != 0)@(negedge WE_EN);
A clocking signal can be defined for many properties using the default clock
statement. An assertion without an explicit clock, must still be terminated with a semi-colon.
Clock operators can still be applied to specific properties to over-ride the default clock - the
clock operator takes precedence over the default clock.
VHDL:
default clock is rising_edge(CLK);
always (EN1 or EN2);
never (GNT and BUSY)@falling_edge(CLK);
Verilog:
default clock = (posedge CLK);
always (EN1 | EN2);
never (GNT & BUSY)@(negedge CLK);
Note each language flavour uses its own syntax in declarations. Verilog uses
= as its definition symbol (DEF_SYM), but VHDL uses is.
Naming Your Properties.
Managment and debugging is easier when properties are named:-
VHDL:
property NOT_GNTBUSY is
never (GNT and BUSY)@falling_edge(CLK);
property P1 is
always(ACK -> next (not BUSY))@rising_edge(CLK);
Verilog:
property NOT_GNTBUSY =
never (GNT & BUSY)@(negedge CLK);
property P1 =
always(ACK -> next (!BUSY))@(posedge CLK);
The property name must be a legal name for your flavour of HDL, and must be unique in the current scope
(see embedding assertions below).
Verification Layer
For a property to be checked in simulation, it must be asserted. Assert the named property
to tell the simulator to start checking the assertion.
VHDL and Verilog:
assert NOT_GNTBUSY;
assert P1;
Embedding Assertions
Assertions can be embedded into your design code, or placed in an external file
(vunit) and associated with your design in compilation (see Esperan’s Verification with PSL
course for details on vunits). An assertion is embedded as a comment using the identifer
psl:-
-- VHDL - these assertions are complete!
-- psl property NOT_GNTBUSY is
-- never (GNT and BUSY)@falling_edge(CLK);
-- psl property P1 is
-- always(ACK -> next (not BUSY))@rising_edge(CLK);
-- psl assert NOT_GNTBUSY;
-- psl assert P1;
// Verilog - these assertions are complete!
// psl property NOT_GNTBUSY =
// never (GNT & BUSY)@(negedge CLK);
// psl property P1 =
// always(ACK -> next (!BUSY))@(posedge CLK);
// psl assert NOT_GNTBUSY;
// psl assert P1;
PSL assertions can break over several lines, but each line must begin with the
comment designator. Normal comments are not allowed inside a PSL assertion, i.e. between
psl keyword and the semi-colon terminating the assertion.
Assertions can be placed anywhere in a design, but it is better to group them
together at the begining or end of your design code.
The next cycle implication operator (-> next) allows multi-cycle property
behavior to be defined. Additional PSL operators such as until and
eventually allow more interesting and
open-ended design properties to be described (see below).
For complex multi-cycle properties where conditions must be checked in and over
many evaluation cycles, SEREs (Sequential Extended Regular Expressions) should be used
(see
the PSL SERE Assertions tutorial).
More PSL Operators
next[N]
An integer count can be added to the next operator to wait for a set number of
evaluation cycles before checking a fulfilling condition:-
-- VHDL
-- psl property P1 is
-- always(REQ -> next[2] BUSY)@rising_edge(CLK);
REQ high must be followed 2 clock cycles later by
BUSY high.
until
Specifies that one condition must remain true until another condition is
true. This is an "open-ended" construct with no limits on the second condition occuring:-
// Verilog
// psl default clock = (posedge CLK);
// psl property P2 =
// always (REQ -> (BUSY until ACK));
When REQ is high, BUSY must go
high in the same cycle and
remain high until ACK goes high.
eventually!
A condition eventually occurs. eventually! is a strong operator
(as indicated by the exclaimation mark) and so the condition of an eventually! operator must occur:-
--VHDL
-- psl default clock is rising_edge(CLK);
-- psl property P2 is
-- always (REQ -> eventually! ACK);
Overlapping Properties and Implication
Every PSL assertion is checked at every evaluation cycle. For an assertion with
implication, the enabling condition is checked at every cycle. If the condition is true, then
a new copy of the assertion is triggered, even if there are already versions active.
If property P2 above is asserted, then for every cycle
REQ is high, a copy of the assertion
would be triggered, e.g. if REQ is high for 3 cycles,
3 assertions would be active. When ACK
goes high, this will pass all 3 assertions.
Multiple active
assertions can cause problems in managing assertions or even result in incorrect failures
being reported. Overlapping assertions can be avoided by constructing implication
properties with edge-triggered rather than level-sensitive enabling conditions.
The easiest way to construct edge-triggered properties is using SEREs (Sequential
Extended Regular Expressions). See
the PSL SERE Assertions tutorial for more information.
Back to top
