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

This is illustrated in the next example, where first we show the coverage collection
using a generate loop and then rewrite it using a covergroup .
Example 18.9. On 32-bit vectors, cover that a rising transition on x[i] is eventually
followed by y[i] asserted.
Solution: Using generate :
bit [31:0] x, y; bit clk;
default clocking ck @( posedge clk); endclocking
for ( genvar i=0; i<32; i++) begin : loopi
prop_cov6: cover property (
!x[i] ##1 x[i] ##1 y[i][->1]

);
end : loopi

Solution: Using a covergroup :
default clocking ck @( posedge clk); endclocking
covergroup cg_vect
with function sample ( bit [31:0] covered);
vct: coverpoint covered {
bins x0 = {covered[0]};
... // enumerate all bit positions
bins x31 = {covered[31]};

}
endgroup
cg_vect cg_inst = new ();
property p_vector_cov;
bit [31:0] rose_x, covered;
(1, rose_x = x)
##1 (1, rose_x = x & ~rose_x)
##0 (|rose_x, covered = 0)
##1 (
(y & rose_x & ~covered)[->1],
covered |= (y & rose_x)

)[+]
##0 (covered == rose_x, cg_inst.sample(covered));
endproperty
prop_cov7: cover property (p_vector_cov);

t

Property p_vector_cov is much more complex than the one used in prop_cov6 .
There are two local variables: rose_x to record the bits of x that had a ris-
ing transition at the start of the property; and covered , which maintains the
set of bits of y & rose_x that have been covered so far. The final condition,
covered == rose_x , indicates that all the rising transitions recorded in rose_x
have been covered by high values on the corresponding bits of y . When that occurs,
the covered bits are sent to the covergroup instance and recorded.
There are two issues with this encoding that need some remedy. First, if for one
of the bits of x that had a rising transition the counterpart bit of y is never asserted,
then no coverage is recorded. It is better always to sample when some match occurs
inside the repetition loop. The second issue is in the declaration of the covergroup .