system-verilog - 用于握手的 SVA

Question

我正在尝试为握手过程编写 SVA 断言。

在我的搜索中，我发现了以下内容:

property p_handshake(clk,req,ack);
@(posedge clk)
req |=> !req [*1:max] ##0 ack;
endproperty
assert property(p_handshake(clock,valid,done));

但是，在有效周期变高后，我的“完成”信号可以出现多个周期。您如何使此语句确保在断言有效后的任何时候都断言“完成”，而不会取消断言有效？

Answer 1

$rose(req) |=> req[*1:$] ##0 ack;

$rose将在 req 的上升沿开始断言. [*1:$]意味着对于 1 到无限时钟的范围，左侧必须为真。您可以使用 [+]相当于 [*1:$] .

编写检查器的其他一些风格是:

$rose(req) |-> req[*1:$] ##1 (ack && req);
$rose(req) |-> ##1 req throughout ack[->1];