Annex A
    Formal Syntax

(Normative)

The formal syntax of SystemVerilog is described using Backus-Naur Form (BNF). The conventions used are:

The full syntax and semantics of Verilog and SystemVerilog are not described solely using BNF. The normative text description contained within the chapters of the IEEE 1364-2001 Verilog standard and this SystemVerilog document provide additional details on the syntax and semantics described in this BNF.

A.1 Source text

A.1.1 Library source text

library_text ::= { library_descriptions }

library_descriptions ::=
library_declaration
| include_statement
| config_declaration

library_declaration ::=
library library_identifier file_path_spec { , file_path_spec }
[ -incdir file_path_spec { , file_path_spec } ] ;

file_path_spec ::= file_path

include_statement ::= include <file_path_spec> ;

A.1.2 Configuration source text

config_declaration ::=
config config_identifier ;
design_statement
{ config_rule_statement }
endconfig

design_statement ::= design { [ library_identifier . ] cell_identifier } ;

config_rule_statement ::=
default_clause liblist_clause
| inst_clause liblist_clause
| inst_clause use_clause
| cell_clause liblist_clause
| cell_clause use_clause

default_clause ::= default

inst_clause ::= instance inst_name

inst_name ::= topmodule_identifier { . instance_identifier }

cell_clause ::= cell [ library_identifier . ] cell_identifier

liblist_clause ::= liblist {library_identifier}

use_clause ::= use [ library_identifier . ] cell_identifier [ : config ]

A.1.3 Module and primitive source text

source_text ::= [ timeunits_declaration ] { description }

description ::=
module_declaration
| udp_declaration
| module_root_item
| statement_or_null

module_nonansi_header ::=
{ attribute_instance } module_keyword [ lifetime ] module_identifier [ parameter_port_list ]
list_of_ports ;

module_ansi_header ::=
{ attribute_instance } module_keyword [ lifetime ] module_identifier [ parameter_port_list ]
[ list_of_port_declarations ] ;

module_declaration ::=
module_nonansi_header [ timeunits_declaration ] { module_item }
endmodule [ : module_identifier ]
| module_ansi_header [ timeunits_declaration ] { non_port_module_item }
endmodule [ : module_identifier ]
| { attribute_instance } module_keyword [ lifetime ] module_identifier ( .* ) ;
[ timeunits_declaration ] { module_item } endmodule [ : module_identifier ]
| extern module_nonansi_header
| extern module_ansi_header

module_keyword ::= module | macromodule

interface_nonansi_header ::=
{ attribute_instance } interface [ lifetime ] interface_identifier
[ parameter_port_list ] list_of_ports ;

interface_ansi_header ::=
{attribute_instance } interface [ lifetime ] interface_identifier
[ parameter_port_list ] [ list_of_port_declarations ] ;

interface_declaration ::=
interface_nonansi_header [ timeunits_declaration ] { interface_item }
endinterface [ : interface_identifier ]
| interface_ansi_header [ timeunits_declaration ] { non_port_interface_item }
endinterface [ : interface_identifier ]
| { attribute_instance } interface interface_identifier ( .* ) ;
[ timeunits_declaration ] { interface_item }
endinterface [ : interface_identifier ]
| extern interface_nonansi_header
| extern interface_ansi_header

program_nonansi_header ::=
{ attribute_instance } program [ lifetime ] program_identifier
[ parameter_port_list ] list_of_ports ;

program_ansi_header ::=
{attribute_instance } program [ lifetime ] program_identifier
[ parameter_port_list ] [ list_of_port_declarations ] ;

program_declaration ::=
program_nonansi_header [ timeunits_declaration ] { program_item }
endprogram [ : program_identifier ]
| program_ansi_header [ timeunits_declaration ] { non_port_program_item }
endprogram [ : program_identifier ]
| { attribute_instance } program program_identifier ( .* ) ;
[ timeunits_declaration ] { program_item }
endprogram [ : program_identifier ]
| extern program_nonansi_header
| extern program_ansi_header

class_declaration ::=
{ attribute_instance } [ virtual ] class [ lifetime ] class_identifier [ parameter_port_list ]
[ extends class_identifier ] ; [ timeunits_declaration ] { class_item }
endclass [ : class_identifier]

