-
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, symbolic 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 && 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; (!pkt_xfer_en_n [*1 to 100]); pkt_eop};
sequence s2 is {pkt_sop; (!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.