如何在断言中使用 SystemVerilog 序列属性？答案

【问题标题】：How can I use SystemVerilog sequence properties in asserts?如何在断言中使用 SystemVerilog 序列属性？
【发布时间】：2017-03-08 14:43:31
【问题描述】：

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

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

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

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。

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

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

【问题讨论】：

标签： system-verilog system-verilog-assertions

【解决方案1】：

请参阅IEEE Std 1800-2012 § 16.12 声明属性，更具体地说是§ 16.12.6 含义，您将看到|-> 语法用法描述为：

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

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

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

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

【讨论】：