SVA介绍----一个简单的断言

一个简单的断言

• • 1. 序列
  • 2. 属性
  • 3. 断言和执行块

1. 序列

• 1.1 简单的信号检查序列：

// 序列s1检查信号‘a’在每个时钟上升沿都为高电平：
seuqnce s1;
	@(posedge clk) a;
endsequence
           

• 1.2 边沿定义的序列

// 序列s2检查信号‘a’在每个时钟上升沿为上升沿/下降沿/保持稳定：
seuqnce s2;
	@(posedge clk) $rose(a);      //当信号/表达式出现上升沿时返回真；
	@(posedge clk) $fell(a);      //当信号/表达式出现下降沿时返回真；
	@(posedge clk) $stable(a);    //当信号/表达式保持稳定时返回真；
endsequence
           

• 1.3 逻辑关系检查序列：

// 序列s3检查信号‘a’或'b'在每个时钟上升沿都为高电平：
seuqnce s1;
	@(posedge clk) a||b;
endsequence
           

• 1.4 带形式参数的序列

// 序列s4检查信号‘a’或'b'在每个时钟上升沿都为高电平，其中a/b为形式参数：
seuqnce s4(a,b);
	a||b;
endsequence
seuqnce s4_inst1;
	s4(sig0,sig1);
endsequence
           

• 1.5 时序关系检查序列：

// 序列s3检查信号‘a’在每个时钟上升沿都为高电平，并且两个时钟周期后b为高电平；
seuqnce s5;
	@(posedge clk) a ##2 b;
endsequence
           

2. 属性

• 2.1 普通属性定义

  一个序列在模拟过程中并不能起什么作用，他们必须像下面的例子那样被断言才能发挥作用；

//序列
seuqnce s5;
	@(posedge clk) a ##2 b;
endsequence
//属性
property p5;
	s5;
endsequence
//断言
a5： assert(p5);

//序列
seuqnce s5a;
	a ##2 b;
endsequence
//属性
property p5a;
	@(posedge clk) s5a;
endsequence
//断言
a5a： assert(p5a);
a5b: assert property(@(posedge clk) s5a); //错误，不能在属性和断言中重复定义时钟
           

通常情况下，在属性(property)的定义中指定时钟，并保持序列(sequence)独立于时钟是一种很好的编码风格，可以提高序列的可重用性。

//断言有时候不需要定义一个独立的属性
seuqnce s5b;
	a ##2 b;
endsequence
a5b: assert property(@(posedge clk) s5b);
           

• 2.1 禁止属性定义

//属性有时可以定义为禁止发生
//序列
seuqnce s6;
	a ##2 b;
endsequence
//属性，与属性p5取值相反
property p6;
	@(posedge clk) not s5a;
endsequence
//断言
a6： assert(p6);
           

3. 断言和执行块

system verilog被定义为每当一个断言检查失败，模拟器在默认情况下打印一条错误信息，模拟器不需要对成功的断言打印任何东西，读者同样也可以使用断言程序中“action block”来定义自定义的成功失败信息，执行块的基本语法如下所示：

assertion_name : 
	assert property(property_name)
		<success message>;
	else
		<fail message>;
//如下所示：
property ： p7;
	@(posedge clk)  a ##2 b;
endproperty
a7:  assert property(p7)
		$dispaly("property p7 successed.\n");
	 else
	 	$dispaly("property p7 failed.\n");