SVA中的局部变量和子程序

1 局部变量

局部变量是动态存在于属性或者序列中的，对其他属性或者序列不可见，即不能在其他属性或者序列中引用，当其所在的属性或者序列执行完毕其生命周期也就宣告结束了。局部变量的使用方法是将局部变量接着子序列放置，两者用逗号隔开，并且置于同一个小括号中，如果自序列匹配，那么变量赋值语句即被执行，每次序列检查匹配结束时，会重新产生变量的一个备份。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2,sig3;
logic [3:0] num_src,num_des;

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

initial begin
    sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;
    num_src = 4'b0000;num_des = 4'b0000;
    #2 sig0 = 1'b1;
    #2 sig0 = 1'b0;sig1 = 1'b1;#2 sig1 = 1'b0;sig2 = 1'b1;num_src = 4'b0001;
    #2 sig1 = 1'b1;sig2 = 1'b0;#2 sig1 = 1'b0;sig2 = 1'b1;num_src = 4'b0101;
    #2 sig1 = 1'b1;sig2 = 1'b0;#2 sig1 = 1'b0;sig2 = 1'b1;num_src = 4'b0110;
    #2 sig3 = 1'b1;num_des = 4'b0001 + 4'b0101 + 4'b0110;
    #2 sig3 = 1'b0;#6 $stop;
end

sequence s;
int lvar = 0;
    (sig1 ##1 sig2,lvar = lvar +num_src)[*3] ##1 ($rose(sig3) && (lvar == num_des));
endsequence // s
property p;
    @(posedge clk) $rose(sig0) |-> ##1 s;
endproperty // p
a : assert property(p) $info("@%0t | p : PASSED!",$time);
    else $info("@%0t | p : FAILED!",$time);
endmodule // top_tb

【仿真结果】

示例中，检测到sig0出现上升沿一个采样周期后，子序列“(sig1 ##1 sig2,lvar = lvar +num_src)”匹配了三次，并且在这三次发生的过程中，num_src的值在每次“sig1##1 sig2”匹配时都会累加到局部变量lvar中。三次匹配完成后的一个采样周期sig3拉高的同时比较lvar中的累加的值是否与此时num_des中的值相等，如果想等，则断言匹配成功，反之失败。在使用局部变量时要注意以下几点：

在有形式参数的属性或者序列中，局部变量名不能与形参名相同；
局部变量不能用于延迟范围中指示延迟，因为延迟范围需要在代码析构时就必须确定，而局部变量只有在调用时才存在；
局部变量不能用于信号位宽的指定，因为信号位宽需要在代码析构时就必须确定，而局部变量只有在调用时才存在；
局部变量仅限于在当前定义的序列或者属性中可见；

2 调用子程序

【注】本小节中将function和task统称为子程序，仅为描述方便。

SVA除了可以检测一些属性序列外，还可以在断言中调用一些子程序，实现一些复杂的功能，也可以将序列或者属性中的局部变量作为参数传递给子程序，辅助断言对设计属性的描述。其使用格式与局部变量类似，都是用逗号将其与子序列分割，但是通过小括号将其与子序列组织在一起。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig0,sig1,sig2,sig3;
logic [3:0] num_src,num_des;

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

initial begin
    sig0 = 1'b0;sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;
    num_src = 4'b0000;num_des = 4'b0000;
    #2 sig0 = 1'b1;
    #2 sig0 = 1'b0;sig1 = 1'b1;#2 sig1 = 1'b0;sig2 = 1'b1;num_src = 4'b0001;
    #2 sig1 = 1'b1;sig2 = 1'b0;#2 sig1 = 1'b0;sig2 = 1'b1;num_src = 4'b0101;
    #2 sig1 = 1'b1;sig2 = 1'b0;#2 sig1 = 1'b0;sig2 = 1'b1;num_src = 4'b0110;
    #2 sig3 = 1'b1;num_des = 4'b0001 + 4'b0101 + 4'b0110;
    #2 sig3 = 1'b0;#6 $stop;
end

sequence s;
int lvar = 0;
    (sig1 ##1 sig2,lvar = lvar +num_src)[*3] ##1 ($rose(sig3) && (lvar == num_des),disp(lvar));
endsequence // s
property p;
    @(posedge clk) ($rose(sig0),disp(4'b0000)) |-> ##1 s;
endproperty // p
a : assert property(p) $info("@%0t | p : PASSED!",$time);
    else $info("@%0t | p : FAILED!",$time);
// task&nbs***bsp;function
task disp(input int lvar);
    $display("@%0t %m local var : %h happened!",$time,lvar);
endtask // disp
endmodule // top_tb

【仿真结果】