system verilog assertions: Using a reg value in a repition operator

Question

I am trying to do something like this:

assert property (@(posedge clk) disable iff (!rst) a[*c] -> $rose(b))

Here c is not a 'constant' but a value coming from some bits of a register. eg: reg[4:0] which is written only once. The check is to see if b is asserted only when a is high for "c" number of cycles.

However, SVAs do not accept a variable like this : [*reg[4:0]]. Any ideas??

Answer 1

Introduce a local variable ctr. At every posedge a new assertion with a new instance of ctr will be created. Set ctr equal to the value in reg1. Check that a is true throughout the down count. Decrement the counter as long as it is larger than zero. The (ctr>0, ctr--)[*0:$] statement will count down until ctr == 0 is true.

You might want to change (ctr>0, ctr--)[*0:$] to (ctr>0, ctr--)[*1:$], depending on what results you expect if reg == 0.

property pr_aRegTimes;
  integer ctr;
  disable iff (!rst)
  @(posedge clk)
    (1, ctr = reg1) ##0 a throughout ((ctr>0, ctr--)[*0:$] ##1 (ctr == 0)) |-> $rose(b);
endproperty

as_aRegTimes: assert property (pr_aRegTimes)
  else $error("aRegTimes failed");

Working example: http://www.edaplayground.com/x/Xh9

Sources:

https://www.doulos.com/knowhow/sysverilog/tutorial/assertions/ http://www.win.tue.nl/~jschmalt/teaching/2IMF20/SvaFvTutorialHVC2013.pdf

Answer 2

property pr_aRegTimes;
  integer ctr;
  disable iff (!rst)
  @(posedge clk)
    ($rose(a), ctr = reg1) ##0 (a&&ctr>0,ctr--)[*] |-> $rose(b);
endproperty