Consider the below code. The assert property is hit and passed according to the output but its pass count is zero in the coverage result. Why?
module tb;
reg Krdy;
reg Drdy;
reg EN;
reg CLK;
reg RSTn;
property check_dout;
@(posedge CLK) disable iff (~RSTn)
(
(
(
(EN & Krdy)
##1
(
((EN & Krdy) == 0)
throughout
(
((EN & Krdy) == 0)
##[0:$]
(EN & Drdy & ~Krdy)
)
)
)
##1
(EN [-> 1])
), $display("antecedent happened at time=%t", $time)
)
|=> (1==1, $display("consequent happended at time=%t", $time));
endproperty
assert property (check_dout)
else $error("Error at time=%t", $time);
always #5 CLK = ~CLK;
initial begin
CLK = 0;
RSTn = 1;
EN = 1;
@(posedge CLK);
Krdy = 1;
Drdy = 0;
@(posedge CLK);
Krdy = 0;
Drdy = 1;
@(posedge CLK);
Drdy = 0;
repeat (3) @(posedge CLK);
$stop;
end
endmodule
I use the following commands in Questasim:
vlog +cover MCVE.sv
vsim -c -assertcover tb -do "run -all;coverage report -detail -assert"
And get the following output:
# run -all
# antecedent happened at time= 35
# consequent happended at time= 45
# ** Note: $stop : MCVE.sv(50)
# Time: 55 ns Iteration: 1 Instance: /tb
# Break in Module tb at MCVE.sv line 50
# Stopped at MCVE.sv line 50
# coverage report -detail -assert
#
# ASSERTION RESULTS:
# --------------------------------------------------------------------------------------------------------------------------------
# Name File(Line) Failure Pass Vacuous Disable Attempt Active Peak Active ATV
# Count Count Count Count Count Count Count
# --------------------------------------------------------------------------------------------------------------------------------
# /tb/assert__check_dout
# MCVE.sv(32) 0 0 4 0 5 1 - off
After inverting the consequence of the property, i.e., 1!=1 and running the above commands, I get:
# run -all
# antecedent happened at time= 35
# ** Error: Error at time= 45
# Time: 45 ns Started: 15 ns Scope: tb File: MCVE.sv Line: 33
# ** Note: $stop : MCVE.sv(50)
# Time: 55 ns Iteration: 1 Instance: /tb
# Break in Module tb at MCVE.sv line 50
# Stopped at MCVE.sv line 50
# coverage report -detail -assert
#
# ASSERTION RESULTS:
# --------------------------------------------------------------------------------------------------------------------------------
# Name File(Line) Failure Pass Vacuous Disable Attempt Active Peak Active ATV
# Count Count Count Count Count Count Count
# --------------------------------------------------------------------------------------------------------------------------------
# /tb/assert__check_dout
# MCVE.sv(32) 1 0 4 0 5 0 - off
The pass count is not incremented because not all the threads of an attempt have succeeded. The use of ##[0:$] causes multiple threads to be created many of which never succeed till the end of the simulation. Thus, the attempt is considered to be active (not passed) till the end of the simulation although one of its threads have passed. That is why there is an active count in the results. More information can be found here:
https://verificationacademy.com/forums/systemverilog/assertion-attempt-getting-incomplete