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最后一次出现的下一个周期。

各个运算符图示如下：