《電子技術(shù)應(yīng)用》
您所在的位置:首頁 > 嵌入式技術(shù) > 設(shè)計(jì)應(yīng)用 > 形式化驗(yàn)證在處理器浮點(diǎn)運(yùn)算單元中的應(yīng)用
形式化驗(yàn)證在處理器浮點(diǎn)運(yùn)算單元中的應(yīng)用
2017年電子技術(shù)應(yīng)用第2期
朱 峰,魯征浩,朱 青
蘇州大學(xué),江蘇 蘇州215006
摘要: 隨著芯片復(fù)雜度的急劇增加,模擬仿真驗(yàn)證不能保證測試向量的完備性,尤其是一些邊界情況。形式驗(yàn)證方法因其完整的狀態(tài)空間遍歷性和良好的完備性,被業(yè)界應(yīng)用于設(shè)計(jì)規(guī)模不大的模塊和子單元中。針對處理器浮點(diǎn)運(yùn)算單元,采用Cadence公司JasperGold工具對一些關(guān)鍵模塊進(jìn)行了形式化驗(yàn)證,對流水控制中的糾錯碼(Error Correcting Code,ECC)、軟件結(jié)構(gòu)寄存器(Software Architected Register,SAR)和計(jì)算單元中的公共模塊分別采用了基于FPV(Formal Property Verification)的性質(zhì)檢驗(yàn)和基于SEC(Sequential Equivalence Checking)的等價性檢驗(yàn)。結(jié)果表明,形式化驗(yàn)證在保證設(shè)計(jì)正確性的基礎(chǔ)上極大地縮短了驗(yàn)證周期。
中圖分類號: TN401;TP301
文獻(xiàn)標(biāo)識碼: A
DOI:10.16157/j.issn.0258-7998.2017.02.005
中文引用格式: 朱峰,魯征浩,朱青. 形式化驗(yàn)證在處理器浮點(diǎn)運(yùn)算單元中的應(yīng)用[J].電子技術(shù)應(yīng)用,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 引言

    隨著集成電路設(shè)計(jì)規(guī)模和復(fù)雜度增加,系統(tǒng)設(shè)計(jì)的功能驗(yàn)證面臨著嚴(yán)峻挑戰(zhàn)。據(jù)統(tǒng)計(jì),驗(yàn)證的時間和人力投入已占到整個設(shè)計(jì)的50%以上,用于測試和錯誤診斷的代價超過了產(chǎn)品實(shí)現(xiàn)成本的50%。因此,推出一種新的驗(yàn)證方法成為驗(yàn)證界的熱點(diǎn)和難點(diǎn)。

    傳統(tǒng)的模擬驗(yàn)證方法,基于軟件或硬件平臺設(shè)計(jì)系統(tǒng)模型,通過對比測試向量的輸出結(jié)果判斷設(shè)計(jì)是否達(dá)到標(biāo)準(zhǔn),這很大程度上取決于測試向量的完備性[1]。面對大型設(shè)計(jì)時,模擬驗(yàn)證逐漸暴露其局限性,難以覆蓋所有的測試向量,無法保證驗(yàn)證的完整性。

    形式化驗(yàn)證采用系統(tǒng)高效的方法,遍歷整個狀態(tài)空間,能夠?qū)υO(shè)計(jì)進(jìn)行完整的驗(yàn)證,近年來受到業(yè)界的廣泛關(guān)注。形式驗(yàn)證包括等價性檢驗(yàn)、性質(zhì)檢驗(yàn)和定理證明。等價性檢驗(yàn)是指驗(yàn)證一個設(shè)計(jì)的不同描述形式之間的功能等價性。性質(zhì)檢驗(yàn)利用時態(tài)邏輯描述設(shè)計(jì)功能,通過窮舉法驗(yàn)證設(shè)計(jì)的系統(tǒng)是否滿足功能要求。定理證明從系統(tǒng)的公理出發(fā),使用推理規(guī)則逐步推導(dǎo)出其所期望特性的證明過程,該方法對驗(yàn)證人員數(shù)學(xué)功底和推導(dǎo)能力要求很高,在學(xué)術(shù)研究之外應(yīng)用較少。研究形式驗(yàn)證在實(shí)際項(xiàng)目中的應(yīng)用,對于提高驗(yàn)證效率,縮短產(chǎn)品開發(fā)周期具有重要意義。

    本文基于一款處理器芯片的浮點(diǎn)運(yùn)算單元,應(yīng)用Cadence公司JasperGold形式驗(yàn)證工具,針對流水控制和計(jì)算單元中的關(guān)鍵模塊分別采用了FPVSEC進(jìn)行驗(yàn)證。

