目录

1.延时操作符（##）

1.1 ##m

1.2 ##[m:n]

2.蕴含操作符（|=>,|->）

2.1 |=>操作符

2.2 |->操作符 

3 重复操作符 ([*m][->m][=m])

3.1 连续重复操作符（[*m][*m:n]）

3.2 跟随重复操作符（[->m][->m:n]）

        3.3 非连续重复操作符（[=m]）

3.4 小结

1.延时操作符（##）

1.1 ##m

示例：

sequence seq2;

        @(posedge clk) a ##2 b ;

endsequence

//在断言的property中调用sequence

check_a_and_b: assert property(seq2);

提示：##0  表示 sig1 和 sig2 必须同时发生才算成功 ，可见，在具体使用过程中，可以使用 ##0 表示两个事件在同一采样时刻同时发生

波形展示：

 sequence只有在时钟上升沿到来后检查a是否为1才会继续检查后面连续x个时钟后的b的值；

1.2 ##[m:n]

##[m:n] 其中m和n都是非负数，m可以为0，n可以为$，n必须大于m，当n为$时，比 较耗费仿真资源，一般不建议使用.

示例：

sequence seq2;

        @(posedge clk) a ##[2:4] b ;

endsequence

//在断言的property中调用sequence

check_a_and_b: assert property(seq2);

 ##[m:n]”采取的是“就近匹配”原则，在第一个序列匹配后将不会在进行后续序列的匹配。

2.蕴含操作符（|=>,|->）

2.1 |=>操作符

示例：

property p1;

        @(posedge clk) sig1 |=> sig2;

endproperty // p1

波形展示：

 表示sig1在时钟上升沿时为高，在当前时钟上升沿的下一个时钟上升沿时sig2也必须为高

2.2 |->操作符 

示例：

property p1;

        @(posedge clk) sig1 |-> sig2;

endproperty // p1

sig1在时钟上升沿时为高，在当前时钟上升沿sig2也必须为高 

NOTE：在编写断言时尽量使用“｜->”而不是“｜=>”，因为你可以通过“｜->”后增加时钟数实现“｜=>”的功能， 但是不能通过“｜=>”实现“｜->”的功能。

 断言时序判断note：例如（cat ##1 dog）|=> mouse

1. 首先判断cat是否为真，只有在cat为真的情况下才会进行后续判断，才会开启以上断言；

2. 遇到如果第二个clk如果依旧为cat，则将其作为初始cat进行判断（上图条件3）；

3 重复操作符 ([*m][->m][=m])

示例：

……

@(posedge clk) $rose(sig0) |-> ##1 sig1 ##1 sig1 ##1 sig1##1 sig1;

……

3.1 连续重复操作符（[*m][*m:n]）

[*m]使用时表达式或者序列每次匹配间隔为一个采样周期，表达式或者序列必须连续重复匹配m次，m不能为$。

[*m:n]使用时表达式或者序列每次匹配间隔为一个采样周期，表达式或者序列重复m到n次，

当m次匹配后，即认为[*m:n]匹配成功，不会再对表达式进行后续的匹配判断，即其本身匹配

采取的是“就近匹配”原则。当然n的存在也是有一定意义的，如果[*m:n]后还存在其他表达

式或者序列，那么其他表达式或者序列的匹配检查点将不能超过第n次匹配。

 

 示例：

property p;

        @(posedge clk) $rose(a) |-> ##1 b[*2];

endproperty // p

提示：

在仿真中$rose并不是单纯的判断信号的跳边沿，而是判断时钟采样信号前后是否存在0->1/x->1/z->1的变化。

在仿真中$fell并不是单纯的判断信号的跳边沿，而是判断时钟采样信号前后是否存在1->/x->0/z->0的变化。

3.2 跟随重复操作符（[->m][->m:n]）

 示例：

property p;

        @(posedge clk) a |-> ##1 b[->3] ##1 a;

endproperty // p

波形展示：

[->m]也有对应的[->m:n]方式，其差别与[*m]和[*m:n]差别类似，不再赘述 .