Coverage - SVA: The Power of Assertions in SystemVerilog - page 406

Efficiency Tip. Unless necessary, avoid using cover sequence on sequence
expressions that may result in multiple matches, such as those containing delay and
repetition ranges or sequence disjunction ( or ).
If the total number of matches is not of interest, the cover statement can be stated
using cover property as discussed next (Sect. 18.2.2 ).

18.2.2 Property Coverage

The syntax of this statement is cover property ( property_spec ) state-
ment_or_null We have seen a description of assert property in Sect. 4.4 .
Similarly, the body of cover property may consist of a disable iff
specification, a clocking event, and a property expression. If the property expression
is a sequence, it is promoted to a property, meaning that the first occurring match
of the sequence is transformed into a success of the property for that particular
evaluation attempt, and any further evaluation within that attempt is curtailed.
The coverage from Example 18.1 is rewritten using cover property in the
following example.

Example 18.2.

default clocking ck @( posedge clk); endclocking
int my_count = 0;
prop_cov1: cover property ( disable iff (reset)
a ##[1:100] b
) begin
my_count++;
$display("success of prop_cov1 at time %t", $time);

t

end

In this case, my_count will be incremented and the $display statement will be
executed for only the first match of the sequence in any evaluation attempt. The
total number of recorded successes will thus be less than or equal to the number
of evaluation attempts of the cover property . Contrast this with the behavior of
cover sequence , for which the total number of recorded matches can exceed the
number of evaluation attempts.
Property successes are classified as vacuous and nonvacuous (see Sect. 10.6 for
discussion of vacuous and nonvacuous successes). Vacuous and nonvacuous suc-
cesses are recorded separately in the coverage database. Therefore, the information
obtained from the coverage database consists of the number of evaluation attempts
started, the number of attempts in which the property succeeded nonvacuously,
and the number of attempts in which the property succeeded vacuously. Attempts
that were disabled are not counted as either vacuous or nonvacuous successes.
A simulation tool may optionally provide a separate count for disabled attempts.