Assertion介绍

1. 什么是assertion？

• 用来与设计功能和时序作比较的属性描述

• 断言可以用来完成：

  • 检查设计的内容
  • 提高设计的可视度和调试能力
  • 检查设计特性在验证中是否被覆盖

• 可读性好，可以用来服务于设计文档；

• 用来检查算法模型的断言在形式验证（formal verification）中可以穷尽计算，找出可能的违例（violation）；

• 可以自由地打开或者关闭；

• 一小部分子集甚至可以用来综合或者移植到emulation中，用来完成跨平台地移植；

2. 基于断言地验证方法学（ABV）

• Assertion Based Verification（ABV）方法学会定义断言如何被使用：
  • 谁写断言？
  • 哪种语言可以用来写断言？
  • 断言可以写在哪里？
  • 可以使用哪些断言库（library）？
  • 断言如何调试？
  • 如何使用形式验证工具？
  • 如何使用断言覆盖率？

3. 断言覆盖率

• 仿真工具可以报告断言覆盖率，来指示哪些断言没有被触发？
• 帮助检查是否验证计划捕捉到了所有需要地覆盖率；
• 断言覆盖率和功能覆盖率可以共同量化验证进度；

4. 断言语言的发展与进步

• 在Verilog中不支持断言，因此需要写过程语句来做替代；
• 一些语言支持断言:
  • Sugar (IBM）进化为PSL (Property Specification Language)
  • OVA-Vera
  • Specman/e
  • ForSpec (Intel)
• 上述语言的优点功能进化为SVA，因此SVA作为SV相对独立的语言分支，值得我们花足够的精力来学习掌握它；

5. 类型划分

• 立即断言（immediate assertion）：
  • 非时序的
  • 执行时如同过程语句
  • 可以在initial / always过程块或者task / function中使用
• 并行断言（concurrent assertion）：
  • 时序性的
  • 关键词property用来区分立即断言和时序断言
  • 之所以称之为并行，是因为它们与设计模块一同并行执行

6. 立即断言

[name:] assert(expression)[pass_statement][else fail_statement]

// 如果状态为REQ，但是req1或者req2均不为1时，断言将失败
time t;
always @(posedge clk)
	if(state == REQ)
		assert(req1 || req2)
		else begin
			t = $time;
			#5 $error("assert failed at time %0t", t);
		end

1
2
3
4
5
6
7
8
9
10
11
12

• 立即断言可以结合$fatal / $error / $warning / $info给出不同严重级别的消息提示
• 规定立即断言和并行断言都不可以修改设计行为

assert(myfunc(a, b)) count1 = count + 1; else ->event1;
assert(y == 0) else flag = 1;
always @(state)
	assert(state == $onehot) else $fatal;
	
1
2
3
4
5

7. 并行断言

base_rule1: assert property(cont_prop(rst, in1, in2)) pass_stat else fail_stat;

// Request-Grant协议描述：
// request拉高，在2个周期后，grant拉高，在1个周期后，request拉低，在1个周期后，grant拉低
property req_grant_prop
	@(posedge clk) req ##2 gnt ##1 !req ##1 !gnt;
endproperty

assert property req_grant_prop else $error("Req-Gnt Protocol violoation");

1
2
3
4
5
6
7
8
9
10

• 并行断言只会在时钟边沿激活，变量的值是采样到的值
• SV的仿真调度机制可以保证并行断言执行会采样的稳定的设计信号变量

8. assertion, property, sequence

• assertion可以直接包含一个property；
• assertion也可以清晰地独立地声明property；
• 在property内部可以有条件地关闭；

// assertion可以直接包含一个property
assert property(@(posedge clk))
	disable iff(!reset)	// property内部可以设置条件来关闭或打开
	a |=> b ## 1 c;

// assertion也可以清晰地独立地声明property
assert property(my_prop);
property my_prop;
	@(posedge clk);
		disable iff(!reset);	// property内部可以设置条件来关闭或打开
		a |=> b ## 1 c;
endproperty

1
2
3
4
5
6
7
8
9
10
11
12
13

• property块可以直接包含sequence；
• 复杂地property也可以独立声明多个sequence；

sequence s1;
	@(posedge clk) a ##1 b ##1 c;
endsequence

sequence s2;
	@(posedge clk) 1 ##1 c;
endsequence

property p1;
	@(posedge clk) disable iff (!reset)
	s1 |=> s2;
endproperty
1
2
3
4
5
6
7
8
9
10
11
12

• 说明：UVM中的seq是为了生成发送一些激励，这里的seq是为描述一种时序
• |=>运算符

9. sequences

• sequence是用来表示在一个或者多个时钟周期内的时序描述
• 是property的基本构建模块，并经过组合来描述复杂的功能属性

sequence s1;
	@(posedge clk) a ##1 b ##1 c;
endsequence

sequence t2;
	(a ##[2:3] b) or (c ##[1:2] d);
endsequence

1
2
3
4
5
6
7
8

• sequence用来提供下列的场景描述：

  • 第一个时钟周期，第一个表达式成立的；
  • 接下来若干个时钟周期后，第二个表达式也成立；
  • 以此类推，在接下来的若干时钟周期，后续的表达式也成立；

• sequence可以在module、interface、program、clocking块和package中声明；

• sequence不可以在类中声明，property会把sequence包含起来使用，property要被设置断言来检查或者覆盖sequence，检查和覆盖也不能发生在类中

• sequence也可以提供形式参数，用来提高复用性

sequence s20_1(data, en);
	(!frame && (data = data_bus)) ##1 (c_be[0:3] == en);
endsequence

1
2
3
4

• 蕴含（implication）操作符用来表示，如果property中左边的先行算子（antecedent）成立，那么property右边的后续算子（consequent）才会被计算；

• 如果先行算子不成功，那么整个属性就默认地被认为成功，这叫做“空成功”（vacuous success）；

• 蕴含结构只能用来属性定义中，不能在序列中使用；

• 蕴含可以分为两类：交叠蕴含（overlapped implication）和非交叠蕴含（non-overlapped implication）；

• |->操作符是交叠交错符号

  • 如果条件满足，则在当拍评估其后续算子序列
  • 如果条件不满足，则表现为空成功，不执行后续算子
    

• |=>操作符是非交叠交错符号

  • 如果条件满足，则在下一个周期评估其后续算子序列；
  • 如果条件不满足，则表现为空成功，不执行后续算子；