0、基于断言的 验证

测试平台的自检机制，通常关注两个方面：

• （1）协议检验：检验控制信号
• （2）数据检验：检验正在处理的数据的完整性

功能覆盖用于衡量验证的完整性，衡量指标包括两项指定的信息：

• （1）协议覆盖（Protocol Converage）：协议覆盖在所有合法和不合法的情况下衡量一个设计，即用来衡量一个设计的功能说明书（function specification）中的所有功能是否都测试过
• （2）测试计划覆盖（Test Plan Converage）：用来衡量测试平台的穷尽性

SVA（SystemVerilog Assertion）着重处理两大类问题：

• （1）协议检验
• （2）协议覆盖
  SVA 直接将设计断言与设计相连，与设计信号交互，但他仍然可以和测试平台很有效的共享信息。

1、SVA 介绍

1.1.、什么是断言

断言是设计的属性的表示：

• 如果一个在模拟中被检查的属性（property)与期望的表现不同，则断言失败
• 如果一个被禁止在设计中出现的属性在模拟过程中发生，则断言失败

示例：相互断言条件检查的Verilog 实现

// 若a和b同时为高电平，则报错（断言失败）
`ifdef ma
if(a&b)
$display("Error: Mutually asserted check failed.\n")
`endif

// 只有当需要时才被纳入设计环境中。可以通过允许 Verilog 条件编译指令 “ `ifdef ” 来实现

1.2、为什么使用 SystemVerilog 断言（SVA）

使用 Verilog 检查的不足：

• （1）Verilog 时一种过程语言，不能控制时序
• （2）Verilog 比较冗长复杂，随着断言数量增加而不方便维护
• （3）Verilog 的检验器可能无法捕捉到所有被触发的并行事件
• （4）Verilog 语言没有提供内嵌的机制来提供功能覆盖率的数据，需要用户自己实现

SVA：一种描述性语言，可以很好的描述时序相关的状况；精确且易于维护；SVA提供了若干内嵌函数用来测试特定的设计情况，并且提供了一些构造来自动收集功能覆盖数据；若断言失败SVA会自动显示错误信息。

1.3、SystemVerilog 的调度

Systemverilog 语言被定义成一种基于事件的执行模式。
断言的评估和执行包括三个阶段：

• 预备（Preponed) ： 在这个阶段，采样断言变量，而且信号（net) 或 变量（variable） 的状态不能改变。确保在时隙开始的时候采样到最稳定的值。
• 观察（Observed）：该阶段对所有的属性表达式求值
• 响应（Reactive）：该阶段调度评估属性成功或失败的代码

1.4、SVA 术语

SystemVerilog 语言中定义了两种断言：并发断言 和 即时断言

1.4.1、并发断言

• 基于时钟周期
• 在时钟边缘，根据调用的变量的采样值计算测试表达式
• 变量的采样在预备阶段完成，而表达式的计算在调度器的观察阶段完成
• 可以被放到过程块(procedural block)、模块（module）、接口（interface），或者一个程序（program）的定义中
• 可以在静态（形式）验证 和 动态验证（模拟）工具中使用

示例：

// 在时钟沿，a和b 不能同时为高电平
a_cc: assertproperty(@ posedge clk) not (a&b));

属性的每一个时钟的上升沿都被检验，不论信号a 和 信号b 是否有值的变换

1.4.2、即时断言

• 基于模拟事件的语义
• 测试表达式的求值就像过程块中的其他 Verilog 的表达式一样。本质不是时序相关的，而是立即被求值
• 必须放在过程块的定义中
• 只能用于动态模拟
  示例：

always_comb
begin
	a_ia: assert ( a && b ) ;
end
/// 即时断言 a_ia 被写成一个过程块的一部分，遵循和信号a、b 相同的事件调度。
// 当信号a 和 信号b 发生变化时，always 块被执行。

对于即时断言，当断言的信号值发生变化时，always块（断言语句）被执行
区别即时断言 和 并发断言 的关键词：** " property" **

1.5、建立 SVA 块

任何设计模型中，功能总是由多个逻辑事件的组合来表示的。
SVA 用关键词** “ sequence”** 来表示这些事件。
==序列（sequence）==的基本语法：

sequence name_of_sequence;
	<test expression>;
endsequence

许多序列可以逻辑或有序地组合起来成更复杂的序列。SVA 提供了关键 “property” 来表示这些复杂的有序行为。
property 基本语法：

property name_of_property;
	<test expression>; or
	<complex seqeunce expressions>;
endproperty

属性：是在模拟过程中被验证的单元。它必须在模拟中被断言来发挥。SVA提供了关键词**“assert”** 来检查属性。
==断言（assert）==基本语法：

assertion_name: assert property ( property_name );

建立 SVA 检验器的步骤：
步骤1： 建立布尔表达式
↓
步骤2：建立序列表达式
↓
步骤3：建立属性
↓
步骤4：断言属性

1.6、一个简单的序列

// 检查信号 a 在每个时钟上升沿都是高电平
sequence s1;
	@(posedge clk) a;
endsequence

1.7、边沿定义的序列

序列s1 使用的是信号的逻辑值。
SVA 也内嵌了边缘表达式，方便用户检测信号值从一个时钟周期到另一个时钟周期的跳变。 —— 使得用户能够检查边沿敏感的信号。
三种有用的内嵌函数：

• $rose( boolean expression or signal_name)：当信号/表达式
• $fell( boolean expression or signal_name ) : 当信号/表达式的最低位变为0 时返回真
• $stabel ( boolean expression or signal_name) ：当表达式的值不发生变化时返回真

示例：

// 序列s2 检查信号 " a " 在每个时钟上升沿跳变为1
sequence s2;
	@(posedge clk) $rose( a );
endsequence

• 在时钟周期2之前，信号”a" 没有被赋值，因此断言值被认定为“x"。值从x到0 的转换不是上升沿，断言失败
• 时钟周期3，信号”a" 在序列中的采样值是1。值从0到1的上升沿转化，所以在时钟3断言成功
• 同理时钟周期9、时钟周期12 断言成功

1.8、逻辑关系的序列

示例：

// 序列s3 检查每一个时钟上升沿，信号“a" 或 信号 “ b" 是高电平
sequence s3;
	@(posedge clk) a || b;
endsequence

1.9、序列表达式

在序列定义中定义形参，相同的序列能够被重用到设计中具有相似行为的信号上。
示例：

// 定义
sequence s3_lib ( a, b );
a || b;
endsequence

// 通用的序列 s3_lib 能重用在任何两个信号上
sequence s3_lib_inst1;
	s3_lib ( req1,  req2 );
endsequence

一些在设计中常见的通用属性都可以被开发成一个库便于重用，如 one-hot 状态机检查，等效性检查等。

1.10、时序关系的序列

时序检查 ：检查的信号需要几个时钟周期才能完成事件
SVA 中，时钟周期延迟 用 ” ## “ 表示。如 ##3 表示3个时钟周期
示例：

// 序列s4：检查信号 " a “ 在 一个给定的时钟上升沿为高电平后，信号"b" 在两个时钟周期后为高电平
// 注意：序列以 信号"a" 在时钟上升沿为高电平开始
sequence s4;
	@(posedge clk) a ##2 b;
endsequence
 

注意：断言成功的序列总是标注在序列开始的位置