SVA(systemverilog assertion)序列循環算子[*] [->] [=]

• [*n : $], [*] [+]連續循環，是針對sequence的連續循環

[* n：$]結構類似于[* n：m]，除了m被$符取代，$符代表無限的意思，并且n意味着重複最少n個周期。 [*]是[* 0：$]的縮寫，表示重複至少0次，最多無限次。 [+]是[* 1：$]的縮寫，表示重複至少1次，最多無限次。

• [=n], [=n:m] 非連續循環算子

能夠對不連續的循環進行評價，循環評價結束時，不連續的可能性依然繼續。重複次數可以是固定常數或固定範圍。

b[=m] is equivalent to ( b [->m] ##1 !b [*0:$]
           

b[=1] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$]
b[=2] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]
           

(a) |=> (b[=2] ##1 c);

該屬性指出，如果從a成立下一個周期開始，那麼b應該成立兩次，b要麼是連續的要麼是不連續的，然後稍後一段時間（即下一個周期或之後）出現c。

如果在第二次出現b後出現新的b（且 c 沒有成立），則該屬性失敗。

但是，如果在b的第二次成立之後，c在新的b之前的任何時間發生，或者與最後一次b同時出現，則屬性成功。

• [->n ], [->n:m] goto循環算子

goto循環算子（Boolean[ - > n]）允許布爾表達式（而不是序列）在連續或不連續的循環中重複，而且循環評價結束時，不連續的可能性也結束了。 重複次數可以是固定常數或固定範圍。

b [->m] is equivalent to ( !b [*0:$] ##1 b)[*m]
           

b[->1] is equivalent to:
!b[*0:$] ##1 b
b[->2] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b
           

（a）|=>（b [->2] ## 1 c）;

上述屬性指出，如果從a成立下一個周期開始，那麼b應該成立兩次，它可以是連續的或不連續的。 但是，c必須發生在b最後一次出現的下一個周期。

各個運算符圖示如下：