system-verilog - 如何在断言中使用 SystemVerilog 序列属性？

Question

我想说“如果有无限数量的输入，最终我会得到一个输出”，我该怎么做？

在脚本的其他部分，我想假设输入的供应有限，所以我不能只写“假设有无限数量的输入”并在全球范围内保持不变。

到目前为止，我已经编写了属性：

property always_another_valid_input;
   @(posedge clock) ##[1:$] valid_input;
endproperty

property foo;
    @(posedge clock) always_another_valid_input |-> ##[0:$] bar == 1;
endproperty

assert property (foo);

但是当我运行它时，我得到一个错误：property instance always_another_valid_input is not allowed in sequence expression。

|->如果我用非序列属性替换 的任一侧，那么我仍然会收到错误消息。它仅在双方都是非序列属性时才有效。

有没有解决这个问题的好方法？

Answer 1

请参阅IEEE Std 1800-2012 § 16.12 Declaring properties，更具体地说 § 16.12.6 Implication，您将看到|->语法用法描述为：

property_expr ::=
    ...
    sequence_expr |->property_expr
    sequence_expr |=>property_expr

左侧必须是序列或序列表达式。即使该属性仅包含序列表达式，它也不能是属性。

如果您声明always_another_valid_input为 asequence而不是 a property，您的代码将编译

sequence always_another_valid_input;
   @(posedge clock) ##[1:$] valid_input;
endsequence