PSL Four-Level Syntax Structure

The abstract syntax of PSL uses for levels:

• Since the language is embedded in the concrete syntax of several other languages, such as Verilog, SystemVerilog and VHDL, its syntactic details vary. In particular, creating state predicates involves expressions that range over the nets and variables of the host language. The precise means for this is defined by the MODELLING LAYER that allows one to create state properties using RTL.

  Non-boolean sub-expressions can be used in the modelling layer to generate boolean state predicates.

     assign tempok = temperature < 99;
  

• All high-level languages and RTLs have their own syntax for boolean operators and this can be used within the modelling layer. However boolean combinations can also be formed using the PSL BOOLEAN LAYER.

      not (rd and wr); -- rd, wr are nets in the RTL (modelling layer).
  

• The PSL TEMPORAL LAYER allows one to define named sub-expressions and properties that use the temporal operators. For example:

     -- Sequence definition
     sequence s1 is {pkt_sop; (not pkt_xfer_en_n [*1 to 100]); pkt_eop};
  
     sequence s2 is {pkt_sop; (not pkt_xfer_en_n [*1 to 100]); pkt_aborted};
  
     -- Property definition
     property p1 is reset_cycle_ended |=> {s1; s2};
  
     -- Property p1 uses previously defined sequences s1 and s2.
  

• The PSL VERIFICATION LAYER implements the declarative language itself. It includes the main keywords, such as assert.