Property Specification Language Tutorial
(Part 2)
by
Ajeetha Kumari
Previous: Propoert Expression: Boolean layer |
Next: Property Expressions: Properties
We will continue to explore property expressions in this part with its temporal layer.
In this part, you will learn about Sequences and Properties. [Editorial note: Pages
have been slightly reorganized to keep the flow of the article.]
Property Expressions: Temporal Layer
While boolean layer forms the foundation of PSL, the real power of PSL comes
from its temporal layer. The term Temporal refers to the design behavior expressed
as a series of boolean expressions over multiple clock cycles. To support this, PSL
has two major components in the temporal layer: Sequences and Properties. Sequences
are built from basic boolean expressions and using sequence operators such as repetition
operators. Properties are built on top of sequences and can include boolean expressions,
sequences and other sub-ordinate properties.
Sequences
One of the main requirements of an assertion language is to be able to concisely
express design behavior over multiple clocks. PSL supports SEREs (Sequential
Extended Regular Expressions) to meet this requirement. It provides an easy
and familiar way to engineers to capture sequential behavior. The syntax is
derived from standard UNIX regular expressions and hence the name SERE. The first
and foremost requirement of any temporal sequence is a neat way to move time forward.
PSL uses SERE concatenation to achieve this. This operator is represented
with a semicolon symbol ;. Hence, the following pseudo-code:
{a;b}
Describes the following behavior:
- a being high in the current clock tick
- Wait till next clock tick (t+1) and
- Check for b being high.
The curly braces around the sequence mark the beginning and ending of a SERE. In real
life, the delay between two such expressions can be:
- More than one
- A range
- Not necessarily occurring in contiguous clock cycles
PSL supports all these requirements via its repetition operators. There are three
types of SERE repetition operators which are explained below.
Consecutive repetition operator
To be able to specify that a signal must be asserted continuously for say 3 clocks,
one can write:
{sig_a;sig_a;sig_a}
PSL provides a short cut notion to the above as:
{sig_a[*3]}
The number can also be a range with a MIN and MAX specification as shown below:
{sig_a[*MIN:MAX]}
Few notes on the ranges:
- Both MIN and MAX have to be elaboration time constants.
- Both have to be natural numbers (0 and above).
- MIN can be set to 0.
- MAX can be set to the key word inf to indicate infinity.
- To specify one or more repetitions, a UNIX regexp style '+' can be used.
The following SEREs show few possible repetitions operators. They all capture
the following requirement of a write protocol.
- The desired sequence starts when signal wr_started gets asserted.
- In the very next clock, wr_channel_busy gets asserted (The number of clocks
that this signal remains asserted is variable, and few variances are shown below).
- The sequence finishes when a wr_done is seen after desired number of
wr_channel_busy.
wr_started; wr_channel_busy[*2]; wr_done;
wr_started; wr_channel_busy[*0:100]; wr_done;
wr_started; wr_channel_busy[*2:inf]; wr_done;
wr_started; wr_channel_busy[+]; wr_done;
Non-Consecutive repetition operator
A non-consecutive repetition is very similar to consecutive repetition except that the occurrences of the
repeated expression/sequence need not be contiguous. PSL uses the symbol '=' to denote non-consecutive
repetition. The examples in the previous section with a non-consecutive repetition are shown below:
wr_started; wr_channel_busy[=2]; wr_done;
wr_started; wr_channel_busy[=0:100]; wr_done;
wr_started; wr_channel_busy[=2:inf]; wr_done;
GOTO Repetition operator
Some times, the requirement is such that, we want to go to the nth repetition and immediately (1 clock after)
after the occurrence of that last repetition we would like to check for the next expression in sequence. The
intermediate repetitions may be non-consecutive i.e. can be spread across multiple cycles. This is referred
to as GOTO repetition in PSL and is represented with '->' symbol. The examples in the previous section
with a GOTO repetition are shown below:
wr_started; wr_channel_busy[->2]; wr_done;
wr_started; wr_channel_busy[->0:100]; wr_done;
wr_started; wr_channel_busy[-> 2:inf]; wr_done;
SERE within operator
The SERE within operator constructs a SERE in which one sequence’s start and end points are fully contained
within the other sequence. In the following example
A_Sere within B_Sere
A_Sere’s start point should be after (or same as) the B_Sere and its end point should be before (or same as)
that of B_Sere.
Compound SERE operators
While the repetition operators enhance PSL with the ability to build basic SEREs, more complex sequences can
be described by combining two or more sequences. PSL provides the following operators for building compound
SEREs.
- Fusion operator (:)
- SERE non-length matching and (&)
- SERE length-matching and (&&)
- SERE or operator (|)
Since these are advanced topics, we will skip them in this tutorial.
Endpoints
In PSL sequences typically span across multiple clocks. Sometimes it is useful to detect whether a particular
sequence has reached its 'end' regardless of its starting time. PSL supports it via endpoint construct. In PSL,
endpoints are assigned a name by the user and such endpoints can be instantiated anywhere wherever a
boolean expression is allowed and it results in true or false.
As an example, a packet transaction is considered complete only when every start-of-packet receives its
end-of-packet signal. However, a packet can be aborted after one or many transfers. The following
endpoint captures the abort sequence via en endpoint and uses it in a property specification later.
endpoint e_pkt_aborted = {pkt_sop; pkt_xfer_in_progress[*1:100];pkt_abort};
property p_expect_eop = {pkt_sop |-> eventually! pkt_eop abort e_pkt_aborted};
Previous: Propoert Expression: Boolean layer |
Next: Property Expressions: Properties
|