This tutorial explains how to construct simple sequential assertions using PSL SEREs
(Sequential Extended Regular Expressions). It assumes you are familar with the
Simple PSL Assertions tutorial.
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.
SEREs
SEREs allow complex multi-cycle PSL properties to be defined, where conditions must be
checked in and over many evaluation cycles.
A SERE is composed of boolean expressions separated by a SERE operator, e.g.
concatention (;), and enclosed in curly brackets {}.
The concatention operator specifies that the boolean conditions should be true on subsequent evaluation
cycles.
{B;C;D}
B high in the first cycle,
then C high in the next and
D high in the third cycle. The following waveform meets this SERE:-
A SERE cycle is defined with either a clock operator or a default clock statement.
If a signal condition is not defined in a given cycle, the assertion ignores that signal. For
example in the SERE above, B is not checked in cycles 2 and 3. To constrain
the assertion further, the signals can be fully-specified in each cycle:-
VHDL: { B and not (C or D);
C and not (B or D);
D and not (B or C) }
Verilog: { B & !(C | D);
C & !(B | D);
D & !(B | C) }
The following waveform meets this SERE:-
SEREs can also be used with a single boolean expression.
VHDL: always {(EN1 or EN2})@falling_edge(CLK);
Verilog: always {(EN1 | EN2})@(negedge CLK);
As the boolean expression is a
SERE, it must still be enclosed in curly brackets {}.
SERE Implication
Although SERE assertions can be constructed without implication, their behavior is nonintuitive,
therefore it is recommended to always use implication operators with SEREs
Same cycle implication uses |->:-
VHDL: {REQ; BUSY} |-> {not GNT}
Verilog: {REQ; BUSY} |-> {!GNT}
If REQ is high in the first cycle and
BUSY is high in the second, GNT
must be low in the second cycle also.
{REQ; BUSY} is the enabling SERE and {not GNT}
is the fulfilling SERE. When the enabling SERE completes, the simulator expects the fulfilling SERE to
follow and will report an error if the fulfilling SERE does not complete.
Next cycle implication uses |=>:-
{REQ; GNT} |=> {ACK}
if REQ is high in the first cycle and
GNT high in the second, ACK must be
high in the third cycle.
Constructing a Complete SERE Assertion
Follow the these steps to construct a simple SERE assertion:-
- Decide on current cycle (|->) or next cycle (|=>)
implication.
- Define the enabling and fulfilling SEREs, enclose in {} and place round the
implication operator.
- Enclose the SEREs in () and prefix with always
(SERE assertions, being conditional, must use always).
- Specify the evaluation cycle using a clock operator @ at the end of the
property, (or use a default clock statement for a collection of properties). Terminate property with ;
- Name the property and assert the property name to enable checking.
- For an embedded assertion, comment each line and insert the psl keyword at the
beginning of the property definition and assert statement.
-- Complete VHDL SERE assertion
-- psl property P1 is
-- always( {REQ; GNT} |=>
-- {BUSY; DONE} )@rising_edge(CLK);
-- psl assert P1;
// Complete Verilog SERE assertion
// psl property P1 =
// always( {REQ; GNT} |=>
// {BUSY; DONE} )@(posedge CLK);
// psl assert P1;
If REQ high is followed by
GNT high, then on the
next cycle BUSY must be
high, followed by DONE
high.
Assertion Status
A SERE assertion, evaluated over several cycles can pass through several states. A simplified diagram
of Assertion Status is as follows:-
An assertion starts inactive. At every evaluation point, the first condition in the enabling
SERE is checked. If this condition is true, the assertion becomes active. If the enabling
SERE fails to complete, then the assertion becomes inactive without any error message. If
the enabling SERE completes, then the assertion is enabled and the fulfilling SERE is
checked. If this completes then the assertion passses. If the fulfilling SERE of an enabled
assertion does not complete, the assertion fails.
Named Sequences
A SERE fragment can be declared as a named sequence and used as a building block in
more complex SEREs.
VHDL:
sequence S1 is {B; C};
sequence S2 is {D; E};
sequence S3 is {X; Y; Z};
property P2 is
always( {S1; S2} |=> S3 )@rising_edge(CLK);
Verilog:
sequence S1 = {B; C};
sequence S2 = {D; E};
sequence S3 = {X; Y; Z};
property P2 =
always( {S1; S2} |=> S3 )@(posedge CLK);
P2 is equivalent to the following property:-
VHDL:
always( {B; C; D; E} |=> {X; Y; Z} )@rising_edge(CLK);
Verilog:
always( {B; C; D; E} |=> {X; Y; Z} )@(posedge CLK);
Named sequences are ideal for breaking down complex SEREs into smaller blocks and
defining SERE patterns which are common to several properties. Sequences can also be
parameterized, which allows common SERE patterns to be used with different signals:-
VHDL:
sequence PARAM (boolean N) is {N; GNT; not N};
...
PARAM(REQ1) -- equals {REQ1; GNT; not REQ1}
PARAM(REQ2) -- equals {REQ2; GNT; not REQ2}
Verilog:
sequence PARAM (boolean N) = {N; GNT; !N};
...
PARAM(REQ1) -- equals {REQ1; GNT; !REQ1}
PARAM(REQ2) -- equals {REQ2; GNT; !REQ2}
Selected SERE Operators
There is a wide range of operators to construct complex SEREs. These are all described in
detail on the Esperan Verification with PSL course. Below are two examples-
Consecutive Repetition [*N]
Defines a sequence which repeats on consecutive evaluation cycles:-
{S; T[*3]; V}
Equivalent to {S; T; T; T; V}
The operator can be used without a SERE, in which case it simply counts evaluation cycles:-
{S; [*2]; V}
Equivalent to {S; -; -; V}
where - represents a cycle in
which no checks are performed.
A range of consecutive repetitions can be counted and there are short-hand notations for
"one or more" repetitions [+] or "zero or more" repetitions [*] .
SERE Or |
Defines that one or more of a choice of multiple sequences hold:-
VHDL:
sequence S4 is {B; C};
sequence S5 is {R; S};
property P3 is
always ( {T} |=> {S4} | {S5} );
Verilog:
sequence S4 = {B; C};
sequence S5 = {R; S};
property P3 =
always ( {T} |=> {S4} | {S5} );
After T occurs, either S4 or S5 must
start in the next evaluation cycle.
The following sequences would satisfy this property:-
- Sequence 1: {T; B; C}
- Sequence 2: {T; R; S}
- Sequence 3: {T; (B and R); S}
- Sequence 4: {T; (B and R); (S and C)}
In sequence 3, both S4 and S5 start in the
cycle following T. However only S5 completes.
Overlapping Properties and Implication
Every PSL assertion is checked at every evaluation cycle. For an assertion with implication,
the enabling SERE is checked at every cycle. If the initial condition of the SERE is true,
then a new copy of the assertion becomes active, even if there are already versions active.
If property P3 above is asserted, then for every cycle
T is high, a copy of the assertion would
be triggered, e.g. if T is high for 3 cycles, 3 assertions would be active.
Each active assertion
will expect the fulfilling condition {S4} | {S5} to complete.
Overlapping assertions can be
avoided by constructing implication properties with edge-triggered rather than level sensitive
enabling conditions. The property P3 above can be made edge-triggered by
defining the enabling SERE as { rose(T) }, i.e. T
low in one cycle, and high in the next.
More detailed information on SERE assertions and PSL coding guidelines can be found on
the Esperan Verification with PSL training course.
Back to top
