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
external VHDL_expression
HDL_UNIT
external VHDL_design_unit
HDL_MOD_NAME
entity_aspect
HDL_DECL
external VHDL_block_declarative_item
HDL_STMT
external VHDL_concurrent_statement
HDL_SEQ_STMT
external VHDL_sequential_statement
HDL_RANGE
range_attribute_name
HDL_VARIABLE_TYPE
external VHDL_subtype_indication
LEFT_SYM
(
RIGHT_SYM
)
Identifier
ID