система Verilog утверждения: Использование значения рег в оператор repition

Question

Я пытаюсь сделать что-то вроде этого:

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

Здесь c не является «константой», но значение исходя из некоторых битов регистра. например: reg[4:0], который написан только один раз. Проверка заключается в том, чтобы убедиться, что b утверждается только в том случае, если a является высоким для числа циклов «c».

Однако SVA не принимают переменную типа: [*reg[4:0]]. Есть идеи??

Answer 1

Внесите локальную переменную ctr. В каждом posedge будет создано новое утверждение с новым экземпляром ctr. Установите ctr, равное значению в reg1. Убедитесь, что значение a равно true. Уменьшите счетчик, если он больше нуля. Оператор (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