引言

传统的RTL级验证方法主要是仿真和形式验证(等价性检查)。对仿真来说,在设计早期出现的功能错误,往往在整个仿真结束后才能发现。而且,随着芯片的规模越来越大,在输出出现错误时,需要耗费大量的调试时间来判断到底是哪个环节出现了问题。虽然现在大多数仿真工具都支持代码覆盖率检查,但即使是达到100%的代码覆盖率,也不能保证100%的功能覆盖率。形式验证中的等价性检查需要一个用于比较的原型,也有一定的局限性。因此,在设计芯片时,需要更高效的验证方法。

图1 设计中断言的分类

图2 基于断言的仿真流程

图3 采用PSL进行形式验证的流程

ABV

断言可以描述设计的输入、输出等功能行为。用一种语言来描述设计的功能行为,然后将此断言嵌在设计(RTL代码)中,或放在一个单独的外部文件中,在仿真或形式验证的过程中,断言将被仿真工具或形式验证工具检查,设计者就能够知道设计是否满足所描述的功能行为。这种验证方法就是ABV (Assertion-Based Verification,基于断言的验证)。ABV有如下几个显著的特点：能够提高对设计的可控性和可观察性;可以实现很高的功能覆盖率验证;通过检查断言可以确定IP是否被正确地集成入设计中。

根据设计中断言所描述的功能行为的不同,可以将其分为3种：应用断言(Application Assertion)、接口断言(Interface Assertion)和结构断言(Structural Assertion)。如图1所示,应用断言主要描述整个设计总的功能行为,如发送一个字节后必须有一个应答信号;接口断言主要描述模块间的通信协议、控制信号的传递等;结构断言主要描述低层次模块内部的属性,如FIFO中的溢出等。

PSL

由于用Verilog/VHDL描述设计的功能行为有很大的局限性,因此本文采用特定的功能描述语言,Accellera的PSL(Property Specification Language)。PSL建立在IBM公司Sugar语言的基础上,由于它具有简洁的语法,非常有利于读写,能表达大量的设计功能行为,而且得到了仿真工具和形式验证工具很好的支持,因此,PSL作为功能描述语言得到了广泛的应用。

基于PSL的断言

PSL主要有两种风格,采用Verilog和VHDL时,PSL的使用方法和语言结构都有所不同,本文中只介绍Verilog格式。

PSL包括4个层：布尔逻辑层(Boolean Layer)、时序层(Temporal Layer)、验证层(Verification Layer)和模型层(Modeling Layer)。其中前3个是主要层,模型层用于构建外围模块,基本不会使用。

PSL用property来描述设计的功能行为,property可以基于时钟,也可以不基于时钟。对于同步设计,建议采用一个默认时钟。

PSL的用法

PSL的使用主要有以下两种方法：

1)．将用PSL写的断言嵌入在设计中。这种方法是用关键字PSL作为注释嵌在RTL代码里面,仿真或形式验证工具会自动识别这些语句并执行。

module IO(clk,…);

…

… // HDL 代码

// default clock=posedge(clk); 指定检查Assertion所采用的时钟沿

// psl property HANDSHAKE=a lways{bus_request}=>{[*0:0];grant [*2];[*0:31]};

// psl assert HANDSHAKE;

endmodule

2)．将用PSL写的断言包含在单独的外部文件中。这种方法是建立在vunit基础上的,仿真或形式验证工具会将此外部文件和RTL一起执行。

vunit V1 (verilog_module_name)

{

defaut clock=posedge(clk);

property A1=never(a&b);

assert A1;

}

基于断言的仿真

目前大多数的仿真工具都支持PSL,它们能执行嵌在RTL设计中或单独在一个外部文件中的断言。基于断言的仿真能及时、迅速地发现错误,并能实现基于功能覆盖率的验证,提高了验证的充分性。

基于断言的仿真流程如图2所示,设计者首先要用PSL语言来描述需要检查的功能行为,在进行仿真时,仿真器会把设计和断言一同进行编译,如果设计不满足断言所描述的属性,仿真器将通过波形来指示断言的仿真失败。这样,设计者将很清楚是哪个属性不满足设计要求,就能够进行针对性的修改,验证效率得到了极大的提高。

除了能及时发现设计中存在的错误,基于断言的仿真还能对设计进行基于功能覆盖率的验证。设计者可以用PSL语言对设计的全部功能行为进行描述,在仿真过程中检查这些断言,这样可以提高设计验证的充分性,克服基于代码覆盖率的仿真所存在的弊端。

基于断言的形式验证

仿真是基于测试平台的,而测试向量有一定的覆盖率,不可能穷举所有的情况,因此仿真很容易忽略一些边缘情况,这时就需要形式验证。目前广泛使用的形式验证是模型检查,它的输入是RTL设计和基于断言的功能行为。形式验证工具将设计转换为一个很大的状态空间,然后通过检查断言是否在这个状态空间内,来判断设计是否满足用断言描述的功能行为。

以前,不同的形式验证工具都有自己的行为描述语言,没有共同标准;现在,PSL成为行为描述语言的标准,极大地提高了形式验证的效率。设计中使用PSL进行基于断言的形式验证的流程如图3所示。

在实际设计中,建议在设计小规模模块时采用模型检查,这样可以节省搭建测试平台所需的大量时间,提高验证效率;而在设计大的模块或整体验证的时候,建议采用基于断言的仿真。

结语

本文介绍了目前芯片设计领域最高效的基于断言的验证方法,这种验证方法已被国外的许多大公司所采用,国内的设计领域刚刚接触到这种方法,还没有实际运用到设计中。随着EDA工具对断言验证越来越好的支持,相信基于断言的验证方法将会被广泛的采用。