我正在尝试做这样的事情:
assert property (@(posedge clk) disable iff (!rst) a[*c] -> $rose(b))
这里c
不是一个“常数”,而是一个来自寄存器某些位的值。eg:reg[4:0]
只写一次。检查是否b
仅在 a 为高“c”个周期时才被断言。
但是,SVA 不接受这样的变量 : [*reg[4:0]]
。有任何想法吗??
我正在尝试做这样的事情:
assert property (@(posedge clk) disable iff (!rst) a[*c] -> $rose(b))
这里c
不是一个“常数”,而是一个来自寄存器某些位的值。eg:reg[4:0]
只写一次。检查是否b
仅在 a 为高“c”个周期时才被断言。
但是,SVA 不接受这样的变量 : [*reg[4:0]]
。有任何想法吗??
引入一个局部变量ctr
。ctr
在每个 posedge都会创建一个带有新实例的新断言。设置ctr
等于 中的值reg1
。检查a
整个向下计数是否正确。只要计数器大于零,就递减计数器。该(ctr>0, ctr--)[*0:$]
语句将倒计时,直到ctr == 0
为真。
您可能希望更改(ctr>0, ctr--)[*0:$]
为(ctr>0, ctr--)[*1:$]
,具体取决于您期望的结果 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");
工作示例: 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