避免使用 SVA 序列的支持代码来处理流水线事务

Question

假设我们有一个协议，内容如下。一旦主机将 req 设置为 fill，从机将通过 rsp:

发出 4 次传输信号

整个事务的 SVA 序列是（假设从站可以在 trans 个周期之间插入 idle 个周期）：

req == fill ##1 (trans [->1]) [*4];

现在，假设允许主服务器处理请求。这意味着下一个 fill 被允许在 4 trans 周期完成之前开始：

上面的 SVA 序列没有帮助，因为对于第二个 fill 它将错误地匹配 4 个 trans 周期，留下最后一个 trans "floating" .只有在匹配了前一个 fill 的周期后，它才需要开始匹配 trans 个周期。

序列需要单次评估中无法获得的全局信息。基本上它需要知道它的另一个实例是运行。我能想到的唯一实现方法是使用一些 RTL 支持代码：

int num_trans_seen;
bit trans_ongoing;
bit trans_done;
bit trans_queued;

always @(posedge clk or negedge rst_n)
  if (!rst_n) begin
    num_trans_seen;
    trans_ongoing <= 0;
    trans_done <= 0;
    trans_queued <= 0;
  end
  else begin
    if (trans_ongoing)
      if (num_trans_seen == 3 && req == trans) begin
        trans_done <= 1;
        if (req == fill || trans_queued)
          trans_queued <= 0;
        else
          trans_ongoing <= 0;
        num_trans_seen == 0;
      end
    else
      if (trans_queued) begin
        trans_queued <= 0;
        trans_ongoing <= 1;
      end

    if (trans_done)
      trans_done <= 0;
  end

上面的代码应该在事务进行时提高 trans_ongoing 位，并在发送 fill 的最后一个 trans 时在时钟周期中脉冲 trans_done . （我说应该是因为我没有测试它，但这不是重点。让我们假设它有效。）

有了这样的东西，可以将序列重写为：

req == fill ##0 (trans_ongoing ##0 trans_done [->1]) [*0:1]
  ##1 (trans [->1]) [*4];

这应该可行，但我对需要支持代码这一事实并不感到特别兴奋。其中有很多冗余，因为我基本上重新描述了大部分事务是什么以及流水线是如何工作的。它也不容易重复使用。一个 sequence 可以放在一个包中并导入到其他地方。支持代码只能放在某个模块中并重复使用，但它与存储序列的包是不同的逻辑实体。

这里的问题是：有没有什么方法可以编写序列的流水线版本，同时避免需要支持代码？

Answer 1

一种可能的解决方案可以通过以下 2 个断言实现。

第一张图片 -

(req == fill) && (rsp == idle) |=> ((rsp == trans)[->1])[*4]

对于第二张图片 -

(req == fill) && (rsp == trans) |=> ((rsp == trans)[->1])[*0:4] ##1 (rsp == idle) ##1 ((rsp == trans)[->1])[*4]

一个问题是，如果每个周期有连续的"fill"个请求（连续4个"fill"个请求，没有任何中间"idle"），那么第二个断言将不会计算"trans" 每个 "fill" 请求的周期（相反，它只会在第二组 "trans" 周期本身完成）。

到目前为止，我无法修改给定错误的断言。

Answer 2

看起来 rsp 在传输开始之前总是空闲的。如果 rsp 的 idle 是一个常数值，并且它是一个 trans 永远不会是的值，那么您可以使用：

req == fill ##0 (rsp==idle)[->1] ##1 trans[*4];

当流水线支持 1 到 3 个阶段时，以上应该有效。

对于 4+ 深的管道，我认为你需要一些辅助代码。断言的 success/fail 块可用于计算已完成的 trans;这使您免于编写额外的 RTL。属性中的局部变量可用于对填充的计数值进行采样。采样值将用作开始采样预期反式模式的标准。

int fill_req;
int trans_rsp;
always @(posedge clk, negedge rst_n) begin
  if(!rst_n) begin
    fill_req <= '0;
    trans_rsp <= '0;
  end
  else begin
    if(req == fill) begin
      fill_req <= fill_req + 1; // Non-blocking to prevent risk of race condition
    end
  end
end

property fill_trans();
  int id;
  @(posedge clk) disable iff(!rst_n)
  (req == fill, id = fill_req) |-> (rsp==idle && id==trans_rsp)[->1] ##1 trans[*4];
endproperty

assert property (fill_trans()) begin
  // SUCCESS
  trans_rsp <= trans_rsp + 1; // Non-blocking to prevent risk of race condition
end
else begin
  // FAIL
  // trans_rsp <= trans_rsp + 1; // Optional for supporting pass after fail
  $error("...");
end

仅供参考：我还没有时间对此进行全面测试。它至少应该让你朝着正确的方向前进。

我进行了更多试验，发现了一个可能更符合您喜好的解决方案；没有支持代码。

根据 IEEE Std 1800-2012 § 16.9.2 序列重复 ，trans[->4] 相当于 (!trans[*] ##1 trans)[*4]。因此，我们可以使用局部变量来检测扩展表单的新填充请求。例如下面的序列

sequence fill_trans;
  int cnt;                                // local variable
  @(posedge clk)
  (req==FILL,cnt=4) ##1 (                 // initial request set to 4
    (rsp!=TRANS,cnt+=4*(req==FILL))[*]    // add 4 if new request
    ##1 (rsp==TRANS,cnt+=4*(req==FILL)-1) // add 4 if new request, always minus 1
  )[*] ##1 (cnt==0);                      // sequence ends when cnt is zero
endsequence

除非有另一个未提及的限定符，否则您不能使用典型的 assert property();，因为它会在每次有填充请求时启动新的断言线程。而是使用 expect 语句，它允许等待属性评估（IEEE Std 1800-2012 § 16.17 Expect 语句）。

always @(posedge clk) begin
  if(req==FILL) begin
    expect(fill_trans);
  end
end

我尝试重新创建您的描述行为以进行测试 https://www.edaplayground.com/x/5QLs

避免使用 SVA 序列的支持代码来处理流水线事务

Avoiding support code for SVA sequence to handle pipelined transaction

system-verilog

system-verilog-assertions