Property Specification Language Tutorial
(Part 3)
by
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;
endmodule
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
|