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:
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.
PSL Golden Reference Guide: The perfect project companion for PSL
Get project ready in PSL with Assertion-based Verification using PSL