SystemVerilog 断言及其应用--(神州龙芯集成)

[摘要]：在介绍SystemVerilog 断言的概念、使用断言的好处、断言的分类、断言的组成以
及断言如何被插入到被测设计（DUT）的基础上，本文详细地介绍了如何使用不同的断言语句
对信号之间的复杂时序关系进行严格的检查，并针对每个例子展示了在ModelSim 6.1b 仿真
环境中所显示的波形。本文旨在帮助读者理解如何使用断言对设计中信号间复杂时序关系进
行验证的方法，并由此介绍一些基本的SystemVerilog 断言、操作符、代码段和断言验证方
法学。
关键字：SystemVerilog，断言, DUT, SVA，Assertion
1． 前言
当今，数字电路的规模和复杂度在不断增长，这使得对设计进行彻底的验证将成为一项巨大
的挑战。在整个芯片设计过程中，验证工作所需的时间将占去设计周期的70％～80％，验证
工程师的人数将是设计工程师的两倍。这就迫切需要提高验证工作的效率，以解决验证瓶颈
问题。
传统上，对被测设计（DUT）的验证都是通过在DUT 的输入端口加上具有特定时序激励，然后
观察DUT 的内部状态变化和最后的输出信号，以确定DUT 工作是否正确。这种方法对简单的
小规模的设计很有用。但当设计规模变大时，要想使用这种方法来验证DUT 是不现实的。因
为对于规模大的设计，要想遍历设计将遇到的各种情况，验证其正确性，需要成千上万的特
定时序激励。并且如果设计稍有一点变动，这些时序激励就得重新编写。设计的复杂性迫使
验证工程师使用随机测试平台来生成更多的验证激励。高级验证语言，如OVA，PSL 等，便在
创建复杂测试平台时得到了广泛的应用。但这些验证语言和RTL 级的编码语言不一致，使得
验证很容易出现错误，造成调试工作的不方便。
SystemVerilog 的出现可以解决这些问题。 SystemVerilog 是在Verilog 语言的基础上发展
而来的，用SystemVerilog 语言可以很容易地生成复杂的随机测试激励，并能方便地编写断
言和测试代码覆盖率的代码

由此可见，用SystemVerilog 描述的断言可以应用于设计过程的各个阶段，它不仅能快而准
确地定位设计中的错误，还能统计功能覆盖率。用SystemVerilog 描述的断言能显著提高验
证准确性和验证效率，加快设计进程，提高我们对设计的信心

2． SVA 概述
SystemVerilog 语言是Verilog 语言的增强，它增强了Verilog 原有的编程能力，又引入了新
的数据类型和验证方法。SystemVerilog 断言（以下简称SVA）就属于这些新的验证方法中的
一种。
那么什么是断言呢？断言就是对设计属性（行为）的描述，它是用描述性语言来描述设计的
属性。在仿真过程中，如果一个被描述的属性不是我们期望的那样，那么断言就会失败；或
者在仿真过程中，如果出现了一个不应该出现的属性，那么断言也会失败。
那么为什么要使用断言呢？原有的Verilog 语言是一种过程性语言，设计它的目的是用于硬
件描述，不是用于仿真验证，因此它不能很好地控制时序。要描述复杂的时序关系，Verilog
语言需要编写冗长的代码，很容易出错，且不易维护。SVA 是一种描述性语言，可以完美地描
述和控制时序相关的问题，而且语言本身简洁易读，容易维护。SVA 还提供了许多内嵌的函数
用于测试特定的时序关系和自动收集功能覆盖率数据。并且当断言失败时，仿真系统会根据
失败断言的严重程度来决定是打印一条错误提示信息还是退出仿真过程，便于定位出错的位
置。
比如要验证这样一个属性：“当信号a 在某一个时钟周期为高电平时，那么在接下来的2～4
个时钟周期内，信号b 应该为高电平”。用Verilog 语言描述这样一个属性需要一大段代码，
而用SVA 描述就只需要几行代码。下面的代码为SVA。
例1：
property a2b_p;
@(posedge sclk) $rose(a) |-> [2:4] $rose(b);
endproperty
a2b_a: assert property(a2b_p);
a2b_c: cover property(a2b_p);
property 和endproperty 为SVA 的关键字，用于描述属性。a2b_p 为属性的名字。$rose 为
SVA 的内嵌函数，用于检查信号的上升沿。assert property 也为SVA 的关键字，表示并发断
言。a2b_a 为断言的名字，它把属性a2b_p 作为参数。a2b_c 为覆盖语句，它用于记录断言的
成功。下图为本断言在ModelSim 6.1b 环境中的仿真波形和断言出错信息。

