Property Specification Language (PSL) Grammar

IEEE Std 1850-2010

This document is copyrighted by the IEEE. It is made available for a wide variety of both public and private uses. These include both use, by reference, in laws and regulations, and use in private self-regulation, standardization, and the promotion of engineering practices and methods. By making this document available for use and adoption by public authorities and private users, the IEEE does not waive any rights in copyright to this document.
Get the full Language Reference Manual, at https://standards.ieee.org/findstds/standard/1850-2010.html
Sigasi has created this browsable version of the grammar, hoping that it would be useful to you, but without any warranty whatsoever.
More browsable grammars of Hardware Description and Verification languages.
## A.4 Syntax productions

The rest of this section defines the PSL syntax.

A.4.1 Verification units

PSL_Specification: { Verification_Item }
Verification_Item: HDL_UNIT
| Verification_Unit
Verification_Unit: Vunit_Type PSL_Identifier [ ( Hierarchical_HDL_Name ) ] { { Inherit_Spec } { Override_Spec } { VUnit_Item } }
Vunit_Type: vunit
| vpkg
| vprop
| vmode
Context_Spec: Binding_Spec
| Formal_Parameter_List
Binding_Spec: Hierarchical_HDL_Name
Hierarchical_HDL_Name: HDL_Module_Name { Path_Separator instance_Name }
HDL_Module_Name: HDL_Module_Name [ ( HDL_Module_Name ) ]
Path_Separator: .
| /
Instance_
Name: HDL_or_PSL_Identifier
Inherit_Spec: [ nontransitive ] inherit vunit_Name { , vunit_Name } ;
VUnit_Item: HDL_DECL
| HDL_STMT
| PSL_Declaration
| PSL_Directive
| Vunit_Instance
Vunit_Instance: Label : Vunit_Type vunit_Name [ ( Actual_Parameter_List ) ] ;
Override_Spec: override Name_List ;
Name_List: Name { , Name }
Formal_Parameter_List: Formal_Parameter { ; Formal_Parameter }

A.4.2 PSL declarations

PSL_Declaration: Property_Declaration
| Sequence_Declaration
| Clock_Declaration
Property_Declaration: property PSL_Identifier [ ( Formal_Parameter_List ) ] DEF_SYM Property ;
Formal_Parameter_List: Formal_Parameter { ; Formal_Parameter }
Formal_Parameter: Param_Spec PSL_Identifier { , PSL_Identifier }
Param_Spec: const
| [ const | mutable ] Value_Parameter
| sequence
| property
Value_Parameter: HDL_Type
| PSL_Type_Class
HDL_Type: hdltype HDL_VARIABLE_TYPE
PSL_Type_Class: boolean
| bit
| bitvector
| numeric
| string
Sequence_Declaration: sequence PSL_Identifier [ ( Formal_Parameter_List ) ] DEF_SYM Sequence ;
Clock_Declaration: default clock DEF_SYM Clock_Expression ;
Clock_Expression: boolean_Name
| boolean_Built_In_Function_Call
| ( Boolean )
| ( HDL_CLK_EXPR )
Actual_Parameter_List: Actual_Parameter { , Actual_Parameter }
Actual_Parameter: Any_Type
| Number
| Boolean
| Property
| Sequence

A.4.3 PSL directives

PSL_Directive: [ Label : ] Verification_Directive
Label: PSL_Identifier
HDL_or_PSL_Identifier: SystemVerilog_Identifier
| Verilog_Identifier
| VHDL_Identifier
| SystemC_Identifier
| GDL_Identifier
| PSL_Identifier
Verification_Directive: Assert_Directive
| Assume_Directive
| Restrict_Directive
| Restrict_Guarantee_Directive
| Cover_Directive
| Fairness_Statement
Assert_Directive: assert Property [ report String ] ;
Assume_Directive: assume Property ;
Restrict_Directive: restrict Sequence ;
Restrict_Guarantee_Directive: restrict! Sequence ;
Cover_Directive: cover Sequence [ report String ] ;
Fairness_Statement: fairness Boolean ;
| strong fairness Boolean , Boolean ;

