The PSL language is formally structured into four distinct layers: the boolean, temporal, verification and modelling layers. The verification and temporal layers have a native syntax of their own, whereas the modelling and boolean layers borrow the syntax of the underlying HDL. Thus PSL is said to come in three flavours: VHDL, Verilog and GDL. The flavour directly determines the syntax used for the boolean and modelling layers and also has a small influence on the syntax of the temporal layer.
The boolean layer consists of boolean expressions containing variables and operators from the underlying language. Formally, the boolean layer consists of any expression that is allowed as the condition in an if statement in the underlying language. As such, expressions in the boolean layer are evaluated at a single point in time.
(a & (a-1)) == 0 // Verilog flavour (a and (a-1)) = 0 -- VHDL flavour
The temporal layer forms the major part of the PSL language. As well as including expressions from the boolean layer, expressions in the temporal layer may include temporal operators and Sequential Extended Regular Expressions or SEREs. It is usual for temporal expressions to be sampled on a clock. PSL is intended for designs with synchronous timing.
(always req -> next (ack until grant)) @clk
The verification layer consists of verification directives together with syntax to group PSL statements and bind them to HDL modules. A verification directive is an instruction to a tool to tell it what to do with a property. The principle verification directives are assert (the tool should attempt to prove the property), assume (the tool may assume the given property is true) and cover (the tool should measure how often the given property occurs during simulation).
assert (always req -> ack) @clk;
Verification directives such as the one above can be embedded in the HDL code as comments. Alternatively, verification directives can be grouped into verification units, or vunits, and placed in a separate file. There are actually three kinds of verification unit, with the vunit being the most general, the vprop containing nothing but assertions, and the vmode containing anything but assertions. A verification unit can be explicitly bound to an HDL module or design unit.
vunit my_properties(myVerilog.instance.name) {
assert (always req -> ack) @ clk;
assume (never req && reset)@ clk;
}
The modelling layer allows extra code fragments from the underlying language to be included with the properties to augment what is possible using PSL alone. For example, the modelling layer could be used to calculate the expected value of an output.
The modelling layer includes some additional language constructs and convenience functions. For example, the prev() function returns the value of an expression in the previous cycle. Currently, these functions are only part of the Verilog flavour modelling layer, but most tools unofficially support VHDL flavoured versions too.
PSL keywords are case sensitive. As you've probably noticed above, statements are terminated by a semi-colon ; .
Next: Simple Properties