system verilog assertions：在重复运算符中使用reg值

Posted 2023-02-01

我想做这样的事情：

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

这里c不是'常数'，而是来自寄存器的某些位的值。例如：reg[4:0]，只写一次。检查是否仅在a为“c”个循环次数时才确定b是否有效。

但是，SVA不接受这样的变量：[*reg[4:0]]。有任何想法吗？？

答案

引入局部变量ctr。在每个posedge将创建一个新的断言与ctr的新实例。设置ctr等于reg1中的值。检查a在整个向下计数中是否为真。只要计数器大于零，就减少计数器。 (ctr>0, ctr--)[*0:$]声明将倒计时直到ctr == 0为真。

您可能想要将(ctr>0, ctr--)[*0:$]更改为(ctr>0, ctr--)[*1:$]，具体取决于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");

工作示例：http://www.edaplayground.com/x/Xh9

资料来源：

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

另一答案

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