For the following example ::
module top ;
bit req , gnt , clk ;
property pr1 ;
@( posedge clk ) req |-> ##2 gnt ;
endproperty
ap_property : assert property ( pr1 ) $display ("TIME : %2t Assertion PASS " , $time );
else $display ("TIME : %2t Assertion FAIL " , $time );
initial forever #5 clk = ! clk ;
initial begin
#4 ; req = 0 ;
#10 ; req = 1 ;
#10 ; req = 0 ;
#10 ; gnt = 1 ;
#2 ; $finish() ;
end
endmodule
My expectation is that I should observe Vacuous Pass reports whenever ’ req ’ is False i.e at TIME : 5 , 25 , 35 .
However in the O/P I observe only the Non-Vacuous Pass report at TIME : 35 .
Am I missing something here ?