Doubts on cover property & cover sequence

SystemVerilog
, , ,
1

Hi All,

I am new to SystemVerilog Assertions and have a few doubts related to cover property

As per my understanding unlike assert property, it’s illegal to write fail action block for cover property. Are there any further differences between them ?

[Q1] Does cover property / cover sequence support all operators that assert property supports ?

Eg: Both types of Implication operators , clock delay , multi-clocked property expressions , always , s_until_with etc

While going through LRM Section 16.14.3 Cover statement I realized SV has cover sequence as well which gave me my next question

[Q2] What are the differences b/w cover property & cover sequence? When should one prefer to use one over the other?

LRM mentions

The difference between the two categories is that for sequence coverage, all matches per evaluation attempt are reported, whereas for property coverage the coverage count is incremented at most once per evaluation attempt.

cover property ( property_spec ) statement_or_null

The results of this coverage statement for a property shall contain the following:
— Number of times attempted
— Number of times succeeded (maximum of one per attempt)
— Number of times succeeded because of vacuity

cover sequence (
[ clocking_event ] [ disable iff ( expression_or_dist ) ] sequence_expr )
statement_or_null

Results of coverage for a sequence shall include the following:
— Number of times attempted
— Number of times matched (each attempt can generate multiple matches)

For the following Testbench

always #5 clk = !clk;

c1:cover property( @(posedge clk) a ##[1:3] b |-> c );

c2:cover sequence( @(posedge clk) a ##[1:3] b |-> c );

initial begin:B1
  #4   a = 1;
  #10; b = 1;
       a = 0;
       c = 1;
  #10; b = 1;
  #10; b = 1;
  #02; $finish();
end

[Q2] For 1st attempt at T:5, would c1 report that it has succeeded ( i.e non-vacuous pass ) only once whereas c2 report that it succeeds ( i.e non-vacuous pass ) thrice ?

[Q3] What does the following mean :: “Number of times succeeded because of vacuity“

Does it mean that cover property reports vacuous pass whereas cover sequence doesn’t ?

initial begin:B2
  #4   a = 0;
  #10; a = 0;
  #10; a = 0;
  #02; $finish();
end

[Q4] For above stimulus would c1 report :: 3 attempts , 0 times succeeded & 3 vacuous pass