Let, Sequence and Property Declarations; Inference - SVA: The Power of Assertions in SystemVerilog - page 172

In the preceding example, the inference was quite simple, both the clock and
the disabling expression were obtained directly from the default declarations. What
happens if an instance of a property or sequence is used directly inside the body of
another property or sequence definition? How is the clock or disabling expression
inferred in such cases? This will be discussed after we examine the syntax for
defining sequences and properties.

8.2.1 Syntax of Sequence-Endsequence

The syntax of a sequence declaration is as follows, where items in [] brackets are
optional:

sequence identifier ( sequence_port_list )
{local_variable_declarations}
sequence_expression ;
endsequence [ : identifier ]

The sequence_port_list consists of a possibly empty comma-separated list of
individual port declarations. Each such port can have the following components:

[ local [ port_direction ] ] type
identifier {dimension} [ = default_argument ]

where

￿ port direction is only allowed when the keyword local is used indicating that it
is a local variable port (see Chap. 16 ). It can be input , output ,or inout .
￿ type is a type specification. It is obligatory when the port is a local variable port,
otherwise it is optional. In addition to any integral type, the type can also be
an event , sequence , or the keyword untyped . untyped indicates that the port(s)
following the keyword do not have any formal type and is used to explicitly denote
ports as untyped, especially when typed ports precede an untyped port.
￿ identifier { dimension } is a usual port name which can have an optional specifi-
cation of dimensions provided that it is a local variable port or a typed integral
port.
￿ default argument is an optional default actual argument. It has to be type
compatible with the port type in the case the type is specified.

The declaration of a sequence is an extension of the interface of let .Themain
differences are the addition of types event and sequence , and the possibility to
indicate local variable ports with their direction and type. Keyword untyped can be
used to indicate ports that have no specified type. Let us concentrate on ports other
than local variable ports, the latter are described in detail in Chap. 16 . The type of a
port may be specified, but it can also be left without a type like in let declarations.
A port without a type specification or an explicit untyped can be specified only