SVA中的延迟

在并行断言中，因为所有的行为都是基于采样事件而进行的，为了更好的描述时序关系，SVA中增加了基于采样事件的延迟，其格式有如下两种方式：

##m;
##[m:n];

其中m和n都是非负数，m可以为0，n可以为$，n必须大于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 sig1 = 1'b1;   sig0 = 1'b0;
    #2 sig1 = 1'b0;#4 sig2 = 1'b1;#2 sig2 = 1'b0;
    #4 $stop;
end
// property
property p;
    @(posedge clk) sig0 |-> ##1 sig1 ##3 sig2;
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb

【仿真结果】

示例中，sig0发生一个采样周期后sig1被采样到为高电平，在经过3个采样周期（##3）sig2被采样到高电平，此时序列匹配。这里的##3指的是三个采样周期，不是三个时间单位。当然m不止可以为正数，也可以为0，如下例。

【示例】

`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;sig2 = 1'b1;
    #2 sig1 = 1'b0;sig2 = 1'b0;#4 $stop;
end
// property
property p;
    @(posedge clk) sig0 |-> ##1 sig1 ##0 sig2;
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb

【仿真结果】

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

除了使用上例中固定的具体延迟外，还存在一种延迟区间，即时序窗口，如下例。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic       clk;
logic       sig0;
logic [4:0] sig1;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end
initial begin
    sig0 = 1'b0;sig1 = 5'b0_0000;
#2 sig0 = 1'b1;
#2 sig1 = 5'b0_0001;sig0 = 1'b0;
#2 sig1 = 5'b0_0010;
#2 sig1 = 5'b0_0100;
#2 sig1 = 5'b0_1000;
#2 sig1 = 5'b1_0000;
#2 sig1 = 5'b0_0000;
#4 $stop;
end
// property p
property p(num);
    @(posedge clk) $rose(sig0) |-> ##[2:4] sig1[num]
endproperty // p
// assertion
genvar i;
generate for (i = 0;i < 5;i = i +1) begin : a_loop
    a : assert property(p(i)) $display("@%0t | p[i] : PASSED!",$time,i);
        else $display("@%0t | p[i] : FAILED!",$time,i);
    end
endgenerate // a_loop
endmodule // top_tb

【仿真结果】

示例中，针对sig1的每一位开启了3个并行的检查进程，其中sig1[0]开启的序列为：

序列1：$rose(sig0) |-> ##2 sig1[0];

序列2：$rose(sig0) |-> ##3 sig1[0];

序列3：$rose(sig0) |-> ##4 sig1[0];

仿真过程中，会分别判断上述三个序列，因为对于sig1[0]来说在整个检查的过程中，序列1、序列2和序列3都不匹配，所以整个属性都不匹配，并且从示例中可以看出，属性失败取决于最长的那个序列。

sig1[4]和sig1[0]的情况类似，不再赘述。

sig1[1]和sig1[2]、sig1[3]情况类似，在第一次匹配后整个属性断言成功了，不同的是，这三个信号分别在##2、##3、##4匹配成功。

【示例】

`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 sig1 = 1'b1;sig0 = 1'b0;
#10 $stop;
end
// property p
property p;
    @(posedge clk) $rose(sig0) |-> ##[2:4] sig1;
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb

【仿真结果】

示例中，可以看到“##[2:4]sig1”虽然对sig1开启了三个并行的检查序列，但是在第一个序列（##2 sig1）检查成功后，不管第二个（##3 sig1）和第三个（##4 sig1）序列是否匹配，对应的进程都会***掉，即“##[m:n]”采取的是“就近匹配”原则，在第一个序列匹配后将不会在进行后续序列的匹配。那么“##[m:n]”中还有必要使用其中的“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;sig1 = 1'b1;
    #6 sig2 = 1'b1;#2 sig2 = 1'b0;#2 $stop;
end
// property p
property p;
    @(posedge clk) $rose(sig0) |-> ##[2:4] sig1 ##1 sig2;
endproperty // p
// assertion
a : assert property(p) $display("@%0t | p : PASSED!",$time);
    else $display("@%0t | p : FAILED!",$time);
endmodule // top_tb

【仿真结果】