如何在 Systemverilog 中使用递归属性

Question

待验证模块如下... 该模块有一个输入 in1 和一个输出 out1，在交替的时钟周期上，out1 是 in1 的缓冲和反相值。

我尝试使用递归属性.

对检查器模块进行编码

module check (input in1, out1, clk);

    property p1(bit state);
        bit nxt;
        @(posedge clk) 
        (1 ,nxt=!state) |-> (out1 == (nxt) ? !in1 : in1) and 
                             nexttime p1(nxt);
    endproperty

    initial assert property(p1(0)) else $fatal(3, "Failed!");

endmodule

但是，运行 edaplayground 的代码抛出此错误...

RROR VCP2000 "Syntax error. Unexpected token: nexttime[_NEXTTIME]. The 'nexttime' is a SystemVerilog keyword and cannot be used as an identifier.

我知道这个断言可以不用递归来完成，但是我想用递归来写。

Answer 1

错误提示您错误地使用了 nexttime，这是一个 systemverilog 属性关键字。此运算符检查以下代码中的 "if the clock ticks once more, then a shall be true at the next clock tick"

property p1;
  nexttime a;
endproperty

默认情况下，每个时钟脉冲都会检查并发断言，所以这里不需要递归。大致，你可以这样做：

module check (input in1, out1, clk);
bit o_nxt;

function bit update(input bit nxt);
o_nxt = nxt;
return 1;
endfunction

    property p1(bit state);
        bit nxt;
        @(posedge clk) 
        (1 ,nxt=!state) |-> (out1 == (nxt) ? !in1 : in1) and 
                             update(nxt);
    endproperty

    initial assert property(p1(o_nxt)) else $fatal(3, "Failed!");

endmodule

如何在 Systemverilog 中使用递归属性

How to use recursive properties in Systemverilog

recursion

properties

system-verilog

assertion

system-verilog-assertions