Property Specification Language Tutorial

Previous: Anatomy of a PSL Assertion | Next: Property Expressions: Temporal layer

Property Expressions

A property expression can be as simple as a boolean equation spanning just one clock cycle or can be a complex temporal SERE (Sequential Extended Regular Expression) spanning multiple (and possibly variable number of) cycles.

Property Expressions: Boolean Layer

The lowest level of any PSL property is a boolean expression, and PSL avoids re-inventing wheel here. It derives its boolean expressive power entirely from the underlying HDL. There are currently 4 different flavors defined in 1.1 version of LRM viz. Verilog, VHDL, SystemVerilog and GDL flavors. Of these the GDL flavor is more of a place holder for a generic description layer and is not completely developed yet. Recently a SystemC flavor is being proposed and also a 'portable PSL' that shall enable properties written in one flavor with a design described in a different flavor.

Verilog flavor

For Verilog, the following are few sample legal boolean expressions.

 		 mem_rd && mem_wr
		!pkt_sop || (pkt_stop && pkt_eop)

VHDL flavor

An equivalent expression of the same in VHDL flavor is shown below.

		 mem_rd and mem_wr
		 (not pkt_sop) or (pkt_sop and pkt_eop)
Infact most of the boolean layer is available as part of VHDL’s built-in assert construct.

As one can see, at the boolean layer, PSL looks quite similar to the underlying HDL and this is characteristic of PSL often referred to as language neutrality.

Next time:In Part 2 of this series, we will learn about the temporal layer of property expressions. This will consists of Sequences and Properties.

Previous: Anatomy of a PSL Assertion | Next: Property Expressions: Temporal layer


Verification Management
Join Verification Management Group

Shop Amazon - Contract Cell Phones & Service Plans

Book of the Month