kaiyun官方注册
您所在的位置: 首页> 嵌入式技术> 设计应用> 形式化验证在处理器浮点运算单元中的应用
形式化验证在处理器浮点运算单元中的应用
2017年电子技术应用第2期
朱 峰,鲁征浩,朱 青
苏州大学,江苏 苏州215006
摘要:随着芯片复杂度的急剧增加,模拟仿真验证不能保证测试向量的完备性,尤其是一些边界情况。形式验证方法因其完整的状态空间遍历性和良好的完备性,被业界应用于设计规模不大的模块和子单元中。针对处理器浮点运算单元,采用Cadence公司JasperGold工具对一些关键模块进行了形式化验证,对流水控制中的纠错码(Error Correcting Code,ECC)、软件结构寄存器(Software Architected Register,SAR)和计算单元中的公共模块分别采用了基于FPV(Formal Property Verification)的性质检验和基于SEC(Sequential Equivalence Checking)的等价性检验。结果表明,形式化验证在保证设计正确性的基础上极大地缩短了验证周期。
中图分类号:TN401;TP301
文献标识码:A
DOI:10.16157/j.issn.0258-7998.2017.02.005
中文引用格式:朱峰,鲁征浩,朱青. 形式化验证在处理器浮点运算单元中的应用[J].电子技术应用,2017,43(2):29-32.
英文引用格式:Zhu Feng,Lu Zhenghao,Zhu Qing. Effective formal applications in CPU floating point unit[J].Application of Electronic Technique,2017,43(2):29-32.
Effective formal applications in CPU floating point unit
Zhu Feng,Lu Zhenghao,Zhu Qing
Soochow University,Suzhou 215006,China
Abstract:With the increasing complexity of chip design, it is almost impossible to ensure the completeness of test space, especially corner cases. Formal verification is applied to block and subunit level design in industry due to systematic and efficient way to explore exhaustively all reachable state space. This paper describes our practical experiences and results with applying formal verification to floating point unit using Cadence JasperGold. Specially, FPV(Formal Property Verification) and SEC(Sequential Equivalence Checking) are applied to ECC(Error Correcting Code) as well as SAR(Software Architecture Register) in pipeline control and shared arithmetic modules respectively. The implemented results show that JasperGold improves verification quality with exposing corner cases, locates potential bugs accurately and speeds up verification achievement.
Key words :floating point unit;formal verification;JasperGold;FPV;SEC

0 引言

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

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

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

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

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所示。

wdz3-t1.gif

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

wdz3-t2.gifwdz3-t3.gif

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产生和错误产生模块封装为一个整体,作为性质检验的设计实现。

wdz3-t4.gif

对于组合后的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],其它模块包括除法、倒数估值等模块,都能够比较快速地收敛,极大地缩减验证周期。

wdz3-t5.gif

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)

此内容为AET网站原创,未经授权禁止转载。
Baidu
map