0 引言

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

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

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

    本文基于一款處理器芯片的浮點運算單元,，應用Cadence公司JasperGold形式驗證工具,，針對流水控制和計算單元中的關鍵模塊分別采用了FPV和SEC進行驗證。

1 SAR驗證

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

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

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

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

2 ECC驗證

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

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

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

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

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

    JasperGold會遍歷所有的狀態(tài)空間，驗證結果顯示耗時101 s,，證明了設計包含描述的所有屬性，說明ECC校驗模塊“檢二”和ECC恢復模塊“糾一”的功能實現(xiàn),。

3 共用模塊的等價性檢驗

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

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

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

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

4 總結

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

參考文獻

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

[2] 陳云霽，馬麟,，沈海華,，等.龍芯2號微處理器浮點除法功能部件的形式驗證[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.

作者信息:

朱  峰，魯征浩,，朱  青

（蘇州大學,，江蘇 蘇州215006）