timeunits_declaration ::=
timeunit time_literal ;
| timeprecision time_literal ;
| timeunit time_literal ;
timeprecision time_literal ;
| timeprecision time_literal ;
timeunit time_literal ;

A.1.4 Module parameters and ports

parameter_port_list ::= # ( parameter_declaration { , parameter_declaration } )

list_of_ports ::= ( port { , port } )

list_of_port_declarations ::=
( port_declaration { , port_declaration } )
| ( )

non_generic_port_declaration ::=
{ attribute_instance } inout_declaration
| { attribute_instance } input_declaration
| { attribute_instance } output_declaration
| { attribute_instance } ref_declaration
| { attribute_instance } interface_port_declaration

port ::=
[ port_expression ]
| . port_identifier ( [ port_expression ] )

port_expression ::=
port_reference
| { port_reference { , port_reference } }

port_reference ::=
port_identifier [ [ constant_range_expression ] ]

port_declaration ::=
non_generic_port_declaration
| { attribute_instance } generic_interface_port_declaration

A.1.5 Module items

module_common_item ::=
{ attribute_instance } module_or_generate_item_declaration
| { attribute_instance } interface_instantiation
| { attribute_instance } program_instantiation
| { attribute_instance } concurrent_assertion_item
| { attribute_instance } bind_directive

module_item ::=
non_generic_port_declaration ;
| non_port_module_item

module_or_generate_item ::=
{ attribute_instance } parameter_override
| { attribute_instance } continuous_assign
| { attribute_instance } gate_instantiation
| { attribute_instance } udp_instantiation
| { attribute_instance } module_instantiation
| { attribute_instance } initial_construct
| { attribute_instance } always_construct
| { attribute_instance } combinational_construct
| { attribute_instance } latch_construct
| { attribute_instance } ff_construct
| { attribute_instance } net_alias
| { attribute_instance } final_construct
| module_common_item
| { attribute_instance } ;

module_root_item ::=
{ attribute_instance } module_instantiation
| { attribute_instance } local_parameter_declaration
| interface_declaration
| program_declaration
| class_declaration
| module_common_item

module_or_generate_item_declaration ::=
net_declaration
| data_declaration
| genvar_declaration
| task_declaration
| function_declaration
| dpi_import_export
| extern_constraint_declaration
| extern_method_declaration
| clocking_decl
| default clocking clocking_identifier ;

non_port_module_item ::=
{ attribute_instance } generated_module_instantiation
| { attribute_instance } local_parameter_declaration
| module_or_generate_item
| { attribute_instance } parameter_declaration ;
| { attribute_instance } specify_block
| { attribute_instance } specparam_declaration
| program_declaration
| class_declaration
| module_declaration

parameter_override ::= defparam list_of_defparam_assignments ;

bind_directive ::=
bind module_identifier bind_instantiation ;
| bind name_of_instance bind_instantiation ;

bind_instantiation ::=
program_instantiation
| module_instantiation
| interface_instantiation

A.1.6 Interface items

interface_or_generate_item ::=
{ attribute_instance } continuous_assign
| { attribute_instance } initial_construct
| { attribute_instance } always_construct
| { attribute_instance } combinational_construct
| { attribute_instance } latch_construct
| { attribute_instance } ff_construct
| { attribute_instance } local_parameter_declaration
| { attribute_instance } parameter_declaration ;
| module_common_item
| { attribute_instance } modport_declaration
| { attribute_instance } extern_tf_declaration
| { attribute_instance } final_construct
| { attribute_instance } ;

extern_tf_declaration ::=
extern method_prototype
| extern forkjoin task named_task_proto ;

interface_item ::=
non_generic_port_declaration ;
| non_port_interface_item

non_port_interface_item ::=
{ attribute_instance } generated_interface_instantiation
| { attribute_instance } specparam_declaration
| interface_or_generate_item
| program_declaration
| class_declaration
| interface_declaration

A.1.7 Program items

program_item ::=
port_declaration ;
| non_port_program_item

non_port_program_item ::=
{ attribute_instance } continuous_assign
| { attribute_instance } module_or_generate_item_declaration
| { attribute_instance } specparam_declaration
| { attribute_instance } local_parameter_declaration
| { attribute_instance } parameter_declaration ;
| { attribute_instance } initial_construct
| { attribute_instance } concurrent_assertion_item
| class_declaration

