SVA介绍----SVA检验器(参数/选择运算符/true表达式)

SVA检验器

• 使用参数的SVA检验器
• 使用选择运算符的SVA检验器
• 使用true表达式的SVA检验器

使用参数的SVA检验器

SVA允许像verilog一样在检验器中使用参数，这位创建可重用的属性提供了很大的灵活性，比如两个信号之间的延迟信息就可以参数化。

//声明参数化的检验器
module gen_chk(input logic a,b,clk);
	parameter delay =1;
	property p16;
		@(posedge clk) a |-> ##delay b;
	endproperty
	a16: assert property(p16);
endmodule
//例化
module top();
	logic clk,a,b,c,d;
	.....
	gen_chk  #(.delay(2))  i1 (a,b,clk);  //将delay修改为2
	gen_chk                i2 (c,d,clk);  //使用默认delay=1
	.....
endmodule
           

使用选择运算符的SVA检验器

SVA允许在序列和属性中使用逻辑运算符，如三目运算符。

//属性p17检查：
//c为高，d==a； c为低，d==b；
property p17;
	@(posedge clk) c ? d==a : d==b; //在同一个时钟沿检查
endproperty
a17: assert property(p17);
           

使用true表达式的SVA检验器

使用true表达式，可以在时间上延长SVA检验器的结束时间，代表一种忽略的状态，使得序列延长，可以用于实现同时检测多个属性且需要同时成功的复杂协议。

`define true 1
//define sequence
sequence s18a;
	@(posedge clk)  a ##1 b;
endsequence
sequence s18a_ext;
	@(posedge clk)  a ##1 b ##1 `true;
endsequence
sequence s18b;
	@(posedge clk)  c ##1 d;
endsequence
//define property
property p18;
	@(posedg  clk)  s18a.ended |-> ##2 s18b.ended;
endproperty
property p18_ext;
	@(posedg  clk)  s18a_ext.ended |=> s18b.ended;
endproperty
a18 : assert property(p18);          //两个属性检查相同的成功条件
a18_ext : assert property(p18_ext);  //但是，两个属性的先行算子成功点不同，ext晚一个时钟周期。