0 引言

    随着集成电路设计规模和复杂度增加，系统设计的功能验证面临着严峻挑战。据统计，验证的时间和人力投入已占到整个设计的50%以上，用于测试和错误诊断的代价超过了产品实现成本的50%。因此，推出一种新的验证方法成为验证界的热点和难点。

    传统的模拟验证方法，基于软件或硬件平台设计系统模型，通过对比测试向量的输出结果判断设计是否达到标准，这很大程度上取决于测试向量的完备性^[1]。面对大型设计时，模拟验证逐渐暴露其局限性，难以覆盖所有的测试向量，无法保证验证的完整性。

    形式化验证采用系统高效的方法，遍历整个状态空间，能够对设计进行完整的验证，近年来受到业界的广泛关注。形式验证包括等价性检验、性质检验和定理证明。等价性检验是指验证一个设计的不同描述形式之间的功能等价性。性质检验利用时态逻辑描述设计功能，通过穷举法验证设计的系统是否满足功能要求。定理证明从系统的公理出发，使用推理规则逐步推导出其所期望特性的证明过程，该方法对验证人员数学功底和推导能力要求很高，在学术研究之外应用较少。研究形式验证在实际项目中的应用，对于提高验证效率，缩短产品开发周期具有重要意义。

    本文基于一款处理器芯片的浮点运算单元，应用Cadence公司JasperGold形式验证工具，针对流水控制和计算单元中的关键模块分别采用了FPV和SEC进行验证。

1 SAR验证

    软件结构寄存器(Software Architected Register，SAR)在浮点运算单元流水线中作为第二级存储区域。SAR整体4个读端口和4个写端口，其内部由8个bank块组成，每个bank块的本质是SRAM，一个SRAM是一读一写，有128个entry，64个结构寄存器。SAR进行读/写操作时，会从8个bank中选择bank块的对应entry，将其中数据传输到其中一个读/写端口处。当出现多个读/写操作访问同一个bank块时，会发生冲突，需要报错。

    SAR的性质检验采用的是JasperGold的FPV。性质检验的主要工作是根据验证的需要编写对应的性质（property），性质的构建方式和完备程度会直接影响到验证的效果。常用编写property的语言有System Verilog和PSL（Property Specification Language)，JasperGold对这两种语言都支持。SAR主要的验证要点：(1)遍历整个读写的地址空间；(2)发生冲突时，能否报错；(3)检测在不同的工作模式下，是否能正常工作。

    在进行端对端数据传输时，数据包在数据通路中会经过缓冲器或存储器，需要进行数据传输完整性验证。因为存储器这类结构易于理解而且很少会出现bug，所以在整个项目的验证过程中不会引起大家的关注。但是因为存储器巨大的状态空间，使其成为提高形式化验证性能的瓶颈。为解决这一问题，在对SAR进行验证时，使用了JasperGold提供的形式计分板证明加速器（Formal Scoreboard Proof Accelerator，PA)。PA可以把存储器进行抽象化，同时保留充分的信息，确保Formal Scoreboard中结果的精确。在SAR具体验证时，用PA替换了SAR中的bank，同时为了简化验证复杂度，在构建属性断言时，核心思想是：在没有发生冲突的情况下，读操作读取的数据应该等于上一次写操作对应地址的写入数据。Check会对相对应写操作数据和读数据进行对比，同时检测冲突发生的情况，具体的验证构如图1所示。

    通过对验证结果分析，发现编写的property涵盖了所有的验证要点，且全部得到了证明。尤其是使用PA之后，证明消耗的时间大大缩短，验证性能提升显著。如图2和图3所示，没有使用PA前，针对SAR一个端口遍历所有读写地址空间，总的证明时间为286.41 s，使用PA之后，所需的证明时间仅为1.04 s。

