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 don’t consider the questions as a tool-specific one. However, I prefer to state the commands I use in Questasim and the output I obtain.
vlog +cover MCVE.sv
``` verilog
vsim -c -coverage tb -do "run -all;coverage report -detail -assert"
``` verilog
# 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
# Count Count
# --------------------------------------------------------------------
# /tb/assert__check_dout
# MCVE.sv(32) 0 0
If I invert the consequence of the property, i.e., 1!=1, things happen as expected.
# 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
# Count Count
# --------------------------------------------------------------------
# /tb/assert__check_dout
# MCVE.sv(32) 1 0