A.4.4 PSL properties

Property: Replicator Property
| FL_Property
| OBE_Property
Replicator: forall Parameter_Definition :
Index_Range: LEFT_SYM finite_Range RIGHT_SYM
| ( HDL_RANGE )
Value_Set: { Value_Range { , Value_Range } }
| boolean
Value_Range: Value
| finite_Range
Value: Boolean
| Number
Proc_Block: [[ Proc_Block_Item { Proc_Block_Item } ]]
Proc_Block_Item: HDL_DECL
| HDL_SEQ_STMT
FL_Property: Boolean
| ( [ [[ HDL_DECL { , HDL_DECL } ]] ] FL_Property )
| Sequence [ ! ]
| FL_property_Name [ ( Actual_Parameter_List ) ]
| FL_Property @ Clock_Expression
| FL_Property abort Boolean
| FL_Property async_abort Boolean
| FL_Property sync_abort Boolean
| Parameterized_Property : Logical Operators :
| NOT_OP FL_Property
| FL_Property AND_OP FL_Property
| FL_Property OR_OP FL_Property ’:’
| FL_Property -> FL_Property
| FL_Property <-> FL_Property : Primitive LTL Operators :
| X FL_Property
| X! FL_Property
| F FL_Property
| G FL_Property
| [ FL_Property U FL_Property ]
| [ FL_Property W FL_Property ] : Simple Temporal Operators :
| always FL_Property
| never FL_Property
| next FL_Property
| next! FL_Property
| eventually! FL_Property ’:’
| FL_Property until! FL_Property
| FL_Property until FL_Property
| FL_Property until!_ FL_Property
| FL_Property until_ FL_Property : ’:’
| FL_Property before! FL_Property
| FL_Property before FL_Property
| FL_Property before!_ FL_Property
| FL_Property before_ FL_Property : Extended Next (Event) Operators :
| X [ Number ] ( FL_Property )
| X! [ Number ] ( FL_Property )
| next [ Number ] ( FL_Property )
| next! [ Number ] ( FL_Property ) ’:(see A.4.7)
| next_a [ finite_Range ] ( FL_Property )
| next_a! [ finite_Range ] ( FL_Property )
| next_e [ finite_Range ] ( FL_Property )
| next_e! [ finite_Range ] ( FL_Property ) ’:’
| next_event! ( Boolean ) ( FL_Property )
| next_event ( Boolean ) ( FL_Property )
| next_event! ( Boolean ) [ positive_Number ] ( FL_Property )
| next_event ( Boolean ) [ positive_Number ] ( FL_Property ) ’:’
| next_event_a! ( Boolean ) [ finite_positive_Range ] ( FL_Property )
| next_event_a ( Boolean ) [ finite_positive_Range ] ( FL_Property )
| next_event_e! ( Boolean ) [ finite_positive_Range ] ( FL_Property )
| next_event_e ( Boolean ) [ finite_positive_Range ] ( FL_Property ) : Operators on SEREs :
| { Sequence } ( FL_Property )
| Sequence |-> FL_Property
| Sequence |=> FL_Property

A.4.5 Sequential Extended Regular Expressions (SEREs)

SERE: Boolean
| Sequence
| Sequence_Instance
| SERE ; SERE
| SERE : SERE
| Compound_SERE
Compound_SERE: Repeated_SERE
| Braced_SERE
| Clocked_SERE
| Compound_SERE | Compound_SERE
| Compound_SERE & Compound_SERE
| Compound_SERE && Compound_SERE
| Compound_SERE within Compound_SERE
| Parameterized_SERE

A.4.6 Parameterized Properties and SEREs

