如何在断言中使用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声明属性，更具体地说是§16.12.6含义，您将看到|->语法ussage被描述为：

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