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

one for prop_cov4 that records the total number of successes of the property and a
second one for the cover point dl_pt of the covergroup instance delay_cg_inst .
dl_pt has 100 bins, one for each value in the delay range [1:100] .
Note that in this formulation of the property, the property operator followed-by
#-# could have been replaced by the overlapping sequence concatenation ##0
because the consequent of #-# is a sequence. The effect is the same.
When should one use one or the other? We believe that this depends on the
property to be covered. If the consequent is a sequence, use ##0 and ##1 .Ifitis
a property, use #-# , and #=# , respectively. Followed-by is also useful even with
sequences when it is desired to identify clearly the trigger condition (the antecedent
of followed-by) in the cover property statement.
We cannot simply substitute s_eventually in place of the sequence operators.
The reason is that s_eventually provides no way to increment the local variable
when the clock advances. We can still extend the formulation with s_eventually
by adding extra code to keep a global count of clock ticks outside the assertion.
We initialize the local variable to the current count of the global counter when a
matches, and when b matches we pass the difference between the global counter
and the local variable value to the sample function call. This is shown in the next
example.

Example 18.8.

default clocking ck @( posedge clk); endclocking
int unsigned tick_counter = 0;
covergroup delay_cg with function sample ( int unsigned delay);
dl_pt: coverpoint delay {
bins delays [100]: {[1:100]};

}
endgroup
delay_cg delay_cg_inst new ();
always @ck
tick_counter <= tick_counter+1;
property p_delay_coverage;
int unsigned start_tick;
disable iff (reset) @( posedge clk)
(a, start_tick = tick_counter)
#-# s_eventually [1:100] (
b,
delay_cg_inst.sample(tick_counter-start_tick),
$display("prop_cov5 success, time %t, delay %0d",
$time, tick_counter-start_tick)

);
endproperty
prop_cov5: cover property (p_delay_coverage);

t

The compression of many generated cover property statements into one
together with a covergroup can be applied in other situations too. For example,
it is common to write the same cover statement on all bits of a vector. Instead, we
can use a generalized cover property on the vectors, save the bit indices that were
triggered in a local variable, and finally update the database using a covergroup .