In the Assertion section of Systemverilog LRM 1800-2017
The below section
16.4.2 Deferred assertion flush points
has the below example.
I have highlighted the line with ambiguity with {{{" "}}}
It basically says a = 0; is in the same time step as the previous statement b = 1; even though there is a clock cycle defference between the two (##1;), Just want to know if this is by error or my understanding of time step is incorrect.
module dut(input logic clk, input logic a, input logic b);
logic c;
always_ff @(posedge clk)
c <= b;
a1: assert #0 (!(a & c)) $display("Pass"); else $display("Fail");
a2: assert final (!(a & c)) $display("Pass"); else $display("Fail");
endmodule
program tb(input logic clk, output logic a, output logic b);
default clocking m @(posedge clk);
default input #0;
default output #0;
output a;
output b;
endclocking
initial begin
a = 1;
b = 0;
##10;
b = 1;
##1;
a = 0;
end
endprogram
module sva_svtb;
bit clk;
logic a, b;
...
dut dut (.*);
tb tb (.*);
endmodule
In the 11th clock cycle, observed deferred assertion a1 will first execute in the Active region, and it will fail
since at this point a and c are both 1. This pending assertion report will mature in the Observed region, and
the failure report will be scheduled in the Reactive region. {{{“However, in the Reactive region of the same time
step, the testbench will set a to 0”}}}, triggering another execution of the implied always_comb block
containing assertion a1. This time a1 will pass. So both a pass and a fail message will be displayed for a1
during this time step.