A.1.8 Class items

class_item ::=
{ attribute_instance } class_property
| { attribute_instance } class_method
| { attribute_instance } class_constraint

class_property ::=
{ property_qualifier } data_declaration
| const { class_item_qualifier } data_type const_identifier [ = constant_expression ] ;

class_method ::=
{ method_qualifier } task_declaration
| { method_qualifier } function_declaration
| extern { method_qualifier } method_prototype

class_constraint ::=
constraint_prototype
| constraint_declaration

class_item_qualifier 11 ::=
static
| protected
| local

property_qualifier 11 ::=
rand
| randc
| class_item_qualifier

method_qualifier 11 ::=
virtual
| class_item_qualifier

method_prototype ::=
task named_task_proto ;
| function named_function_proto ;

extern_method_declaration ::=
function [ lifetime ] class_identifier :: function_body_declaration
| task [ lifetime ] class_identifier :: task_body_declaration

A.1.9 Constraints

constraint_declaration ::= [ static ] constraint constraint_identifier { { constraint_block } }

constraint_block ::=
solve identifier_list before identifier_list ;
| expression dist { dist_list } ;
| constraint_expression

constraint_expression ::=
expression ;
| expression => constraint_set
| if ( expression ) constraint_set [ else constraint_set ]

constraint_set ::=
constraint_expression
| { { constraint_expression } }

dist_list ::= dist_item { , dist_item }

dist_item ::=
value_range := expression
| value_range :/ expression

constraint_prototype ::= [ static ] constraint constraint_identifier

extern_constraint_declaration ::=
[ static ] constraint class_identifier :: constraint_identifier { { constraint_block } }

identifier_list ::= identifier { , identifier }

A.2 Declarations

A.2.1 Declaration types

A.2.1.1 Module parameter declarations

local_parameter_declaration ::=
localparam [ signing ] { packed_dimension } [ range ] list_of_param_assignments ;
| localparam data_type list_of_param_assignments ;

parameter_declaration ::=
parameter [ signing ] { packed_dimension } [ range ] list_of_param_assignments
| parameter data_type list_of_param_assignments
| parameter type list_of_type_assignments

specparam_declaration ::=
specparam [ range ] list_of_specparam_assignments ;

A.2.1.2 Port declarations

inout_declaration ::=
inout [ port_type ] list_of_port_identifiers
| inout data_type list_of_variable_identifiers

input_declaration ::=
input [ port_type ] list_of_port_identifiers
| input data_type list_of_variable_identifiers

output_declaration ::=
output [ port_type ] list_of_port_identifiers
| output data_type list_of_variable_port_identifiers

interface_port_declaration ::=
interface_identifier list_of_interface_identifiers
| interface_identifier . modport_identifier list_of_interface_identifiers

ref_declaration ::= ref data_type list_of_port_identifiers

generic_interface_port_declaration ::=
interface list_of_interface_identifiers
| interface . modport_identifier list_of_interface_identifiers

A.2.1.3 Type declarations

block_data_declaration ::=
block_variable_declaration
| constant_declaration
| type_declaration

constant_declaration ::= const data_type const_assignment ;

data_declaration ::=
variable_declaration
| constant_declaration
| type_declaration

genvar_declaration ::= genvar list_of_genvar_identifiers ;

net_declaration ::=
net_type [ signing ]
[ delay3 ] list_of_net_identifiers ;
| net_type [ drive_strength ] [ signing ]
[ delay3 ] list_of_net_decl_assignments ;
| net_type [ vectored | scalared ] [ signing ]
{ packed_dimension } range [ delay3 ] list_of_net_identifiers ;
| net_type [ drive_strength ] [ vectored | scalared ] [ signing ]
{ packed_dimension } range [ delay3 ] list_of_net_decl_assignments ;
| trireg [ charge_strength ] [ signing ]
[ delay3 ] list_of_net_identifiers ;
| trireg [ drive_strength ] [ signing ]
[ delay3 ] list_of_net_decl_assignments ;
| trireg [ charge_strength ] [ vectored | scalared ] [ signing ]
{ packed_dimension } range [ delay3 ] list_of_net_identifiers ;
| trireg [ drive_strength ] [ vectored | scalared ] [ signing ]
{ packed_dimension } range [ delay3 ] list_of_net_decl_assignments ;

