Any singular
type is allowed, signed or unsigned, packed or unpacked, with the exception of
event and the non-integer types time, shortreal, real, and realtime.
The following
types are not allowed:
·
non-integer_types ( time, shortreal, real
and realtime)
·
string
·
event
·
chandle
·
class
·
associative
arrays
·
dynamic
arrays
Editor’s Note:
If I understand correctly from reading the BNF and sections 3.3.2 and 3.15,
“singular” does not include unpacked values. Also, why isn’t time considered an
integer (or singular) type?
(a ##2 b)[*1:5]
(a ##2 b)
or (a ##2 b ##1 a ##2 b)
or (a ##2 b ##1 a ##2 b
##1 a ##2 b)
or (a ##2 b ##1 a ##2 b
##1 a ##2 b ##1 a ##2 b)
or (a ##2 b ##1 a ##2 b
##1 a ##2 b ##1 a ##2 b ##1 a ##2 b)
Editor’s Note: The preceding example
description says “the following two examples...”, but it seems to be 1 example
that expands to more than two possible matching sequences. Saying “two
examples” does not seem to match the example.
(a[*0:3] ##1 b ##1 c)
(b ##1 c)
or (a ##1 b ##1 c)
or (a ##1 a ##1 b ##1 c)
or (a ##1 a ##1 a ##1 b
##1c)
Editor’s Note: The preceding example
description says “the following two examples...”, but it seems to be 1 example
that expands to more than two possible matching sequences. Saying “two
examples” does not seem to match the example.
Editor’s Note: I assumed that “should”
was an indication of a mandatory requirement, though it could have meant an
optional requirement.
For sequence
coverage, the statement appears as:
cover property ( [ clocking_event ] sequence_instance sequence_spec ) statement_or_null
or
cover property ( [ clocking_event
] sequence_expr ) statement_or_null
For property coverage, the statement
appears as: All other forms of the cover
statement are evaluated for property coverage.
cover property ( property_instance
) statement_or_null
or
cover property ( [ clocking_event
] property_modifier property_expr)
statement_or_null
or
cover property ( [ clocking_event
] property_implication) statement_or_null
Editor’s Note: The 5 preceding syntax
lines do not follow the BNF format from Annex A. Should
they be rewritten using the actual BNF? Are these 5 syntax lines even needed,
since the BNF is already included in this subsection.
The identifier of a particular attempt is
called attemptId, and the clock tick of the
occurrence of the match is called clock step.
The results of
coverage statement for a property shall contain:
— Number of
times attempted
— Number of
times succeeded
— Number of
times failed
— Number of
times succeeded because of vacuity
— Each attempt
with an identifier (attemptID) and time
— Each
success/failure with an identifier (attemptID) and time
In addition, statement_or_null is executed every time a
property succeeds.
Vacuity rules
are applied only when implication operator is used. A property succeeds
non-vacuously only if the consequent of the implication contributes to the
success.
Results of
coverage for a sequence shall include:
— Number of
times attempted
— Number of
times matched (each attempt can generate multiple matches)
— Each attempt
with attemptId and time
— Each match
with clock step, attemptID, and time
In addition, statement_or_null gets executed for every
match. If there are multiple matches at the same time, the statement gets
executed multiple times, one for each match.
attemptID is the identification
of a particular attempt. Clock step is the clock tick of the occurrence of the
match.
Editor’s Note: What is “attemptID”? It does not appear in the BNF or the 5 syntax
lines above.
A concurrent
assertion statement can be used directly outside of a procedural context. It can be
used within a module as a module_common_item, an interface as a module_common_item, or a program as
a non_port_item. In a module, it is used
as a module_item and in an interface as
an interface_item. A concurrent assertion statement is
either an assert or a cover statement.
Such a concurrent assertion statement uses the always semantics.
The
following two forms are equivalent:
assert property ( property_spec property_spec) action_block action_block
always assert property (property_spec property_spec) action_block action_block;
Similarly, the
following two forms are equivalent:
cover property (property_spec property_spec) statement_or_null statement_or_null
always cover property (property_spec property_spec) statement_or_null statement_or_null
Editor’s Note: The 4 preceding syntax
lines do not follow the BNF format from Annex A. Should
they be rewritten using the actual BNF?