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
See also
- VHDL IEEE 1076-2017 Grammar (blog post)
- Sigasi Studio Graphics Configuration Grammar (legacy)
- Register Description Language SystemRDL 2.0 (blog post)
- Portable Test and Stimulus Standard Version 1.0 (blog post)
- SystemVerilog IEEE 1800-2012 Grammar (blog post)