2 ECC验证

    为了保持数据的正确性和一致性，浮点运算单元的流水线控制中引入了纠错码（Error Correcting Code，ECC）校验机制，实现对源操作数的错误检出和及时纠正，利用数据的ECC码可以实现“纠一检二”，即仅有1 bit数据出错时，能纠正该错误，当数据有2 bit错误时，只能检测出错误但不能恢复。

    ECC校验是利用数据初始的纠错码和读取该数据时重新生成的ECC码按位异或生成综合位，根据综合位判断数据是否出错，并将综合位输出供纠错使用。ECC恢复是依据ECC校验输出的纠错信息纠正待纠错数据，当数据出错位大于一位时，错误不可恢复。

    ECC校验和ECC恢复是流水线中不同执行阶段的两个模块，相互独立又相互依赖。当数据经过ECC校验模块且输出的error信号为高时，待纠错数据和纠错码被驱动给ECC恢复模块来判断数据是否可以恢复并纠错。若两个模块分别验证，复杂的纠错码产生机制和有依赖关系输入信号增加了验证难度。故将两个模块直接相连，通过对比输入数据与纠错后数据来验证模块功能。

    如图4所示，设计一个组合电路实现对输入数据的校验和纠错，接入一个错误数据生成模块和纠错码产生模块实现对ECC校验输入信号的产生，避免在输入信号property中描述复杂的纠错码产生机制。错误数据生成模块根据输入信号错误模式e指定注入错误的数量，错误0和错误1信号指定数据具体翻转位。将ECC校验、ECC恢复、ECC产生和错误产生模块封装为一个整体，作为性质检验的设计实现。

    对于组合后的ECC模块，针对不同的数据出错类型，有3类property需检验。在数据没有出错的情况下，输出信号error为0；数据有1 bit出错时，输出error为1，数据不可恢复为0且纠错后数据与输入数据相等；数据有2 bit错误时，输出error为1且数据不可恢复信号为1。根据错误位产生的逻辑，当需要产生2 bit错误时，需要保证两次的翻转位不同，即错误0!=错误1。实际的流水线逻辑中数据位宽为128 bit，对数据的高64 bit和低64 bit分别描述其property验证。

    JasperGold会遍历所有的状态空间，验证结果显示耗时101 s，证明了设计包含描述的所有属性，说明ECC校验模块“检二”和ECC恢复模块“纠一”的功能实现。

3 共用模块的等价性检验

    浮点单元的运算模块非常适合形式化验证，尤其是等价性检验。进行等价性检验主要的工作在于开发一个符合设计规格的参考模型，参考模型可以根据需要灵活的应用不同语言编写。目前业界主流的形式化验证工具只支持Verilog HDL和VHDL，RTL到RTL的等价性检验已经发展比较成熟，有着相对完善的标准。本文采用的JasperGold支持Verilog HDL和VHDL这两种语言，也有一些工具支持C语言，但C到RTL的等价性检验应用较少，发展不是很成熟。

    在浮点单元运算IP设计开发时，先对多个运算IP中共用的基本模块进行了统一设计，在之后各个IP设计中对共用模块进行统一调用。所以，浮点单元运算IP的验证工作先是对共用模块进行验证，然后是对各个IP的验证。出于项目实际情况考虑，在对共用模块进行验证时，因为共用模块实现的功能相对单一，复杂度不高，所以共用模块的参考模型使用Verilog HDL编写。而对运算IP验证的时候，因为IP复杂度高，开发相应参考模型的工作量很大，因此形式化验证和仿真验证共用了统一由C语言开发的参考模型。由于JasperGold不支持C到RTL的等价性检验，在对IP验证的时候使用了其它的验证平台。

    共用模块的等价性检验采用的是JasperGold的SEC,主要包括加法器、减法器、循环移位器、前导零、4-2压缩器、舍入器（rounder）等模块。在编写参考模型时，除了保证其可综合之外，还需要考虑功能的正确。

    图5给出了rounder的形式验证报告，可以看出，相比于仿真验证，证明时间几乎为0，验证速度明显提高。而且这一优势在对整个IP进行验证时更加突出，对浮点单元各个运算IP进行等价性验证时，除了乘加模块需要对参考模型进行特殊的改动^[3]，其它模块包括除法、倒数估值等模块，都能够比较快速地收敛，极大地缩减验证周期。

4 总结

    本文主要介绍了形式化验证方法在浮点单元功能验证中的具体应用。结果表明，相比模拟仿真验证，形式化验证不用构造复杂的验证平台和编写海量的测试激励，在极大减少验证工作量的同时，提高了的可靠性，缩短了验证周期。

参考文献

[1] LAM W.Hardware design verification：simulation and formal method-based approaches[M].US：Prentice Hall PTR，2005.

[2] 陈云霁，马麟，沈海华，等.龙芯2号微处理器浮点除法功能部件的形式验证[J].计算机研究与发展，2006(10)：1835-1841.

[3] JACOBI C，KAI W，PARUTHI V，et al.2005 Design，Automation and Test in Europe Conference and Exposition (DATE 2005)[C].Munich，2005.

作者信息:

朱  峰，鲁征浩，朱  青

（苏州大学，江苏 苏州215006）