用于握手的 SVA答案

【问题标题】：SVA for handshake用于握手的 SVA
【发布时间】：2013-07-08 13:48:38
【问题描述】：

我正在尝试为握手过程编写 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被取消断言？

【问题讨论】：

【解决方案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];

【讨论】：

这里有趣的一点是您（正确地）使用$rose() 作为启用条件。你这样做的原因，而不仅仅是req |-> ...，是因为你不会在req 为高的每个周期产生一个断言线程，而只是第一个。这是一个巨大的性能胜利。

【解决方案2】：

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

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

【讨论】：