断言信号为高阻态表示断言没有被激活，断言信号为1 表示断言被激活，正在检查时序属性。
倒三角表示断言在此刻失败，正三角表示断言在此刻成功。从上图可以看出，断言a2b_a 一
共进行了3 次时序检查，第1、3 次失败，第2 次成功。
第1 次断言失败。在sclk(2)处，信号a 被拉高，但这时采到的a 的值仍为0。在sclk(3)处，
信号a 被拉低，但这时采到的a 的值为1，而前一个时钟采到a 的值为0，表示a 的上升沿到
来，即$rose(a)成立，整个断言被激活，然后进行后序时序检查。在接下来的2～4 个时钟周
期，并没有采样到信号b 的上升沿，则在sclk(7)处断言被标记为失败，断言退出激活状态。
第2 次断言成功。在sclk(9)处，采样到信号a 的上升沿，断言被激活。在随后的第3 个时钟
周期又采样到信号b 的上升沿，断言成功，随即断言退出激活状态。
第3 次断言失败，其断言检测过程和第1、2 次类似，请读者自己分析。
由此我们可以看出SVA 在时序检查时的巨大优势：只需几句代码就可以检查一类时序问题。
而且在检查时，仿真验证系统不仅会打印出错信息，还会在波形中进行标记。这对于我们检
查信号间的时序关系非常方便。

3． SVA 分类及组成
3.1 断言分类
SVA 分为并发断言和即时断言。
并发断言的计算基于时钟周期，在时钟边沿根据变量的采样值计算表达式。它可以放在过程
块（procedural block）、模块（module）、接口（interface）或一个程序块（program）的
定义中。并发断言可以在静态（形式化）验证工具和动态（仿真）验证工具中使用。上面的
例子就是并发断言。
即时断言基于事件的变化，表达式的计算就像Verilog 中的组合逻辑赋值一样，是立即被求
值的，而不是时序相关的。它必须放在过程块的定义中，只能用于动态仿真。一个即时断言
的例子如下：
4
例2：
always_comb
immi_a: assert (a && b);
即时断言被当作过程块的一部分。当信号a 或者信号b 发生变化时，always_c
9d80
omb 块被执行。
区别即时断言和并发断言的关键词是“property”。我们在进行时序检查时，通常使用并发断
言，而很少使用即时断言。
3.2 断言的组成和建立过程
任何复杂的时序模型，其功能总是由多个逻辑事件的组合来表示的。这些事件可以是简单的
同一时钟沿被求值的布尔表达式，也可以是经过几个时钟周期求值计算得到的事件。SVA 使用
关键字sequence（序列）来表示这些事件。许多序列可以被有序地组合起来形成设计的属性，
SVA 用关键字property 来表示属性。最后属性要在断言中被调用才能真正发挥作用。同时我
们还应该用覆盖语句来记录断言成功的次数。由此可以看出断言的建立过程为“编写布尔表
达式 —> 编写序列（sequence）－> 编写属性（property）—> 编写断言（assert property）
和覆盖语句（cover property）”。它们的语法格式为：
序列 属性 断言和覆盖
sequence name_s;
<test expression>;
endsequence
property name_p;
<test expression>; or
<complex sequence expressions>;
endproperty
name_a:assert property
(property name);
name_c:cover property
(property name);
表1 序列、属性、断言语法格式
注意：上表中斜体字为名字。为了方便识别，序列以_s 结尾，属性以_p 结尾，断言以_a 结尾，
覆盖语句以_c 结尾。

参考文献：
【1】《SystemVerilog 验证方法学》，夏宇闻，杨雷，陈先勇，徐伟俊，杨鑫 译，北京航空航
天大学出版社，ISBN:978-7-81124-079-5。
【2】《Verilog 数字系统设计教程》，夏宇闻 编著，北军航空航天大学，ISBN:7-81077-302-X。
【3 】《SystemVerilog 应用手册》， 陈俊杰 等译， 清华大学出版社， ISBN ：
7-302-13441-3/TP.8442。
【4】SystemVerilog 语法手册，《IEEE Standard for SystemVerilog－Unified Hardware
Design,Specification,and Verification Language》。
【5】《SYSTEMVERILOG FOR VERIFICATION》,CHRIS SPEAR,Synopsys,Inc.