0

我有一个长度为 x 的数组。给定测试平台的信号输出将是数组中的每个值，其顺序从 0:x-1 开始。

特别是在我的问题中，数组是滤波器系数，而测试台是脉冲响应。测试需要进行自检，这将需要具有动态长度的序列，因为系数会因测试而异。

我想要的序列应该是这样的：

always @(posedge clk) begin
  assert_sequence : assert property (    
        (data_out == array_1[0])
    |=> (data_out == array_1[1])
    |=> (data_out == array_1[2]) 
    |=> (data_out == array_1[3]) 
    |=> (data_out == array_1[4]) 
    |=> (data_out == 0) ) 
      $info("Seen the sequence");
    else
      $error("Sequence was incorrect");  
  end

这可以动态进行吗？我尝试了一个 genvar for 循环，但它会引发错误。我搜索了论坛，找不到任何符合我要求的东西。

可能这样的事情可以给出正确的答案？

    always @(posedge clk) begin
  assert_sequence : assert property (    
        (data_out == array1[0][0])

  for(genvar i = 1; i < 5, i++) begin
    |=> (data_out == array1[i])
  end

    |=> (data_out == 0) ) 
      $info("Seen the sequence");
    else
      $error("Sequence was incorrect");  
  end
4

2 回答 2

1

如前所述，SVA 可能不是这里的自然选择。但是，确实是一个有趣的问题，所以有点思考：

您是否尝试过使用递归属性？类似于以下内容：

property check_sequence(coefficients);
  (data_out == coefficients[0]) ##0
    ((coefficients.size() == 1) or 
     (##1 check_sequence(coefficients[1:coefficient.size()]));
endproperty

assert_label: check_sequence(array_1);

仍然需要一个触发器 - 未在原始 q 中指定。

它是否是最有效或可读的解决方案是另一回事。

于 2020-05-22T01:09:50.460 回答
0

评论非常有用，并记录了我为解决此问题所采取的方向。只是重新审视了这个问题并想出了这个不优雅的解决方案。

for(genvar i = 1; i < 5; i++) begin
  always @(posedge clk) begin
    assert_sequence : assert property (
                                       (data_out == array1[0])
                               |-> ##i (data_out == array1[i])
                               |-> ##(5-i) (data_out == 0) //This line prevents error 
                                                                  //as my coefficients are symmetric
                                    )
      $info("Impulse response Coefficient %0d seen", i);
  else
      $error("Impulse response Coefficient %0d not seen", i);
  end
end

这段代码创建了多个断言，并描述了当我看到第一个系数时，我希望在 i 个时钟周期内看到 (i+1) 系数，并且由于我的对称性问题，我将在 (5-i) 个时钟周期内看到一个 0。

于 2020-05-21T09:16:49.887 回答