$past 带有输入信号

Question

我想验证如果一个事件发生，那么在过去的“num_ticks”，应该已经断言了一些信号。

举个例子，我写的属性是：

property test_past;
  @(posedge clk)
    $rose(gnt) |-> $past(req, num_ticks);
endproperty

这里的问题是 num_ticks。如果 num_ticks 是写入属性的模块的输入信号，则断言失败。如果我将 num_ticks 声明为一个 int，并将其分配给一个常量，它就通过了。

$past 只适用于常数值吗？ LRM中没有提到这个。

我正在使用 Questasim 10.3

Answer 1

您可以为此目的使用多个断言。

假设num_ticks是4位宽，那么你可以这样做

genvar x;
generate
  for (x=0; x<16; x++)
  begin
    property test_past;
      @(posedge clk)
      (num_ticks == x) && $rose(gnt) |-> $past(req, x);
    endproperty
  end
endgenerate

$past 带有输入信号

$past with an input signal

system-verilog

uvm

questasim

system-verilog-assertions