Parameterized_Property: for Parameters_Definition : And_Or_Property_Op ( FL_Property )
Parameterized_SERE: for Parameters_Definition : And_Or_SERE_Op { SERE }
Parameters_Definition: Parameter_Definition { Parameter_Definition }
Parameter_Definition: PSL_Identifier [ Index_Range ] in Value_Set
And_Or_Property_Op: AND_OP
| OR_OP
And_Or_SERE_Op: &&
| &
| |

A.4.7 Sequences

Sequence: Sequence_Instance
| Repeated_SERE
| Braced_SERE
| Clocked_SERE
| Sequence Proc_Block
Repeated_SERE: Boolean [* [ Count ] ]
| Sequence [* [ Count ] ]
| [* [ Count ] ]
| Boolean [+]
| Sequence [+]
| [+]
| Boolean [= Count ]
| Boolean [-> [ positive_Count ] ]
| Boolean Proc_Block
| Sequence Proc_Block
Braced_SERE: { [ [[ HDL_DECL { HDL_DECL } ]] ] SERE }
| { [ free HDL_Identifier { HDL_Identifier } ] SERE }
Sequence_Instance: sequence_Name [ ( Actual_Parameter_List ) ]
Clocked_SERE: Braced_SERE @ Clock_Expression
Count: Number
| Range
Range: Low_Bound RANGE_SYM High_Bound
Low_Bound: Number
| MIN_VAL
High_Bound: Number
| MAX_VAL

A.4.8 Forms of expression

Any_Type: HDL_or_PSL_Expression
Bit: bitHDL_or_PSL_Expression
Boolean: booleanHDL_or_PSL_Expression
BitVector: bitvectorHDL_or_PSL_Expression
Number: numericHDL_or_PSL_Expression
String: string_HDL_or_PSL_Expression
HDL_or_PSL_Expression: HDL_Expression
| PSL_Expression
| Built_In_Function_Call
| Union_Expression
HDL_Expression: HDL_EXPR
PSL_Expression: Boolean -> Boolean
| Boolean <-> Boolean
Built_In_Function_Call: prev ( Any_Type [ , Number ] )
| next ( Any_Type )
| stable ( Any_Type )
| rose ( Bit )
| fell ( Bit )
| ended ( Sequence [ , Clock_Expression ] )
| isunknown ( BitVector )
| countones ( BitVector )
| onehot ( BitVector )
| onehot0 ( BitVector )
| nondet ( Value_Set )
| nondet_vector ( Number , Value_Set )
Union_Expression: Any_Type union Any_Type

A.4.9 Optional branching extension

OBE_Property: Boolean
| ( OBE_Property )
| property_Name [ ( Actual_Parameter_List ) ] : Logical Operators :
| NOT_OP OBE_Property
| OBE_Property AND_OP OBE_Property
| OBE_Property OR_OP OBE_Property
| OBE_Property -> OBE_Property
| OBE_Property <-> OBE_Property : Universal Operators :
| AX OBE_Property
| AG OBE_Property
| AF OBE_Property
| A [ OBE_Property U OBE_Property ] : Existential Operators :
| EX OBE_Property
| EG OBE_Property
| EF OBE_Property
| E [ OBE_Property U OBE_Property ]

VHDL Flavor macros

DEF_SYM: is
RANGE_SYM: to
AND_OP: and
OR_OP: or
NOT_OP: not
MIN_VAL: 0
MAX_VAL: inf
HDL_EXPR: Extended_VHDL_Expression
HDL_CLK_EXPR: VHDL_expression
HDL_UNIT: VHDL_design_unit
HDL_MOD_NAME: entity_aspect
HDL_DECL: VHDL_block_declarative_item
HDL_STMT: VHDL_concurrent_statement
HDL_SEQ_STMT: VHDL_sequential_statement
HDL_RANGE: range_attribute_name
HDL_VARIABLE_TYPE: VHDL_subtype_indication
LEFT_SYM: (
RIGHT_SYM: )
Identifier: ID