基于断言的验证方法在总线协议验证中的应用

摘 要： 随着ASIC和SoC设计复杂程度的不断提高，功能验证越来越受到重视。作为新兴的验证方法，基于断言的验证得到越来越广泛的应用。本文介绍了基于断言的验证方法及其应用于功能验证的诸多优点，总结了断言验证在总线协议验证中的应用方法，并采用PSL语言举例进行了说明。
关键词：SoC；总线验证；断言；基于断言的验证；PSL

引言
随着芯片复杂程度的增加，保证芯片功能的正确性成为SoC和ASIC设计中的最大的挑战。芯片的验证要花费越来越多的时间，同时也出现了许多新的验证方法和理论，如基于断言的验证、覆盖率导向的验证、可约束的随机激励、事务级验证等。其中，基于断言的验证(Assertion Based Verification: ABV)是硬件设计功能验证的一种有效方法。
作为一种对设计对象的属性或行为特性的描述，断言并不是新的概念。随着硬件描述语言应用于硬件设计，断言的方法也被引入设计验证当中。VHDL语言中的关键字assert使设计者可以在代码中方便地加入断言；各种新的验证语言，如Vera、e、PSL以及SystemVerilog对断言也都有更好的支持。另外，各种仿真工具对断言的支持，尤其是断言在形式验证中的应用，使基于断言的验证方法在设计验证中发挥了越来越重要的作用。

对于硬件的断言和
基于断言的验证
断言是对设计意图进行的一种陈述，它必须经过验证。基于断言的验证是把断言加入设计以增加设计可见性的验证技术。每个硬件设计都会包含一些设计对象的特性，这些特性保证了硬件能够正常工作。断言就是用于对这些硬件系统的特性进行描述，即说明硬件的某些行为必须发生或从不发生。
断言可以描述组合逻辑特性，也可以描述时序逻辑特性。断言可以嵌入在源代码中，也可以在单独的文件中加入。断言的检查可以通过动态仿真的方法进行，也可以通过静态形式验证的方法进行。

图1 事务检查仿真波形图

基于断言的验证适用于“白盒”、“黑盒”、“灰盒”三种验证方法。在白盒设计中，断言嵌入在代码中，一般由设计工程师在编写代码时加入。它可以在验证中更早地发现错误，而且可以在更接近于出错点的地方发现错误，以节省调试时间。 黑盒的验证方法只在模块的边界进行观测，所以错误只有在传递到输出信号的时候才能够被检测到。应用于黑盒验证时，断言通常用于描述接口特性，如总线协议，一般由验证工程师编写在单独的断言描述文件中。而灰盒是介于黑盒和白盒之间的验证方法，包含了一定的设计实现特性。
基于断言的验证给传统的验证方法注入了新鲜的血液，极大提高了验证效率，它的优点主要体现在以下六个方面。
(1)提高了设计可见性(observa bility)：嵌入在代码中的断言使得观测点更加接近错误发生的地方，从而提高了可见性。
(2)节省了调试时间：因为基于断言的验证提高了设计可见性，所以验证工程师可以在较为准确的位置及早发现错误。
(3)简化了可重用IP核的验证：IP核在被使用之前都要经过验证，应用断言验证IP核与系统的接口，可以提高验证效率。
(4)功能覆盖率的记录更加方便：由于在仿真过程中可以记录断言覆盖率，所以对断言覆盖率的检查成为功能覆盖率的一种形式。
(5)方便了形式验证：断言可以用来描述属性，这使得断言在形式验证中得到了广泛的应用。
(6)可以用作记录文档的语言：用断言描述设计说明，不仅准确，而且还具有可执行的特点，这样就可以直接在仿真或是形式验证中使用，节省了验证时间。

图2 时序合法性检查仿真波形图

基于断言的验证方法在
总线协议验证中的应用
SoC设计中使用了大量的IP核，要把IP整合到整个系统中，需要通过各种系统接口。对于简单模块的连接，可以通过自己定义的接口实现。而成熟的IP通常都兼容若干种总线协议，这样应用IP时只要把它连接到标准的总线上就可以了。AMBA、WishBone都是目前比较常用的总线协议。
断言特别适合描述时序特性和因果特性，这也使得断言验证特别容易应用到总线协议的验证过程中。在接口处加入断言可以极大地方便总线规则的检查。许多针对总线的验证IP，如Synopsys DesignWare中的AMBA3 AXI、AMBA2.0、USB2.0等，里面也大量用到了断言。但是，大多数的验证IP都是收费的，会增加设计成本。而且如果用户对已有的总线协议进行了修改，那么就不能在验证中直接使用验证IP。这时，应用基于断言的验证方法就可以大大提高验证效率。
本文在举例时用到的断言语言是Accellera的PSL(Property Specification Language)语言。PSL建立在IBM公司Sugar语言的基础上，由于它具有简洁的语法，非常有利于读写，能表达大量的设计功能行为，而且很多现有的仿真工具和形式验证工具都已经支持PSL，因此PSL作为功能描述语言得到了广泛的应用。文中的仿真工具采用Cadence的IUS(Incisive Unified Simulator)，因为它对Verilog和PSL都有很好的支持。

