SVA: dma req check

SystemVerilog
1

Hi ,

I would like to write assertion check between dma_req and dma_burstend.

spec1; dma_req is high for two clk_sys, where as dma_burst_end is for one clk_sys
spec2: Dut should not generate another dma_req until “dma_burstend received for current dma_req”

for two clk_sys dma_req check , does following works


   property dma_req_check();
      @(posedge of sys_clk)
	$rose(dma_req)|-> (dma_req[*2] ##1 !dma_req) 
      endproperty

Does following code works for spec2?



property
@(posedge clk_sys)
$fell(dma_req)|-> !dma_req[+] ##1  dma_burstend
endproperty
2

In reply to cool_cake20:

can anybody clarify my doubt ?

3

In reply to :

Hi Ben,

    Thanks for suggestion , i have written two kinds of checks as below



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;
	#25;
	dma_req=0;
	#30;
	$finish;
    end
endmodule // test

After the simulation ,i am expecting that both assertion should fail, but ap_dma2cycles2 catching the failure where as ap_dma2cycles1 is not.

in ap_dma2cycles1 : assertion started executing from 2nd clock cycle.

4

In reply to cool_cake20:

Can’t we upload the wave.png from desktop to this blog ?

I tried to attach the picture but it is asking for URL ?

5

In reply to cool_cake20:

@(posedge clk)
$rose(dma_req)|-> (dma_req[*2] ##1 !dma_req);
means that if
@t0 $rose(dma_req)==1 then
@t0 dma_req ==1 // one repetition
@t1 dma_req ==1 // 2nd repetition at next cycle
@t2 dma_req ==0 //

$rose(dma_req)|=> (dma_req[*2] ##1 !dma_req);
means that if
@t0 $rose(dma_req)==1 then
@t1 dma_req ==1 // one repetition
@t2 dma_req ==1 // 2nd repetition at next cycle
@t3 dma_req ==0 //

Thus, you need
$rose(dma_req)|=> (dma_req[*2] ##1 !dma_req);

To upload, you’ll need an area to share.
google drive is a good place. I use my site, since I have access to it.

6

In reply to ben@SystemVerilog.us:

You should be able to attach a .jpg or .pdf to a post

7

In reply to dave_59:

You should be able to attach a .jpg or .pdf to a post

How do you do this?
Both LINK or PICTURE icons (above the square box) require a url
Dave, in your reply, please attach the image that is in this link, and explain to me how you did it.
Maybe I am missing something.

1256×681 90.4 KB

Ben

8

In reply to ben@SystemVerilog.us:

Try this

9

In reply to dave_59:

Please explain to me how you did it.
There is no menu for an attachment, just links.

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.

11

In reply to cool_cake20:

All signals are sampled in the Preponed region (see 1800’2012 4.4 Stratified event scheduler), just before the clocking event. If you do the analysis, you’ll see that it works OK, as expected.
Ben SystemVerilog.us

12

In reply to ben@SystemVerilog.us:

Thanks ben, i will try to analyse , by the way how did you enable “Assertion thread view” in questa .

Dave : Please let us know how did you uploaded the image ?

13

In reply to cool_cake20:

how did you enable “Assertion thread view” in questa .

From the assertion window. Click on the assertion and do a right-mouse click. It’s on the menu.
I compile with vlog -vopt -assertdebug -sv
I sim with vsim -vopt -assertdebug