学霸笔记-验证断言（立即断言&并行断言）

1.何为断言

断言主要用来检查仿真过程中存在的时序问题，如果存在异常情况，断言会报警。一般在数字电路设计中都要加入断言，断言占整个设计的比例应不少于30%。

2.断言的作用：

使用断言可以缩短研制周期；

使用断言可以使设计中存在的各种问题更容易被动态监测观察；

使用断言内嵌的覆盖率统计功能（cover）可以更加容易的获得对于功能的覆盖性；

断言的可读性较一般描述语言更容易理解；

通过全局控制实现设计中断言的开关；

断言可以加速形式验证，提高形式验证的效率；

3.断言的种类

断言分为立即断言和并行断言；

3.1立即断言

立即断言主要用来检查当前仿真时间的条件，可以理解为if...else，放在过程块中使用。

语法：

labels：assert（expression）action_block;

action_block 操作块在断言表达式的求值之后立即执行

操作块指定在断言成功或失败时采取什么操作

action_block: pass_statement; else fail_statement;

例子：

assert(expression) $display("expression evaluates to true");

else $fatal("expression evaluates to false");

断言失败默认严重程度为error，error达到一定数量仿真会退出；

立即断言构建思路：

3.2并发断言

并发断言检 查跨越多个时钟周期的事件序列 。

可以认为并发断言是一个连续运行的模块，为整个仿真过程检查信号，所以需要在并发断言内指定一个采样时钟。

并发断言仅在有时钟周期的情况下出现

测试表达式是基于所涉及变量的采样值在时钟边缘进行计算的

可以在过程块、module、interface和program块内定义并发断言

区别并发断言和立即断言的关键字是property

格式：

断言名： assert property (判断条件)

例子：

check_a_and_b:assert property (@(posedge clk) (a&&b))

$display("a&&b is true");

else

$error ("a&&b is false")；

4.断言层次结构

SVA中可以存在内建的单元，这些单元可以是以下的几种：

• Boolean expressions 布尔表达式

布尔表达式是组成断言的最小单元，断言可以由多个逻辑事件组成，这些逻辑事件可以是简单的布尔表达式.在SVA中，信号或事件可以使用常用的操作符，如：&&, ||, !, ^，& 等；

• Sequence序列

sequence是布尔表达式更高一层的单元，一个sequence中可以包含若干个布尔表达式，同时在sequence中可以使用一些新的操作符，如 ## 、重复操作符、序列操作符

• Property 属性

property是比sequence更高一层的单元，也是构成断言最常用的模块，其中最重要的性质是可以在property中使用蕴含操作符(|-> |=>)；

4.1 sequence 序列

在任何设计中，功能总是由多个逻辑事件的组合来表示，这些事件可以是简单的同一个时钟沿被求值的布尔表达式，也可以是经过几个时钟周期的求值事件，SVA用关键字sequence来表示这些事件，sequence可以让断言易读，复用性高；

sequence具有如下特性：

• 可带参数；

• 可以在 property 中调用；

• 可以使用局部变量；

• 可以定义时钟周期；

sequence的定义格式如下：

sequence name_of_sequence(参数);

……

endsequence

以下代码分别通过property，sequence+property实现对a&&b仿真时间的判断：

sequence 序列可以带参数：

用法： 

sequence 序列可以有时序

带时序关系的sequence ：在SVA中时钟延时用符号"##"来表示，如"##2"表示延时两个时钟周期；

例如：

sequence会 在时钟上升沿到来后首先检查 a 是否为 1，当a为1时，两个时钟周期后继续检查b是否为1，当b为1时，断言pass ；

sequence 序列可以内嵌

4.2 property 序列 

property是比sequence更高一层的单元，也是构成断言最常用的模块，其中最重要的性质是可以在

property中使用 蕴含(overlapped)操作符(|-> |=>)；

并行断言构建思路： 

5.sequence和property的异同

除了以上的区别外，立即断言和并发断言的采样时间是否相同也是验证过程中需要注意的问题，以下的代码进行演示：

波形展示：

 以上代码对a&&b分别进行了immediate和concurrent assertions,波形显示两种断言结果完全相同，都在时钟上升沿前进行采样。

6.补充知识点（assert/cover/assume）

assert：

cover：

assume:

注：优秀验证学员随堂笔记，已经征求到学生的同意，会持续给牛友们分享！

大家看完记得 一键三连！多多支持