system-verilog-assertions - 系统 Verilog 断言，SVA

Question

我正在为握手协议编写断言，其中可以有背靠背的请求和确认。Acks 可以在 req 之后的 1 到 5 个周期之间出现。我如何使用断言来确保每个 req 有 1 个 ack，同时还要考虑 req 或 ack 上的故障？

属性 p1: @(posedge clk) req ##[1:5] ack ; 最终属性

属性 p2: @(posedge clk) $rose(ack) |-> $past(req,5);

我不确定这是否保持 req 与 ack 的一对一映射。

Answer 1

确认之前可以有两个请求吗？如果不是，我会写：

property p_test;
@(posedge clk)
$rose(req) |=> !req[*0:$] ##0 ack;
endproperty

如果 req 仅是脉冲则有效

Answer 2

我认为您的意思是在任何确认之前可能有多个请求？如果是这样，解决方案需要属性变量或辅助逻辑。形式属性没有内存或计数器（不使用变量）。

如果你想使用辅助逻辑，这里有一些代码：

假设您最多允许 15 个未完成且最多需要 25 个时钟来获得所有确认：

logic [3:0] req_cnt, ack_cnt;
always @ (posedge clk) if (rst) req_cnt <= 0; else req_cnt <= req_cnt + req;
always @ (posedge clk) if (rst) ack_cnt <= 0; else ack_cnt <= ack_cnt + ack;

assert property (@ (posedge clk) disable iff (rst) sync_accept_on(req) ##25 req_cnt == ack_cnt);

计算请求和确认。然后断言在 25 个无 req 周期后，req_cnt == ack_cnt。

如果没有超过 1 个未完成的请求，则逻辑要简单得多。请澄清是否是这种情况。

Answer 3

下面的属性 2 与属性 1 不同步。

属性 p2: @(posedge clk) $rose(ack) |-> $past(req,5);

您是说 ack 必须提前 5 个时钟发出请求。但是属性 1 表示 req 后跟 ack 是有效的。

我认为您需要一个带有请求的 id，当 ack 发生时您可以匹配该请求。

    sequence s_ack_check;
        byte id;
        (req && id == ack_id) ##[1:5](ack && ack_id == id);
    endsequence