Property Specification Language Tutorial

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)

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.