PSL is an abbreviation for Property Specification Language. A property is a boolean-valued fact about a design-under-test. Right now, PSL works alongside a design written in VHDL or Verilog, but in future PSL may be extended to work with other languages. Properties written in PSL may be embedded within the HDL code as comments or may be placed in a separate file alongside the HDL code.
Properties are used to create assertions. An assertion is an instruction to a verification tool to prove that a given property holds. The verification tool could be a simulator (dynamic verification) or a model checker that constructs a mathematical proof of a property (static formal verification).
Properties can play a number of different roles in verification:
- Monitors that dynamically check the state of the design during simulation
- Constraints that define legal sequences of input vectors for simulation
- Functional coverage points that allow the completeness of simulation to be measured
- Assertions to be proved by static formal property checkers
- Assumptions to be made by static formal property checkers when proving assertions
Properties in PSL are composed of boolean expressions written in the host language (VHDL or Verilog) together with temporal operators and sequences native to PSL. The boolean expressions enable PSL to sample the state of the HDL design at a particular point in time, whilst the temporal operators and sequences describe the relationship between states over time. What PSL brings to the underlying HDL is the ability to describe temporal relationships clearly and concisely.
With future extension in mind, PSL also allows expressions to be written in a neutral formal called GDL (for General Description Language) in addition to VHDL and Verilog.