1 SAR驗(yàn)證

    軟件結(jié)構(gòu)寄存器(Software Architected Register,SAR)在浮點(diǎn)運(yùn)算單元流水線中作為第二級存儲區(qū)域。SAR整體4個讀端口和4個寫端口,其內(nèi)部由8個bank塊組成,每個bank塊的本質(zhì)是SRAM,一個SRAM是一讀一寫,有128個entry,64個結(jié)構(gòu)寄存器。SAR進(jìn)行讀/寫操作時,會從8個bank中選擇bank塊的對應(yīng)entry,將其中數(shù)據(jù)傳輸?shù)狡渲幸粋€讀/寫端口處。當(dāng)出現(xiàn)多個讀/寫操作訪問同一個bank塊時,會發(fā)生沖突,需要報(bào)錯。

    SAR的性質(zhì)檢驗(yàn)采用的是JasperGold的FPV。性質(zhì)檢驗(yàn)的主要工作是根據(jù)驗(yàn)證的需要編寫對應(yīng)的性質(zhì)(property),性質(zhì)的構(gòu)建方式和完備程度會直接影響到驗(yàn)證的效果。常用編寫property的語言有System Verilog和PSL(Property Specification Language),JasperGold對這兩種語言都支持。SAR主要的驗(yàn)證要點(diǎn):(1)遍歷整個讀寫的地址空間;(2)發(fā)生沖突時,能否報(bào)錯;(3)檢測在不同的工作模式下,是否能正常工作。

    在進(jìn)行端對端數(shù)據(jù)傳輸時,數(shù)據(jù)包在數(shù)據(jù)通路中會經(jīng)過緩沖器或存儲器,需要進(jìn)行數(shù)據(jù)傳輸完整性驗(yàn)證。因?yàn)榇鎯ζ鬟@類結(jié)構(gòu)易于理解而且很少會出現(xiàn)bug,所以在整個項(xiàng)目的驗(yàn)證過程中不會引起大家的關(guān)注。但是因?yàn)榇鎯ζ骶薮蟮臓顟B(tài)空間,使其成為提高形式化驗(yàn)證性能的瓶頸。為解決這一問題,在對SAR進(jìn)行驗(yàn)證時,使用了JasperGold提供的形式計(jì)分板證明加速器(Formal Scoreboard Proof Accelerator,PA)。PA可以把存儲器進(jìn)行抽象化,同時保留充分的信息,確保Formal Scoreboard中結(jié)果的精確。在SAR具體驗(yàn)證時,用PA替換了SAR中的bank,同時為了簡化驗(yàn)證復(fù)雜度,在構(gòu)建屬性斷言時,核心思想是:在沒有發(fā)生沖突的情況下,讀操作讀取的數(shù)據(jù)應(yīng)該等于上一次寫操作對應(yīng)地址的寫入數(shù)據(jù)。Check會對相對應(yīng)寫操作數(shù)據(jù)和讀數(shù)據(jù)進(jìn)行對比,同時檢測沖突發(fā)生的情況,具體的驗(yàn)證構(gòu)如圖1所示。

wdz3-t1.gif

    通過對驗(yàn)證結(jié)果分析,發(fā)現(xiàn)編寫的property涵蓋了所有的驗(yàn)證要點(diǎn),且全部得到了證明。尤其是使用PA之后,證明消耗的時間大大縮短,驗(yàn)證性能提升顯著。如圖2和圖3所示,沒有使用PA前,針對SAR一個端口遍歷所有讀寫地址空間,總的證明時間為286.41 s,使用PA之后,所需的證明時間僅為1.04 s。

wdz3-t2.gifwdz3-t3.gif

