SVA中的重复运算操作

当需要检查某个信号保持一种状态多个采样周期时，虽然在SVA中可以使用连续##1逐个指定该信号，如下例，sig1要在sig0为上升沿之后保持4个时钟周期的高电平。

【示例】

……

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

……

虽然实现了特定的要求，但是这种实现方式明显很繁琐，为此，在SVA中提供了重复运算符，从而可以缩减繁琐的表达式，而这些重复运算符根据其实现的功能又分为三大类，具体有如下表所示。

重复运算符	说明	格式
连续重复（consecutive repetition）	表达式或者序列在指定数量的采样周期内连续的匹配，表达式或者序列的每次匹配之间都有一个采样周期的延迟。	expr or sequence_name[n] expr or sequence_name[m:n]
跟随重复（goto repetition）	表达式匹配达到指定的次数，而且每次匹配不一定在连续的采样周期上，被检验的重复表达式的最后一个匹配应该发生在整个序列匹配结束之前	expr[->n] expr[->m:n]
非连续重复（non-consecutive repetiton）	与跟随重复类似，除了它并不要求信号的最后一次匹配发生在整个序列匹配前的那个采样周期	expr[=n] expr[=m:n]

注意，跟随重复与非连续重复只允许使用表达式，不能使用序列。

1 [*m]和[*m:n]

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

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end
initial begin
        sig0 = 1'b0;   sig1 = 1'b0;
    #2  sig0 = 1'b1;#2 sig0 = 1'b0;sig1 = 1'b1;
    #10 sig1 = 1'b0;#4 $stop;
end
// property p
property p;
    @(posedge clk) $rose(sig0) |-> ##1 sig1[*5];
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb

【仿真结果】

示例中$rose(sig0)后，sig1从下一个采样周期开始连续保持了5个采样周期的高电平。

[*m:n]使用时表达式或者序列每次匹配间隔为一个采样周期，表达式或者序列重复m到n次，当m次匹配后，即认为[*m:n]匹配成功，不会再对表达式进行后续的匹配判断，即其本身匹配采取的是“就近匹配”原则。当然n的存在也是有一定意义的，如果[*m:n]后还存在其他表达式或者序列，那么其他表达式或者序列的匹配检查点将不能超过第n次匹配，其格式如下：

由上图示意可见在“[*m:n]”后如果还有其他序列存在，那么“[*m:n]”类似于同时开启了多个并行的序列，并且各并行序列在属性检查中是一种“或”的关系。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end
initial begin
        sig0 = 1'b0; sig1 = 1'b0;
    #2  sig0 = 1'b1;
    #2  sig0 = 1'b0; sig1 = 1'b1;
    #10 sig1 = 1'b0;
    #2  sig0 = 1'b1;
    #2  sig0 = 1'b0; sig1 = 1'b1;
    #4  sig1 = 1'b0;#4 $stop;
end
// property
property p;
    @(posedge clk) sig0 |-> ##1 sig1[*2:5];
endproperty // p
// assert
a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb

【仿真结果】

示例中，当sig1连续2两个采样周期为高，即认为“sig1[*2:5]”为真，不用等到sig1保持5个采样周期。那么，“sig1[*2:5]”中的“5”有什么作用呢？请看下面的示例。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2,sig3;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end
initial begin
        sig0 = 1'b0; sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;
    #2  sig0 = 1'b1; sig1 = 1'b1;
    #2  sig0 = 1'b0; sig1 = 1'b0;sig2 =1'b1;
    #8  sig2 = 1'b0;
    #2  sig3 = 1'b1;
    #2  sig3 = 1'b0;
    #1 $stop;
end
// property
property p1;
    @(posedge clk) $rose(sig0) |-> sig1 ##1 sig2[*1:4] ##2 sig3;
endproperty // p1
property p2;
    @(posedge clk) $rose(sig0) |-> sig1 ##1 sig2[*1:4];
endproperty // p2
// assert
a1 : assert property(p1) $display("@%0t | p1 : PASSED!",$time);
    else $display("@%0t | p1 : FAILED!",$time);
a2 : assert property(p2) $display("@%0t | p2 : PASSED!",$time);
    else $display("@%0t | p2 : FAILED!",$time);
endmodule // top_tb

【仿真结果】

示例中，“$rose(sig0) |-> sig1 ##1 sig2[*1:4]”在5ns匹配成功，因为sig2此时有一个采样时钟的匹配，即p2匹配成功，可见sig2并不需要等到4个采样周期后匹配，其在第一个采样周期就已经匹配了。如果“$rose(sig0) |-> sig1 ##1 sig2[*1:4]”之后还有序列或者表达式，那么该序列或者表达式检查的起始点为“$rose(sig0) |-> sig1 ##1 sig2[*1:4]”距离该序列或者表达式最近的匹配位置。p1中sig3就发生在sig2保持三个采样周期匹配后的两个采样周期，此时sig2并没有在第一个采样周期匹配时就结束。在使用“[*m:n]”时，m也可以设置为0，此时表示sequence[*0:n]中的sequence可以不发生。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2,sig3;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
    sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;
    #2 sig0 = 1'b1;sig1 = 1'b1;
    #2 sig1 = 1'b0;sig0 = 1'b0;
    #2 sig3 = 1'b1;sig1 = 1'b0;
    #4 $stop;
end

property p;
    @(posedge clk) $rose(sig0) |-> sig1 ##1 sig2[*0:2] ##2 sig3;
