0 引言

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

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

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

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

1 SAR驗(yàn)證

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

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

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

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

2 ECC驗(yàn)證

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

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

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

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

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

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

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

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

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

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

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

4 總結(jié)

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

參考文獻(xiàn)

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

[2] 陳云霽,，馬麟，沈海華,，等.龍芯2號(hào)微處理器浮點(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）