1

待验证的模块如下... 该模块有一个输入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 “语法错误。意外标记：nexttime[_NEXTTIME]。‘nexttime’是 SystemVerilog 关键字，不能用作标识符。

我知道这个断言可以在没有递归的情况下完成，但我想使用递归来编写它。

4

1 回答 1

2

该错误表明您nexttime以错误的方式使用了 systemverilog 属性关键字。该运算符在以下代码中检查“如果时钟再次滴答，则a在下一个时钟滴答时应为真”

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
于 2015-11-08T04:39:00.613 回答