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

While much can be expressed using sequences only, property operators can
provide additional expressive power. The combination of (simple) sequences and
property operators helps to state clearly the intent of the coverage statement.

Example 18.3. Cover with a property expression:

prop_cov2: cover property ( disable iff (reset)
@( posedge clk) a |-> s_eventually [1:100] b
) begin
my_count++;
$display("success of prop_cov2 at time %t", $time);

t

end

The disadvantage of this form is that when a is false, there is a vacuous success
of the property. Coverage of vacuous successes is not useful. The property can be
reformulated using the followed-by operator, which is better suited for this purpose.

Example 18.4.

prop_cov3: cover property ( disable iff (reset)
@( posedge clk) a #-# s_eventually [1:100] b
) begin
my_count++;
$display("success of prop_cov3 at time %t", $time);

t

end

This example illustrates two ideas: (1) the use of the operator followed-by #-#
for concatenating sequences with properties (the Boolean a on the left-hand side of
#-# is a simple sequence), and (2) the use of strong bounded eventuality requiring
the simple sequence b (implicitly cast to property) to occur within 100 clock ticks
after a and due to its strength not to record a hit if there are not enough clock ticks
to complete an evaluation attempt at the end of simulation.

Efficiency Tip. Use cover property unless all matches are absolutely needed.

Avoid using implications in cover property statements. Instead, either use
sequences or replace the implication with a followed-by operator.

The followed-by operator is necessary when the consequent is expected to be a
property or when you wish to indicate clearly the trigger sequence in the antecedent.
Followed-by is particularly useful in checker libraries where the checker arguments
may not be restricted to sequences only.
It is often of interest to obtain information on the conditions under which a
particular coverage scenario occurred. For instance, in the above example it may