图3 信号回送检查仿真波形图

不定态检查
输入信号未连接以及内部信号错误的连接会在RTL模型中产生不定态信号x，这种信号会传递到总线上，所以应该对总线中的不定态信号进行检查，如地址线和数据线不能出现不定态x，握手信号和控制信号不能出现x和z。设要检查SysAD信号的所有63位不能出现不定态，加入PSL断言为：
property X_Detection = never ((^SysAD[63:0] === 1'bx) && reset_n) @(posedge clk);
assert X_Detection;
有效范围检查
信号在定义功能时会规定某些值时无效，所以应该对总线进行信号有效范围的检查。比如有一部分地址是系统保留地址或是有特殊用途，如果出现这些地址就需被视为非法。下例的PSL断言是使地址线Addr不会出现大于16进制数e0000000的地址。
property Valid_Range = never ((Addr[31:0] >= 32'he0000000) && reset_n) @(posedge clk);
assert Valid_Range;
信号组合有效性检查
RTL模型中要通过控制信号传递信息，但是多个控制信号的组合是受到限制的，所以要在总线接口处对控制信号的组合有效性进行检查。比如读使能和写使能不能同时有效，以下就是读信号read和写信号write不能同时有效的PSL断言。
property Valid_Combination = never (({read,write}==2'b11) && reset_n) @(posedge clk);
assert Valid_Combination;
复位中的信号检查
系统复位后，要求某些控制信号和数据信号有确定的状态，这样可以保证系统不进入死锁，所以应该在总线接口处加入复位后的信号检查。下面的断言用于描述复位后读控制信号read和写控制信号write都为0：
property Reset_Check = always ({!reset_n;reset_n}|->{(!read&&!write)}) @(posedge clk);
assert Reset_Check;
事务检查
总线协议中的各种事务，比如读操作和写操作，在不同的协议中有不同的描述。对于协议中的各种事务，应该加入断言，用来检查时序，并进行功能覆盖率的分析。下面是用PSL语言描述的MIPS系统接口总线协议的单数据读操作：
property Read_Transaction = always {(!RdRdy && reset_n &&!
ValidOut&&SysCmd[8]==1'b0 && SysCmd[7:5]==3'b000)}
->{[*0:4];(!Releas);[*0:2];
(SysCmd[8]==1'b1&&!ValidIn)}
@(posedge clk);
cover Read_Transaction;
仿真波形图如图1所示。这里在验证层用的关键词是cover，表示用来进行覆盖率的分析。
时序合法性检查
各种总线协议不仅会对信号的组合进行约束，也会对信号出现顺序的合法性进行限制。例如，外设的响应信号不能在主机发出请求之前出现。所以，对时序合法性进行检查是必须的。下面的断言描述在接收到grant信号后开始数据传输操作：
property Sequence_Check = always ({{req[*1:4]}:{grant}; req} |-> {start}) @ (posedge clk);
assert Sequence_Check;
仿真波形图如图2所示。
信号回送检查
多数总线协议中需要主机发送请求，在获得响应后才能进行操作。如果得不到外设的响应，就会进入死锁状态，导致系统停止运行，所以应该加入断言来检查这种情况是否发生。下例是表示在req信号发出后5个周期内必须收到总线仲裁控制信号grant。
property Response_Check = always {!req;req} |-> {{[*1:5]}:{grant}} @ (posedge clk);
assert Response_Check;
仿真波形图如图3所示。

结语
本文介绍了硬件断言和基于断言的验证方法，并说明了断言应用于芯片设计验证的诸多好处。断言验证已经应用于实际的设计和验证当中，而断言比较容易被应用于总线协议验证过程中。本文总结了对于总线协议应用断言验证的一些方法，这些方法对验证实践有一定的指导作用。本文应用PSL语言对这些方法举例进行说明，而且通过工具进行了仿真。这说明基于断言的验证方法作为一种新的验证方法，可以作为整个验证过程中的一环，提高设计和验证的效率。■

参考文献：
1 Harry Foster, A. Krolnik, D. Lacey. Assertion-Based Design (Second Edition)[c]. Kluwer Academic Publishers, New York, 2004
2 Ben Cohen, S. Venkataramanan, A. Kumari. Using PSL/Sugar for Formal and Dynamic Verification (Second Edition)[c]. VhdlCohen, Los Angeles, California, 2004