SVA: dma req check

SystemVerilog
10

In reply to ben@SystemVerilog.us:

Hi Ben Thanks for your help,

With this new code assertion is getting failed(as expected).
$rose(dma_req)|=> (dma_req[*2] ##1 !dma_req);

But i am not able to understand it’s execution , in either case the ANTCDENT started 15ns, but as per my understanding $rose(dma_req) happened at 5ns so i am expecting that ANTCDENT should start from 5ns itself(please look at wave).



module test;
  bit clk,dma_req,dma_burstend;
   always #5 clk=~clk;
   property dma_req_check;
      @(posedge clk)
	$rose(dma_req)|=> (dma_req[*2] ##1 !dma_req);
   endproperty
 
   ap_dma2cycles1: assert property (dma_req_check);
 
   property dma_req_check2;
      real t,t_now;
      real t2=20;
      @(posedge dma_req) (1,t=$realtime) |-> @(negedge dma_req)(1,t_now=$realtime) ##0 ((t_now-t)==20);
   endproperty
 
  ap_dma2cycles2:assert property(dma_req_check2);
 
   initial
     begin
	#5;
        dma_req=1;
	#20;
	dma_req=0;
	#30;
	$finish;
    end
endmodule // test

With above code (dma_req is high for 2 clk followed by low),those two assertions has to pass , but ap_dma2cycles1 reporting failure which is wrong.

Here i am suspecting that $rose(dma_req) is not captured at 5ns that is why it is behaving like that, because of this ANTCDENT started at next posedge of clk which at 15ns.