Property Specification Language Tutorial

(Part 3)


Ajeetha Kumari

Previous: Property Expression: Properties | Next: Miscelleneous

Property Expressions: Verification Layer

Verification Directives

Properties are just declarations and they must be directed by a verification directive in-order to direct a verification tool to check/assume for the validity of the property. PSL supports the following directives:

  • assert
  • assume
  • assume_guarantee
  • cover
  • restrict
  • restrict_guarantee
  • fairness
  • strong_fairness

Among these, the assert and cover are the most frequently used in simulation based ABV. Other directives are mostly used in Formal Verification.

The assert directive instructs the tool to check that the property being asserted holds and if not to report a failure. The cover directive is used to specify valid legal behaviors and checking for their occurrence in simulation, in other words it is used to capture control centric functional coverage points.

PSL allows labeling of such directives and is a good coding style to use descriptive labels for them.

Verification Units

PSL is a property language that talks about the design and needs to be linked to a design unit (say RTL model) in order for a tool to check that the design meets the requirements as described by PSL properties. PSL supports a set of verification units as containers of properties so that a set of properties can be linked to a design. Of these, vunit is the most commonly used and is described below.

Using vunit

A vunit is used as a container for PSL properties.

vunit v1 {

property pkt_xfer 
   = {pkt_sop; pkt_xfer_in_progress[*1:100];pkt_abort} @posedge clk;

a1 : assert pkt_xfer;
} // vunit v1
Now, in the above property, there are various signals used in the basic boolean expressions that are expected to be existing in a RTL design. The link to the design under test occurs via an argument to the vunit specification. These properties can be either bound to a design module or an instance of a module.
vunit v1 (module_name) {

vunit v2 (top.chip.ctl_unit.pkt_processor) {
} // v2

Adding properties 'inline' in RTL

Often RTL designers find it convenient to inline simple assertions, assumptions along with their RTL code. PSL LRM does not specify how this can be done, but a pseudo-standard is adopted by various EDA vendors to use a pragma based approach. In a Verilog RTL, one can use:

  module proc_eng();
    reg clk,a,b;
    // psl a1 : assert always (a |-> b) @posedge clk;
Similarly in a VHDL design, one can use -- psl pragma.

Property Expressions: Modeling Layer

Though PSL is very capable of capturing certain classes of properties, it requires some additional helper code at times to model auxiliary combinational signals, state machines etc. that are not part of the actual design but are rather required to express the property in a concise manner. PSL uses underlying HDL to model such code. PSL LRM requires that such code be restricted to synthesizable sub-set of the HDL. A simple example is shown below in Verilog flavor.

vunit v1 (dut) {
// Signal a_and_b is purely for a verification purpose.
wire a_and_b = sig_a && sig_b;

a_and_b_ohot : assert always onehot(a_and_b) @ (posedge clk);
} // v1

Previous: Property Expression: Properties | Next: Miscelleneous


Verification Management
Join Verification Management Group

Shop Amazon - Contract Cell Phones & Service Plans

Book of the Month