如何在斷言中使用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