type_declaration ::=
typedef [ data_type ] type_declaration_identifier ;
| typedef hierarchical_identifier . type_identifier type_declaration_identifier ;
| typedef [ class ] class_identifier ;
| typedef class_identifier [ parameter_value_assignment ] type_declaration_identifier ;

block_variable_declaration ::=
[ lifetime ] data_type list_of_variable_identifiers ;
| lifetime data_type list_of_variable_decl_assignments ;

variable_declaration ::=
[ lifetime ] data_type list_of_variable_identifiers_or_assignments ;

lifetime ::= static | automatic

A.2.2 Declaration data types

A.2.2.1 Net and variable types

casting_type ::= simple_type | number | signing

data_type ::=
integer_vector_type [ signing ] { packed_dimension } [ range ]
| integer_atom_type [ signing ]
| type_declaration_identifier { packed_dimension }
| non_integer_type
| struct packed [ signing ] { { struct_union_member } } { packed_dimension }
| union packed [ signing ] { { struct_union_member } } { packed_dimension }
| struct [ signing ] { { struct_union_member } }
| union [ signing ] { { struct_union_member } }
| enum [ integer_type [ signing ] { packed_dimension } ]
{ enum_identifier [ = constant_expression ] { , enum_identifier [ = constant_expression ] } }
| string
| event
| chandle
| class_scope_type_identifier

class_scope_type_identifier::=
class_identifier :: { class_identifier :: } type_declaration_identifier
| class_identifier :: { class_identifier :: } class_identifier

integer_type ::= integer_vector_type | integer_atom_type

integer_atom_type ::= byte | shortint | int | longint | integer

integer_vector_type ::= bit | logic | reg

non_integer_type ::= time | shortreal | real | realtime

net_type ::= supply0 | supply1 | tri | triand | trior | tri0 | tri1 | wire | wand | wor

port_type ::=
data_type
| net_type [ signing ] { packed_dimension }
| trireg [ signing ] { packed_dimension }
| [ signing ] { packed_dimension } range

signing ::= signed | unsigned

simple_type ::= integer_type | non_integer_type | type_identifier

struct_union_member ::= { attribute_instance } data_type list_of_variable_identifiers_or_assignments ;

A.2.2.2 Strengths

drive_strength ::=
( strength0 , strength1 )
| ( strength1 , strength0 )
| ( strength0 , highz1 )
| ( strength1 , highz0 )
| ( highz0 , strength1 )
| ( highz1 , strength0 )

strength0 ::= supply0 | strong0 | pull0 | weak0

strength1 ::= supply1 | strong1 | pull1 | weak1

charge_strength ::= ( small ) | ( medium ) | ( large )

A.2.2.3 Delays

delay3 ::= # delay_value | # ( mintypmax_expression [ , mintypmax_expression [ , mintypmax_expression ] ] )

delay2 ::= # delay_value | # ( mintypmax_expression [ , mintypmax_expression ] )

delay_value ::=
unsigned_number
| real_number
| identifier

A.2.3 Declaration lists

list_of_defparam_assignments ::= defparam_assignment { , defparam_assignment }

list_of_genvar_identifiers ::= genvar_identifier { , genvar_identifier }

list_of_interface_identifiers ::= interface_identifier { unpacked_dimension }
{ , interface_identifier { unpacked_dimension } }

list_of_modport_port_identifiers ::= port_identifier { , port_identifier }

list_of_net_decl_assignments ::= net_decl_assignment { , net_decl_assignment }

list_of_net_identifiers ::= net_identifier { unpacked_dimension }
{ , net_identifier { unpacked_dimension } }

list_of_param_assignments ::= param_assignment { , param_assignment }

list_of_port_identifiers ::= port_identifier { unpacked_dimension }
{ , port_identifier { unpacked_dimension } }

list_of_udp_port_identifiers ::= port_identifier { , port_identifier }

list_of_specparam_assignments ::= specparam_assignment { , specparam_assignment }

list_of_tf_port_identifiers ::= port_identifier { unpacked_dimension } [ = expression ]
{ , port_identifier { unpacked_dimension } [ = expression ] }

