Regarding Vacuous Pass Reports

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 ?

In reply to hisingh:

By default, vacuous success does not count as an assertion “pass”.

Use $assertpasson(), $assertcontrol(6,31,7), or a tool command line option that turns vacuous success into an assertion pass.

In reply to dave_59:

Thanks Dave ,

Seems like the book I am referring has a couple of errors .

Via the book I was made to believe that to ignore the vacuous pass reports via assert property we should be using cover property instead of assert property .