SystemVerilog 并发断言序列动态长度

Question

我有一个长度为 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

Answer 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 中指定。

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

Answer 2

注释非常有用，并记录了我解决此问题的方向。只是重新审视了这个问题，并提出了这个不优雅的解决方案。

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。