list_of_tf_variable_identifiers ::= port_identifier variable_dimension [ = expression ]
{ , port_identifier variable_dimension [ = expression ] }

list_of_type_assignments ::= type_assignment { , type_assignment }

list_of_variable_decl_assignments ::= variable_decl_assignment { , variable_decl_assignment }

list_of_variable_identifiers ::= variable_identifier variable_dimension
{ , variable_identifier variable_dimension }

list_of_variable_identifiers_or_assignments ::=
list_of_variable_decl_assignments
| list_of_variable_identifiers

list_of_variable_port_identifiers ::= port_identifier variable_dimension [ = constant_expression ]
{ , port_identifier variable_dimension [ = constant_expression ] }

A.2.4 Declaration assignments

const_assignment ::= const_identifier = constant_expression

defparam_assignment ::= hierarchical_parameter_identifier = constant_expression

net_decl_assignment ::= net_identifier = expression

param_assignment ::= parameter_identifier = constant_param_expression

specparam_assignment ::=
specparam_identifier = constant_mintypmax_expression
| pulse_control_specparam

type_assignment ::= type_identifier = data_type

pulse_control_specparam ::=
PATHPULSE$ = ( reject_limit_value [ , error_limit_value ] ) ;
| PATHPULSE$ specify_input_terminal_descriptor $ specify_output_terminal_descriptor
= ( reject_limit_value [ , error_limit_value ] ) ;

error_limit_value ::= limit_value

reject_limit_value ::= limit_value

limit_value ::= constant_mintypmax_expression

variable_decl_assignment ::=
variable_identifier [ variable_dimension ] [ = constant_expression ]
| variable_identifier [ ] = new [ constant_expression ] [ ( variable_identifier ) ]
| class_identifier [ parameter_value_assignment ] = new [ ( list_of_arguments ) ]

A.2.5 Declaration ranges

unpacked_dimension ::= [ dimension_constant_expression : dimension_constant_expression ]
| [ dimension_constant_expression ]

packed_dimension 9 ::=
[ dimension_constant_expression : dimension_constant_expression ]
| [ ]

range ::= [ msb_constant_expression : lsb_constant_expression ]

associative_dimension ::=
[ data_type ]
| [ * ]

variable_dimension ::=
{ unpacked_dimension }
| [ ]
| associative_dimension

dpi_dimension ::=
variable_dimension
| { [ ] }

A.2.6 Function declarations

function_data_type 8 ::=
integer_vector_type { packed_dimension } [ range ]
| integer_atom_type
| type_declaration_identifier { packed_dimension }
| non_integer_type
| struct [ packed ] { { struct_union_member } } { packed_dimension }
| union [ packed ] { { struct_union_member } } { packed_dimension }
| enum [ integer_type { packed_dimension } ]
{ enum_identifier [ = constant_expression ] { , enum_identifier [ = constant_expression ] } }
| string
| chandle
| void

function_body_declaration ::=
[ signing ] [ range_or_type ]
[ interface_identifier . ] function_identifier ;
{ function_item_declaration }
{ function_statement_or_null }
endfunction [ : function_identifier ]
| [ signing ] [ range_or_type ]
[ interface_identifier . ] function_identifier ( function_port_list ) ;
{ block_item_declaration }
{ function_statement_or_null }
endfunction [ : function_identifier ]

function_declaration ::=
function [ lifetime ] function_body_declaration

function_item_declaration ::=
block_item_declaration
| { attribute_instance } tf_input_declaration ;
| { attribute_instance } tf_output_declaration ;
| { attribute_instance } tf_inout_declaration ;
| { attribute_instance } tf_ref_declaration ;

function_port_item ::=
{ attribute_instance } tf_input_declaration
| { attribute_instance } tf_output_declaration
| { attribute_instance } tf_inout_declaration
| { attribute_instance } tf_ref_declaration
| { attribute_instance } port_type list_of_tf_port_identifiers
| { attribute_instance } tf_data_type list_of_tf_variable_identifiers

function_port_list ::= function_port_item { , function_port_item }

named_function_proto::= [ signing ] function_data_type function_identifier ( list_of_function_proto_formals )

list_of_function_proto_formals ::=
[ { attribute_instance } function_proto_formal { , { attribute_instance } function_proto_formal } ]

function_proto_formal ::=
tf_input_declaration
| tf_output_declaration
| tf_inout_declaration
| tf_ref_declaration

