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 【仿真结果】 
示例中，子程序的用法与局部变量类似，都是附加在相应的子序列之后，用逗号分隔。在$rose(sig0)匹配时，调用了子程序disp。在sequence s匹配的最后，也调用了子程序，同时将局部变量传递给了子程序disp，子程序在每次调用后都会对传入的变量值进行一定的处理。
在SVA中，合理的使用局部变量和子程序可以实现更加复杂的功能描述，同时增加了断言检查的灵活性。但是一般不要将设计结构的实现放在SVA中的子程序中，因为断言一般仅用于检查，不用于具体的电路的实现，通常的综合工具不会将断言实现为具体的电路。
