Property Specification Language Tutorial

Anatomy of a PSL assertion (contd.)

Property to be checked

This forms the core of PSL. PSL allows properties to be first declared and then used in an assertion or simply specify the complete property in the assertion itself as shown in Figure 1.

Clocking event

Properties can be either clocked or unclocked. For now this tutorial focuses on clocked properties. A clock for a property can be either specified inline in the property definition itself as shown in Figure 1. The symbol @ is used to specify clocking. Any boolean expression can be used as clock. PSL also allows a default clock specification, syntax of which is shown below.

// Using Verilog flavor.
default clock = (posedge clk);

a_with_implicit_clk : assert always {fifo_full |-> !wr_fifo};

a_with_explicit_clk : assert always {fifo_full |-> !wr_fifo} @(posedge clk);

Flvors, layers, examples

PSL is a multi-flavored, multi-layered language. This tutorial will walk through different layers in detail, but for the sake of simplicity will not focus on the different flavors. However the following few examples shall attempt in filling that gap.

The assertion example in Figure-1 is a Verilog flavored one, a similar one written in VHDL flavor will look like:

mutex_p  :   assert        always           not(rd and wr)       @(rising_edge(clk));

PSL is a well structured, layered language. It has four layers viz. boolean, temporal, verification and modeling layer. Each layer brings in a unique expressiveness to PSL. These layers are described in detail in later sections. A few quick start examples are shown below to demonstrate the concept of building PSL properties using individual layers. First a boolean expression is shown, as part of boolean layer. Temporal layer in PSL consists of SEREs/Sequences and properties. A simple sequence example shows how to build a sequence using boolean expressions as leaf elements. Then a property example is constructed using the previously defined sequences and combining them with Property operators. Finally, a verification directive (assert) is applied on the previously defined property to demonstrate the verification layer.

  -- BOOLEAN LAYER
  not (rd and wr); -- rd, wr are design signals.

-- TEMPORAL LAYER
-- Sequence definition
sequence s1 is {pkt_sop; (not pkt_xfer_en_n [*1 to 100]); pkt_eop};

sequence s2 is {pkt_sop; (not pkt_xfer_en_n [*1 to 100]); pkt_aborted};
-- In s1 and s2, the individual sequence elements (such as pkt_sop, 
-- pkt_xfer_en_n etc.) are design signals.

-- Property definition
property p1 is reset_cycle_ended |=> {s1; s2};

-- Property p1 uses previously defined sequences s1 and s2.

-- VERIFICATION LAYER
a1 : assert p1;

-- Verification directive is being used on a previously defined property p1.