2 ECC驗(yàn)證

    為了保持?jǐn)?shù)據(jù)的正確性和一致性,浮點(diǎn)運(yùn)算單元的流水線控制中引入了糾錯碼(Error Correcting Code,ECC)校驗(yàn)機(jī)制,實(shí)現(xiàn)對源操作數(shù)的錯誤檢出和及時糾正,利用數(shù)據(jù)的ECC碼可以實(shí)現(xiàn)“糾一檢二”,即僅有1 bit數(shù)據(jù)出錯時,能糾正該錯誤,當(dāng)數(shù)據(jù)有2 bit錯誤時,只能檢測出錯誤但不能恢復(fù)。

    ECC校驗(yàn)是利用數(shù)據(jù)初始的糾錯碼和讀取該數(shù)據(jù)時重新生成的ECC碼按位異或生成綜合位,根據(jù)綜合位判斷數(shù)據(jù)是否出錯,并將綜合位輸出供糾錯使用。ECC恢復(fù)是依據(jù)ECC校驗(yàn)輸出的糾錯信息糾正待糾錯數(shù)據(jù),當(dāng)數(shù)據(jù)出錯位大于一位時,錯誤不可恢復(fù)。

    ECC校驗(yàn)和ECC恢復(fù)是流水線中不同執(zhí)行階段的兩個模塊,相互獨(dú)立又相互依賴。當(dāng)數(shù)據(jù)經(jīng)過ECC校驗(yàn)?zāi)K且輸出的error信號為高時,待糾錯數(shù)據(jù)和糾錯碼被驅(qū)動給ECC恢復(fù)模塊來判斷數(shù)據(jù)是否可以恢復(fù)并糾錯。若兩個模塊分別驗(yàn)證,復(fù)雜的糾錯碼產(chǎn)生機(jī)制和有依賴關(guān)系輸入信號增加了驗(yàn)證難度。故將兩個模塊直接相連,通過對比輸入數(shù)據(jù)與糾錯后數(shù)據(jù)來驗(yàn)證模塊功能。

    如圖4所示,設(shè)計(jì)一個組合電路實(shí)現(xiàn)對輸入數(shù)據(jù)的校驗(yàn)和糾錯,接入一個錯誤數(shù)據(jù)生成模塊和糾錯碼產(chǎn)生模塊實(shí)現(xiàn)對ECC校驗(yàn)輸入信號的產(chǎn)生,避免在輸入信號property中描述復(fù)雜的糾錯碼產(chǎn)生機(jī)制。錯誤數(shù)據(jù)生成模塊根據(jù)輸入信號錯誤模式e指定注入錯誤的數(shù)量,錯誤0和錯誤1信號指定數(shù)據(jù)具體翻轉(zhuǎn)位。將ECC校驗(yàn)、ECC恢復(fù)、ECC產(chǎn)生和錯誤產(chǎn)生模塊封裝為一個整體,作為性質(zhì)檢驗(yàn)的設(shè)計(jì)實(shí)現(xiàn)。

wdz3-t4.gif

    對于組合后的ECC模塊,針對不同的數(shù)據(jù)出錯類型,有3類property需檢驗(yàn)。在數(shù)據(jù)沒有出錯的情況下,輸出信號error為0;數(shù)據(jù)有1 bit出錯時,輸出error為1,數(shù)據(jù)不可恢復(fù)為0且糾錯后數(shù)據(jù)與輸入數(shù)據(jù)相等;數(shù)據(jù)有2 bit錯誤時,輸出error為1且數(shù)據(jù)不可恢復(fù)信號為1。根據(jù)錯誤位產(chǎn)生的邏輯,當(dāng)需要產(chǎn)生2 bit錯誤時,需要保證兩次的翻轉(zhuǎn)位不同,即錯誤0!=錯誤1。實(shí)際的流水線邏輯中數(shù)據(jù)位寬為128 bit,對數(shù)據(jù)的高64 bit和低64 bit分別描述其property驗(yàn)證。

    JasperGold會遍歷所有的狀態(tài)空間,驗(yàn)證結(jié)果顯示耗時101 s,證明了設(shè)計(jì)包含描述的所有屬性,說明ECC校驗(yàn)?zāi)K“檢二”和ECC恢復(fù)模塊“糾一”的功能實(shí)現(xiàn)。