range_or_type ::=
{ packed_dimension } range
| function_data_type

dpi_import_export ::=
import "DPI" [ dpi_import_property ] [ c_identifier = ] dpi_function_proto ;
| export "DPI" [ c_identifier = ] function function_identifier ;

dpi_import_property ::= context | pure

dpi_function_proto ::=
named_function_proto
| [ signing ] function_data_type function_identifier ( list_of_dpi_proto_formals )

list_of_dpi_proto_formals ::=
[ { attribute_instance } dpi_proto_formal { , { attribute_instance } dpi_proto_formal } ]

dpi_proto_formal ::=
data_type [ port_identifier dpi_dimension { , port_identifier dpi_dimension } ]

A.2.7 Task declarations

task_body_declaration ::=
[ interface_identifier . ] task_identifier ;
{ task_item_declaration }
{ statement_or_null }
endtask [ : task_identifier ]
| [ interface_identifier . ] task_identifier ( task_port_list ) ;
{ block_item_declaration }
{ statement_or_null }
endtask [ : task_identifier ]

task_declaration ::= task [ lifetime ] task_body_declaration

task_item_declaration ::=
block_item_declaration
| { attribute_instance } tf_input_declaration ;
| { attribute_instance } tf_output_declaration ;
| { attribute_instance } tf_inout_declaration ;
| { attribute_instance } tf_ref_declaration ;

task_port_list ::= task_port_item { , task_port_item }
| list_of_port_identifiers { , task_port_item }

task_port_item ::=
{ attribute_instance } tf_input_declaration
| { attribute_instance } tf_output_declaration
| { attribute_instance } tf_inout_declaration
| { attribute_instance } tf_ref_declaration ;
| { attribute_instance } port_type list_of_tf_port_identifiers
| { attribute_instance } tf_data_type list_of_tf_variable_identifiers

tf_input_declaration ::=
input [ signing ] { packed_dimension } list_of_tf_port_identifiers
| input tf_data_type list_of_tf_variable_identifiers

tf_output_declaration ::=
output [ signing ] { packed_dimension } list_of_tf_port_identifiers
| output tf_data_type list_of_tf_variable_identifiers

tf_inout_declaration ::=
inout [ signing ] { packed_dimension } list_of_tf_port_identifiers
| inout tf_data_type list_of_tf_variable_identifiers

tf_ref_declaration ::=
[ const ] ref tf_data_type list_of_tf_variable_identifiers

tf_data_type ::=
data_type
| chandle

named_task_proto ::= task_identifier ( task_proto_formal { , task_proto_formal } )

task_proto_formal ::=
tf_input_declaration
| tf_output_declaration
| tf_inout_declaration
| tf_ref_declaration

A.2.8 Block item declarations

block_item_declaration ::=
{ attribute_instance } block_data_declaration
| { attribute_instance } local_parameter_declaration
| { attribute_instance } parameter_declaration ;

A.2.9 Interface declarations

modport_declaration ::= modport modport_item { , modport_item } ;

modport_item ::= modport_identifier ( modport_ports_declaration { , modport_ports_declaration } )

modport_ports_declaration ::=
modport_simple_ports_declaration
| modport_hierarchical_ports_declaration
| modport_tf_ports_declaration

modport_simple_ports_declaration ::=
input list_of_modport_port_identifiers
| output list_of_modport_port_identifiers
| inout list_of_modport_port_identifiers
| ref [ data_type ] list_of_modport_port_identifiers

modport_hierarchical_ports_declaration ::=
interface_instance_identifier [ [ constant_expression ] ] . modport_identifier

modport_tf_ports_declaration ::=
import_export modport_tf_port

modport_tf_port ::=
task named_task_proto { , named_task_proto }
| function named_function_proto { , named_function_proto }
| task_or_function_identifier { , task_or_function_identifier }

import_export ::= import | export

A.2.10 Assertion declarations

concurrent_assertion_item ::=
concurrent_assert_statement
| concurrent_cover_statement
| concurrent_assertion_item_declaration

concurrent_assert_statement ::=
[block_identifier : ] assert_property_statement

concurrent_cover_statement ::=
[block_identifier : ] cover_property_statement

