Property Specification Language Tutorial

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}

• 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

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}

 {sig_a[*3]}

  {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

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 (|)

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};