endproperty // p

a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);
endmodule

【仿真结果】

示例中，虽然sig2并没有发生，但是整个属性的断言还是成功的，是因为指定的sig2匹配情况为为”sig2[*0:2]”，即sig2在0至2两个采样周期内最多只要匹配一次即可，示例中sig2匹配了0个采样周期，所以此时”##1 sig2[*0:2]”匹配。注意”##1 sig2[*0:2]”中的##1不会因为sig2不发生就叠加到后续的表达式中，即表达式不会因为sig2不发生变成”$rose(sig0) |-> sig1 ##3 sig3”。

2 [->m]和[->m:n]

[->m]使用时表示表达式重复连续匹配出现m次，但是整个重复表达式的最后一次匹配必须发生在其后续表达式匹配前的一个采样周期，其使用格式一般如下：

exp[->m]

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
       sig0 = 1'b0;sig1 = 1'b0;sig2= 1'b0;
    #2 sig0 = 1'b1;
    #2 sig1 = 1'b1;sig0 = 1'b0;
    #2 sig1 = 1'b0;
    #4 sig1 = 1'b1;
    #2 sig1 = 1'b0;
    #6 sig1 = 1'b1;
    #2 sig2 = 1'b1;sig1 = 1'b0;
    #2 sig2 = 1'b0;
    #2 $stop;
end

property p;
    @(posedge clk) sig0 |-> ##1 sig1[->3] ##1 sig2;
endproperty // p

a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb

【仿真结果】

示例中，sig1在先序算子匹配后完成了三次匹配，在第三次匹配后的紧接着的采样周期sig2采样为真，整个序列匹配成功。如果第三次匹配后紧接着的采样周期sig2不为高，那么该序列匹配失败。通过示例可以看到作为重复表达式的sig1，并没有在连续的采样周期或者特定间隔的采样周期匹配三次，说明[->m]对于其表达式出现的方式并没有严格的要求，只要最后一次匹配发生在其后续表达式匹配成功前的一个采样周期即可。同样[->m]也有对应的[->m:n]方式，其差别与[*m]和[*m:n]差别类似，不再赘述，此处给出示例如下。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
       sig0 = 1'b0;sig1 = 1'b0;sig2= 1'b0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;#2 sig1 = 1'b1;
    #2 sig1 = 1'b0;#4 sig1 = 1'b1;#2 sig1 = 1'b0;
    #6 sig1 = 1'b1;#2 sig1 = 1'b0;#5 sig1 = 1'b1;
    #2 sig1 = 1'b0;#8 sig1 = 1'b1;#2 sig1 = 1'b0;sig2 = 1'b1;
    #2 sig2 = 1'b0;#2 $stop;
end

property p1;
    @(posedge clk) sig0 |-> ##1 sig1[->2:5] ##1 sig2;
endproperty // p1

property p2;
    @(posedge clk) sig0 |-> ##1 sig1[->2:5];
endproperty // p2

a1 : assert property(p1) $display("@%0t | p1 : PASSED!",$time);
     else $display("@%0t | p1 : FAILED!",$time);
a2 : assert property(p2) $display("@%0t | p2 : PASSED!",$time);
     else $display("@%0t | p2 : FAILED!",$time);
endmodule // top_tb

【仿真结果】

仅使用“sig0 |-> ##1 sig1[->2:5]”，其后如果没有其他的表达式，那么匹配采取“就近原则”，即满足最少匹配次数即认为整个属性匹配成功。

3 [=m]和[=m:n]

[=m]和 [->m]工作情况类似，唯一的区别是 [->m]要求整个重复表达式的最后一次匹配必须发生在其后续表达式匹配的前一个相邻采样周期，而[=m]并没有要求整个重复表达式的最后一次匹配必须发生在一定的条件下。[=m]的格式一般如下：

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end

initial begin
       sig0 = 1'b0;   sig1 = 1'b0;    sig2 = 1'b0;
    #2 sig0 = 1'b1;#2 sig0 = 1'b0;#2  sig1 = 1'b1;
    #2 sig1 = 1'b0;#4 sig1 = 1'b0;#2  sig1 = 1'b0;
    #6 sig1 = 1'b1;#2 sig1 = 1'b0;#20 sig2 = 1'b1;
    #2 sig2 = 1'b0;#2 $stop;
end

property p1;
    @(posedge clk) sig0 |-> ##1 sig1[=2] ##1 sig2;
endproperty // p1

property p2;
    @(posedge clk) sig0 |-> ##1 sig1[=2];
endproperty // p2

a1 : assert property(p1) $display("@%0t | p1 : PASSED!",$time);
     else $display("@%0t | p1 : FAILED!",$time);
a2 : assert property(p2) $display("@%0t | p2 : PASSED!",$time);
     else $display("@%0t | p2 : FAILED!",$time);
endmodule // top_tb

【仿真结果】

示例中，sig1匹配两次后表示“sig1[=2]”匹配成功，如图中断言a2所示。如果“sig1[=2]”后续还有其他表达式，那么“sig1[=2]”并没有要求后续的表达式在sig1第二次匹配后的下一个采样周期匹配，即对于sig2发生在“sig1[=2]”之后的采样周期数没有具体要求，如仿真波形中的断言a1所示。[=m]和[=m:n]的差别与 [*m]和[*m:n]之间的差别类似，这里不再赘述。