assert_property_statement::=
assert property ( property_spec ) action_block
| assert property ( property_instance ) action_block

cover_property_statement::=
cover property ( property_spec ) statement_or_null
| cover property ( property_instance ) statement_or_null

property_instance ::=
property_identifier [ ( actual_arg_list ) ]

concurrent_assertion_item_declaration ::=
property_declaration
| sequence_declaration

property_declaration ::=
property property_identifier [ property_formal_list ] ;
{ assertion_variable_declaration }
property_spec ;
endproperty [ : property_identifier ]

property_formal_list ::=
( formal_list_item { , formal_list_item } )

property_spec ::=
[clocking_event ] [ disable iff ] ( expression ) [ not ] property_expr
| [ disable iff ( expression ) ] [ not ] multi_clock_property_expr

property_expr ::=
sequence_expr
| sequence_expr |-> [ not ] sequence_expr
| sequence_expr |=> [ not ] sequence_expr
| ( property_expr )

multi_clock_property_expr ::=
multi_clock_sequence
| multi_clock_sequence |=> [ not ] multi_clock_sequence
| ( multi_clock_property_expr )

sequence_declaration ::=
sequence sequence_identifier [ sequence_formal_list ] ;
{ assertion_variable_declaration }
sequence_spec ;
endsequence [ : sequence_identifier ]

sequence_formal_list ::=
( formal_list_item { , formal_list_item } )

sequence_spec ::=
multi_clock_sequence
| sequence_expr

multi_clock_sequence::=
clocked_sequence { ## clocked_sequence }

clocked_sequence ::=
clocking_event sequence_expr

sequence_expr ::=
cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }
| sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }
| expression { , function_blocking_assignment } [ boolean_abbrev ]
| ( expression { , function_blocking_assignment } ) [ boolean_abbrev ]
| sequence_instance [ sequence_abbrev ]
| ( sequence_expr ) [ sequence_abbrev ]
| sequence_expr and sequence_expr
| sequence_expr intersect sequence_expr
| sequence_expr or sequence_expr
| first_match ( sequence_expr )
| expression throughout sequence_expr
| sequence_expr within sequence_expr

cycle_delay_range ::=
## constant_expression
| ## [ cycle_delay_const_range_expression ]

sequence_instance ::=
sequence_identifier [ ( actual_arg_list ) ]

formal_list_item ::=
formal_identifier [ = actual_arg_expr ]

actual_arg_list ::=
( actual_arg_expr { , actual_arg_expr } )
| ( . formal_identifier ( actual_arg_expr ) { , . formal_identifier ( actual_arg_expr ) } )

actual_arg_expr ::=
event_expression

boolean_abbrev ::=
consecutive_repetition
| non_consecutive_repetition
| goto_repetition

sequence_abbrev ::= consecutive_repetition

consecutive_repetition ::= [* const_or_range_expression ]

non_consecutive_repetition ::= [*= const_or_range_expression ]

goto_repetition ::= [*-> const_or_range_expression ]

const_or_range_expression ::=
constant_expression
| cycle_delay_const_range_expression

cycle_delay_const_range_expression ::=
constant_expression : constant_expression
| constant_expression : $

assertion_variable_declaration ::=
data_type list_of_variable_identifiers ;

A.3 Primitive instances

A.3.1 Primitive instantiation and instances

gate_instantiation ::=
cmos_switchtype [delay3] cmos_switch_instance { , cmos_switch_instance } ;
| enable_gatetype [drive_strength] [delay3] enable_gate_instance { , enable_gate_instance } ;
| mos_switchtype [delay3] mos_switch_instance { , mos_switch_instance } ;
| n_input_gatetype [drive_strength] [delay2] n_input_gate_instance { , n_input_gate_instance } ;
| n_output_gatetype [drive_strength] [delay2] n_output_gate_instance
{ , n_output_gate_instance } ;
| pass_en_switchtype [delay2] pass_enable_switch_instance { , pass_enable_switch_instance } ;
| pass_switchtype pass_switch_instance { , pass_switch_instance } ;
| pulldown [pulldown_strength] pull_gate_instance { , pull_gate_instance } ;
| pullup [pullup_strength] pull_gate_instance { , pull_gate_instance } ;

cmos_switch_instance ::= [ name_of_gate_instance ] ( output_terminal ,