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));

但是，在有效周期变高后，允许我的“完成”信号出现多个周期。您如何做出此声明以确保在断言valid 之后的任何时候都断言“done”，而不会取消断言 valid？

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];

Answer 2

您是否还需要一个 SVA 来确保当 $rose 有效时，还没有断言完成？如果你这样做，那么请考虑这个 SVA- $rose(valid) |-> ~done ##1 $stable(~done) [*949:950] ##[1:$] done;

上述要求在一段时间内未断言，然后在将来的某个时间断言。