3 共用模塊的等價性檢驗(yàn)

    浮點(diǎn)單元的運(yùn)算模塊非常適合形式化驗(yàn)證,尤其是等價性檢驗(yàn)。進(jìn)行等價性檢驗(yàn)主要的工作在于開發(fā)一個符合設(shè)計(jì)規(guī)格的參考模型,參考模型可以根據(jù)需要靈活的應(yīng)用不同語言編寫。目前業(yè)界主流的形式化驗(yàn)證工具只支持Verilog HDL和VHDL,RTL到RTL的等價性檢驗(yàn)已經(jīng)發(fā)展比較成熟,有著相對完善的標(biāo)準(zhǔn)。本文采用的JasperGold支持Verilog HDL和VHDL這兩種語言,也有一些工具支持C語言,但C到RTL的等價性檢驗(yàn)應(yīng)用較少,發(fā)展不是很成熟。

    在浮點(diǎn)單元運(yùn)算IP設(shè)計(jì)開發(fā)時,先對多個運(yùn)算IP中共用的基本模塊進(jìn)行了統(tǒng)一設(shè)計(jì),在之后各個IP設(shè)計(jì)中對共用模塊進(jìn)行統(tǒng)一調(diào)用。所以,浮點(diǎn)單元運(yùn)算IP的驗(yàn)證工作先是對共用模塊進(jìn)行驗(yàn)證,然后是對各個IP的驗(yàn)證。出于項(xiàng)目實(shí)際情況考慮,在對共用模塊進(jìn)行驗(yàn)證時,因?yàn)楣灿媚K實(shí)現(xiàn)的功能相對單一,復(fù)雜度不高,所以共用模塊的參考模型使用Verilog HDL編寫。而對運(yùn)算IP驗(yàn)證的時候,因?yàn)镮P復(fù)雜度高,開發(fā)相應(yīng)參考模型的工作量很大,因此形式化驗(yàn)證和仿真驗(yàn)證共用了統(tǒng)一由C語言開發(fā)的參考模型。由于JasperGold不支持C到RTL的等價性檢驗(yàn),在對IP驗(yàn)證的時候使用了其它的驗(yàn)證平臺。

    共用模塊的等價性檢驗(yàn)采用的是JasperGold的SEC,主要包括加法器、減法器、循環(huán)移位器、前導(dǎo)零、4-2壓縮器、舍入器(rounder)等模塊。在編寫參考模型時,除了保證其可綜合之外,還需要考慮功能的正確。

    圖5給出了rounder的形式驗(yàn)證報(bào)告,可以看出,相比于仿真驗(yàn)證,證明時間幾乎為0,驗(yàn)證速度明顯提高。而且這一優(yōu)勢在對整個IP進(jìn)行驗(yàn)證時更加突出,對浮點(diǎn)單元各個運(yùn)算IP進(jìn)行等價性驗(yàn)證時,除了乘加模塊需要對參考模型進(jìn)行特殊的改動[3],其它模塊包括除法、倒數(shù)估值等模塊,都能夠比較快速地收斂,極大地縮減驗(yàn)證周期。

wdz3-t5.gif

4 總結(jié)

    本文主要介紹了形式化驗(yàn)證方法在浮點(diǎn)單元功能驗(yàn)證中的具體應(yīng)用。結(jié)果表明,相比模擬仿真驗(yàn)證,形式化驗(yàn)證不用構(gòu)造復(fù)雜的驗(yàn)證平臺和編寫海量的測試激勵,在極大減少驗(yàn)證工作量的同時,提高了的可靠性,縮短了驗(yàn)證周期。

參考文獻(xiàn)

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

[2] 陳云霽,馬麟,沈海華,等.龍芯2號微處理器浮點(diǎn)除法功能部件的形式驗(yàn)證[J].計(jì)算機(jī)研究與發(fā)展,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.



作者信息:

朱  峰,魯征浩,朱  青

(蘇州大學(xué),江蘇 蘇州215006)

此內(nèi)容為AET網(wǎng)站原創(chuàng),未經(jīng)授權(quán)禁止轉(zhuǎn)載。