從移動設(shè)備到汽車乃至工業(yè)機械，越來越多的產(chǎn)品采用需要軟硬件協(xié)同工作的高級處理技術(shù)來執(zhí)行一系列艱巨的任務(wù)。不過，隨著系統(tǒng)日趨復(fù)雜性，設(shè)計人員在驗證軟硬件是否能夠協(xié)同工作方面也面臨著日益嚴(yán)峻的挑戰(zhàn)。過去數(shù)十年來，企業(yè)和研究人員已推出一系列相關(guān)方法。不過，要想驗證軟硬件是否能如愿協(xié)同工作，仍然困難重重。

10 多年來，形式驗證技術(shù)一直是設(shè)計團隊進行硬件準(zhǔn)確性驗證工作最具發(fā)展?jié)摿Φ募夹g(shù)之一。最近據(jù)英特爾公司透露，該公司工程師正是采用了這種驗證技術(shù)，才解決了上世紀(jì) 90 年代 Pentium I 微處理器浮點單元問題。[1] 形式驗證技術(shù)隨后備受英特爾及眾多其它硬件設(shè)計公司推崇，不過這種技術(shù)仍是一種比較冷門的選擇。軟硬件協(xié)同驗證的形式驗證技術(shù)在業(yè)界仍未得到廣泛采用。

OneSpin Solutions 公司、凱澤斯勞滕大學(xué) (University of Kaiserslautern)和賽靈思的研究人員近期聯(lián)合對如何采用形式驗證技術(shù)全面驗證賽靈思同時內(nèi)含嵌入式固件和硬件組件的 IP 軟核進行了一項調(diào)研。研究發(fā)現(xiàn)，在可擴展的形式驗證環(huán)境中，可以捕獲固件和硬件之間的互動。這項調(diào)研工作是產(chǎn)業(yè)界和學(xué)術(shù)界的一項重要合作，充分利用了近期與硬件有關(guān)的固件形式驗證技術(shù)的進步，而且采用了間隔屬性檢查(IPC) 這種有界模型檢驗方式。

模型檢驗和 IPC
形式驗證技術(shù)采用數(shù)學(xué)方法，以確保設(shè)計滿足嚴(yán)格的功能準(zhǔn)確性規(guī)范要求。它從設(shè)計模型、系統(tǒng)工作環(huán)境描述以及設(shè)計可能遇到的一系列屬性入手。隨后要驗證這些屬性能否適用于所有情況，是否會出現(xiàn)屬性失效的情況。設(shè)計人員越來越多地結(jié)合采用形式驗證和較傳統(tǒng)的仿真驗證技術(shù)，從而發(fā)揮二者的最佳優(yōu)勢。舉例來說，等效性檢驗和斷言源于形式驗證技術(shù)，不過現(xiàn)已廣泛融入仿真驗證流程之中。

模型檢驗是一種先進的系統(tǒng)自動形式驗證技術(shù)，這些系統(tǒng)可作為有限狀態(tài)機，系統(tǒng)規(guī)范則被視為時序邏輯的一系列屬性。每個屬性指定一段時間內(nèi)與系統(tǒng)狀態(tài)集相關(guān)的有效（或無效）邏輯行為。舉例來說，RESET 屬性斷言：當(dāng) RESET 信號處于活躍狀態(tài)，不管系統(tǒng)在一段時間內(nèi)轉(zhuǎn)換為何種狀態(tài)，都將返回 RESET 狀態(tài)。這些屬性能以熟悉的語言格式表達，如SystemVerilog 斷言或 SVA（見側(cè)欄：“間隔屬性檢查的工作原理”）。

一系列屬性構(gòu)成系統(tǒng)規(guī)范的抽象模型。模型檢驗軟件負(fù)責(zé)處理每個屬性，為全面驗證屬性，將涵蓋設(shè)計所有可達的狀態(tài)。如果屬性失效，那么模型檢測器會返回反例，說明屬性未滿足重設(shè)要求。

模型檢驗工作自動執(zhí)行，相對迅速。與仿真驗證技術(shù)不同的是，它能全面測試系統(tǒng)模型，從而常常能夠發(fā)現(xiàn)隱蔽的問題。有時這些問題會出現(xiàn)在不起眼的角落里，有時那些為仿真測試臺創(chuàng)建刺激測試模型和斷言的驗證工程師很容易忽視問題的起因。

現(xiàn)代系統(tǒng)有大量的狀態(tài)變量，通常會出現(xiàn)所謂“狀態(tài)空間爆炸”問題，可達的狀態(tài)呈幾何級數(shù)增長。由于狀態(tài)空間非常復(fù)雜，很容易超出傳統(tǒng)模型檢測器的能力范圍，從而限制這種技術(shù)的實用性，所以才需要使用間隔屬性檢查等更新的模型檢驗方法，也就是我們在這項工作中所使用的方法 [2]。

IPC 是一種專用的有界模型檢測器。與其它有界模型檢測器一樣，IPC會將屬性范圍限制在有限的時鐘周期數(shù)之內(nèi)，從而控制整體復(fù)雜性，并采用布爾可滿足性 (SAT) 解算器來執(zhí)行實際的模型檢驗工作。IPC 和傳統(tǒng)有界模型檢測器的區(qū)別在于，它的時鐘周期窗口能允許屬性斷言在任意時間點上啟動。

IPC 還可提供一種解決狀態(tài)空間爆炸問題的簡單方法。IPC 方法通過設(shè)計抽象來指導(dǎo)用戶創(chuàng)建代表驗證的設(shè)計關(guān)鍵功能的概念狀態(tài)機 (CSM)。CSM 可捕獲給定設(shè)計中所有基本操作或事務(wù)處理。在抽象的最高層，CSM的每次狀態(tài)轉(zhuǎn)換都代表一個原子運動，被唯一的屬性所覆蓋。實際上，由于CSM 是設(shè)計提取后的抽象視圖，因此在相應(yīng)的 RTL 代碼中，每個 CSM 事務(wù)處理都對應(yīng)于多達數(shù)百個相關(guān)信號活動的時鐘周期。適當(dāng)?shù)膶傩钥刹东@全部最相關(guān)的狀態(tài)以及周期精度級的輸入輸出信號行為，支持提取的完整周期。每個屬性指定多周期時間間隔中的預(yù)期行為，精確對應(yīng)于 CSM 的一次轉(zhuǎn)換或操作。因此該方法就叫做間隔屬性檢查，也被稱作操作式間隔屬性檢查。

CSM 抽象有意不捕獲底層 RTL設(shè)計的所有細節(jié)，而只是詳細闡述對捕獲完整系統(tǒng)行為至關(guān)重要的控制狀態(tài)子集，以縮減狀態(tài)空間和降低狀態(tài)轉(zhuǎn)換復(fù)雜性。這樣，IPC 就不同于基于斷言的標(biāo)準(zhǔn)驗證（該驗證需要設(shè)計人員向 RTL 代碼添加局部信號級斷言，并通過仿真或盡可能使用形式驗證技術(shù)來進行檢查）。很多情況下這種斷言會檢查設(shè)計人員在實施 RTL 代碼相應(yīng)部分時所推斷的先決條件。這些局部斷言與 IP 模塊規(guī)范的關(guān)系可能不夠清楚。此外，這種手動生成的斷
言在整個代碼庫中不規(guī)則分布，難以分析其是否覆蓋了整個設(shè)計功能。

下面，對所有可能的狀態(tài)轉(zhuǎn)換進行自動全面的探索，并對其相應(yīng)的屬性予以驗證。任何屬性失效會突出顯示，并提供導(dǎo)致失效的反例細節(jié)。帶有OneSpin 360 MV 形式驗證工具的操作式 IPC 還能自動進行完整性驗證分析。這也可以采用同樣先進的用于驗證 CSM 屬性的屬性檢查技術(shù)（采用高效的布爾可滿足性解算器）來完成。

完整性證明能夠確保每個可能的輸入序列都有唯一的操作屬性鏈來確定設(shè)計行為。鏈的屬性通過 CSM 中的抽象開始狀態(tài)和結(jié)束狀態(tài)鏈接在一起，而輸入觸發(fā)器則匹配考慮中的各個輸入跡線。此外，分析過程中要檢查每個屬性是否分別指定了特定時間間隔內(nèi)所有相關(guān)的輸出信號，并確保各時間間隔彼此相連，不會存在輸出行為描述上的任何漏洞。

這樣，證明完整性時就能整體檢查屬性集。如果檢查通過，就不會出現(xiàn)屬性集無法確定設(shè)計行為的輸入情況。因此，屬性集也能涵蓋完整的設(shè)計功能。

隨著越來越多地要求對嵌入式固件及其與硬件互動進行驗證，采用形式驗證方法始終是一個挑戰(zhàn)，也需要不斷積極研究。分別對固件和硬件組件進行驗證一直是標(biāo)準(zhǔn)做法，但這最終需要花費大量時間進行全系統(tǒng)集成。此前，驗證工程師采用間隔屬性檢查，主要是用于硬件子系統(tǒng)的形式驗證。不過近期調(diào)研發(fā)現(xiàn)，已找到將這種方法擴展應(yīng)用于含有硬件和固件的更完整系統(tǒng)上的途徑。這項工作的重點就是通過將 IPC 應(yīng)用到賽靈思商用 IP 軟核（即軟錯誤緩解 (SEM) 內(nèi)核）來評估描述固件、硬件及二者之間互動情況的統(tǒng)一形式驗證環(huán)境( http://www.xilinx.com/cn/products/intellectual-property/SEM.htm )。該內(nèi)核包括寄存器傳輸級 (RTL) 邏輯和一個PicoBlaze™ 微控制器。

SEM 內(nèi)核
為更好地了解驗證工作，我們先進一步了解一下這個 IP 軟核。這個賽靈思 IP 軟核不僅能檢測、歸類并糾正賽靈思 FPGA 配置存儲器中的錯誤，而且還可為測試目的注入錯誤。

新型半導(dǎo)體產(chǎn)品容易受到高能級輻射的干擾。比方說，高能中子產(chǎn)生單粒子翻轉(zhuǎn) (SEU)，直接影響芯片，進而導(dǎo)致配置存儲器單元狀態(tài)的變化。為了緩解上述影響， 賽靈思FPGA 配置幀的存儲器單元都采用單錯誤糾正/ 雙錯誤檢測硬件模塊保護機制。對航空器儀表等特定應(yīng)用而言，還應(yīng)采取更為精密的糾錯機制，以抵御極高能級輻射帶來的影響。SEM 內(nèi)核可通過賽靈思 FPGA 中的FRAME_ECC 端口來監(jiān)控糾錯碼(ECC) 模塊的狀態(tài)，然后針對這些情況提供適當(dāng)?shù)慕鉀Q方案。

SEM 內(nèi)核采用賽靈思 PicoBlaze微控制器來監(jiān)控配置存儲器單元的狀態(tài)，并根據(jù)需要采取糾錯措施。設(shè)計人員可將 SEM 內(nèi)核集成到設(shè)計中，并與設(shè)計中的其它電路系統(tǒng)組合在一起，實現(xiàn)更高級的防輻射保護機制，滿足應(yīng)用需求。如果檢測到配置存儲器錯誤，SEM 內(nèi)核能直接糾正，或?qū)㈠e誤情況通報給更高一級的系統(tǒng)設(shè)計。

正確操作 SEM 內(nèi)核至關(guān)重要，因為其唯一目的就是確保用戶 FPGA電路的準(zhǔn)確性。賽靈思已對該內(nèi)核進行了全面驗證，不過應(yīng)當(dāng)指出的是，由于種種原因，該 IP 的驗證確實非常艱難。

該內(nèi)核與 UART、前面提到的FRAME_ECC、FPGA 的內(nèi)部配置訪問端口 (ICAP) 和定制錯誤注入接口等接口進行通信。雖然我們對這些接口了如指掌，但卻很難以各種可能的輸入組合加以操作， 讓嵌入式PicoBlaze 微控制器唱重頭戲。SEM內(nèi)核功能的形式驗證要求我們捕獲如下三者之間的互動情況：用匯編代碼編寫的 PicoBlaze 固件、封裝邏輯以及規(guī)范文檔中所述系統(tǒng)資源的外部接口。

為完成上述任務(wù)，我們采用 IPC來驗證 SEM 內(nèi)核中與硬件相關(guān)的軟件的準(zhǔn)確性。

采用 IPC 對固件和硬件進行形式驗證
在對總線協(xié)議的啟動代碼或驅(qū)動程序及其運行所在的硬件等低級固件進行形式驗證時，設(shè)計團隊往往面臨著巨大挑戰(zhàn)。近期，德國凱澤斯勞滕大學(xué)電子設(shè)計自動化集團的一個團隊介紹了一種將 IPC 擴展應(yīng)用于到軟硬件協(xié)同驗證的方法 [3]。其中要解決的難題就是如何處理包含成百上千代碼行代碼的狀態(tài)空間爆炸問題。

該團隊的主要觀點是，利用間隔屬性抽象為有限狀態(tài)序列集，這些序列集用大量代碼行表示，在此基礎(chǔ)上進行操作式屬性檢查。這樣，該技術(shù)可在單個概念狀態(tài)機中將軟硬件事件結(jié)合在一起。通用計算模型采用 IPC方法，首次支持軟硬件交互表示和調(diào)試。當(dāng)然，這種方法也存在局限性，也不適用于所有類型的軟件。特別需要指出的是，大量使用遞歸的代碼不在當(dāng)前討論范疇之中。

驗證 SEM 內(nèi)核時，我們采用固件控制流程圖 (CFG) 來生成屬性模板。基本模塊之間的每個轉(zhuǎn)換都被視為獨立的屬性，由 PicoBlaze 微控制器內(nèi)置的寄存器或外部事件所觸發(fā)。給定周期中描述抽象開始/ 結(jié)束狀態(tài)的功能僅取決于 PicoBlaze 架構(gòu)狀態(tài)及任何外部刺激。

IPC 需要描述 SEM 內(nèi)核在斷言開始/ 結(jié)束時的狀態(tài)，這時我們需要檢查 PicoBlaze 固件和 FPGA 邏輯的RTL 代碼。圖 1 顯示了固件和硬件狀態(tài)的組合。需要注意的是，PicoBlaze微控制器在真正實現(xiàn)軟件有限狀態(tài)機，且其行為直接影響到封裝硬件。如果可能，單獨驗證固件需要一個硬件總線功能模型 (BFM) 接口，實際上這會產(chǎn)生又一個行為測試平臺。不過，IPC 的擴展使我們能在統(tǒng)一的驗證環(huán)境中對包含硬件和固件的全系統(tǒng)的行為進行建模。我們本來能在指令集仿真器中運行固件并對其進行編譯，但卻無法在一個環(huán)境中全面捕獲硬件和固件系統(tǒng)行為。而使用 IPC，我們則可以在統(tǒng)一的硬件/ 固件驗證環(huán)境實現(xiàn)上述操作。

在構(gòu)建屬性時，我們可反復(fù)限制其復(fù)雜性，從而在 OneSpin 360 MV工具中我們就任何給定屬性的復(fù)雜性及其評估時間進行折中，實現(xiàn)最佳平衡。在本例中，我們發(fā)現(xiàn)讓屬性的間隔在 100 個周期以下比較好，這樣屬性驗證可在 30分鐘內(nèi)完成。

SEM 內(nèi)核還涉及到更深層次的設(shè)計因素，也有助于降低屬性復(fù)雜性。SEM 內(nèi)核固件和 PicoBlaze 微架構(gòu)的有關(guān)方面以及如何實施以簡化屬性創(chuàng)建等，都與此相關(guān)。

首先，我們可利用 SEM 內(nèi)核嵌入式固件的某些特性：
? 固件鏡像可實現(xiàn)軟件有限狀態(tài)機，其某些特性有助于正式描述處理器狀態(tài)。特別需要指出的是，固件不會動態(tài)分配存儲器，也不會調(diào)用無限遞歸。這是一般低級嵌入式軟件的典型情況。固件的這兩大特性能大幅簡化處理器狀態(tài)及其存儲器的建模。

? 向驗證工程師提供全局變量和局部變量的詳盡內(nèi)存映射。SEM 內(nèi)核可提供封裝 RTL 中用于觸發(fā)固件狀態(tài)轉(zhuǎn)換的全部外部變量，以便配合供OneSpin 360 MV 工具，共同探索。

? 最后，固件機代碼存儲在 SEM 內(nèi)核的 ROM 中。由于 ROM 可提供可視化驗證流程，因此無需全面驗證 PicoBlaze 微控制器上可運行的任何程序，而只需驗證 ROM 中實際存儲的程序。換言之，經(jīng)現(xiàn)場驗證適用于所有固件的 PicoBlaze 微控制器，我們不必再次驗證。我們可集中精力驗證 PicoBlaze 微控制器與SEM 內(nèi)核的固件以及 wrapper RTL 之間的互動情況。

其次，我們還可利用 PicoBlaze 微架構(gòu)的特性來描述固件鏡像的狀態(tài)。PicoBlaze 微架構(gòu)的一些特性能簡化其在形式驗證工具流程中的集成。

? 指令的執(zhí)行井然有序。由于 SEM內(nèi)核中指令執(zhí)行連續(xù)進行，因此我們能確切知道固件內(nèi)某條指令相對于其它指令的啟動時間。

? 每條指令的解碼或執(zhí)行需要兩個周期。由于 SEM 內(nèi)核固件工作中時延是確定的，因此我們能創(chuàng)建出囊括多條指令的屬性，而這些指令則能根據(jù)確定的總時延加以執(zhí)行。

? PicoBlaze 微架構(gòu)支持有限堆棧深度。堆棧內(nèi)容是 SEM 內(nèi)核狀態(tài)的關(guān)鍵部分，但有限深度情況下，該狀態(tài)不會超過設(shè)定的深度。由于屬性驗證的復(fù)雜性隨狀態(tài)數(shù)量的增加而增大，因此堆棧內(nèi)部設(shè)定的深度可簡化驗證工作。

描述某個周期內(nèi)處理器的狀態(tài)時，架構(gòu)狀態(tài)數(shù)量的描述相對簡單。這種可管理的狀態(tài)描述可直接向 OneSpin360 MV 的屬性生成工具提供信息。

有了這些簡化因素，我們就要描述相關(guān)的狀態(tài)轉(zhuǎn)換了。我們可將作為各個設(shè)計狀態(tài)的固件基本模塊映射后直接描述。從定義上看，基本模塊包括線性指令序列。每個條件跳轉(zhuǎn)或條件函數(shù)調(diào)用都可決定一個基本模塊或兩個潛在后續(xù)模塊的終點。指令的目標(biāo)地址標(biāo)志著新基本模塊的起點。控制流程圖包含基本模塊及后續(xù)關(guān)系。圖中每個邊緣都對應(yīng)于固件的條件分支，并標(biāo)明分支條件。

如果用高級語言來實現(xiàn)固件，則編譯器可自動生成 CFG。不過，借助（符號）指令集仿真器，我們同樣也可從匯編代碼中抽象 CFG。該技術(shù)還能支持僅提供匯編代碼的傳統(tǒng)平臺的協(xié)同驗證。

驗證 SEM 內(nèi)核時，我們采用固件CFG 來生成屬性模板。基本模塊間的每次轉(zhuǎn)換都視為 PicoBlaze 內(nèi)置寄存器或外部事件觸發(fā)的獨立屬性。任何給定周期中描述抽象開始/ 結(jié)束狀態(tài)的功能僅取決于 PicoBlaze 架構(gòu)狀態(tài)和所有外部刺激。

作為外部刺激到架構(gòu)狀態(tài)映射的一部分，實踐證明我們必須指定每個條件跳轉(zhuǎn)或函數(shù)調(diào)用的分支條件。我們關(guān)心的是設(shè)計的整體行為，因此我們要指定外部輸入事件或封裝電路重要的狀態(tài)寄存器（而不是嵌入式處理器的局部狀態(tài)寄存器）的條件。觸發(fā)條件下評估的封裝寄存器可成為抽象狀態(tài)定義的一部分。

SEM 內(nèi)核固件和 PicoBlaze 微控制器本身都能進行條件簡化，因此我們能就處理器狀態(tài)和外部刺激定義所有固件狀態(tài)轉(zhuǎn)換。這種狀態(tài)涵蓋固件和硬件， 可將設(shè)計的整體行為與OneSpin 360 MV 工具中的抽象概念有限狀態(tài)機相關(guān)聯(lián)。

屬性的生成
我們發(fā)現(xiàn)，SEM 內(nèi)核的固件和硬件均能用 1700 種屬性描述，這些屬性捕獲了設(shè)計及其接口的端對端功能。我們用 OneSpin 360 MV 來檢查屬性，并探索整個屬性集的完整性。屬性能并行驗證，服務(wù)器集群中屬性驗證最長大概需要 30 分鐘才能完成。

乍然一看，總共 1700 個屬性好像很多。不過，大多數(shù)屬性（約 1500 個）的驗證只涉及順序 UART 的等待循環(huán)，順序 UART 除轉(zhuǎn)存控制器的狀態(tài)信息外，主要用于調(diào)試目的。切記，每個屬性都是一個以條件跳轉(zhuǎn)結(jié)束的基本軟件模塊，因此每個 UART 等待循環(huán)都會在形式模型中創(chuàng)建唯一的屬性。就設(shè)計的全面驗證來說，我們發(fā)現(xiàn)等待循環(huán)期間無法預(yù)見的負(fù)面效果不會破壞抽象狀態(tài)內(nèi)容。

總之，生成的屬性貫穿固件的整個控制流程，描述了相應(yīng)固件基本模塊執(zhí)行過程中設(shè)計的輸入/ 輸出行為。就本案例研究而言，上述屬性配合現(xiàn)有的驗證測試平臺，可讓您對內(nèi)核功能的準(zhǔn)確性信心百倍。

生成的屬性還反映出一個情況，即 SEM 內(nèi)核錯誤注入測試特性可將錯誤注入到某個配置存儲器位置，不過只有在不按 SEM 內(nèi)核產(chǎn)品文檔建議的方式操作錯誤注入端口時才會發(fā)生此類情況。雖然該問題在正常操作條件下不會發(fā)生， 但賽靈思還是更新了SEM 內(nèi)核特性，從而徹底杜絕了這種可能性。

致力于打造高質(zhì)量
在我們的調(diào)研中，我們演示了用于形式驗證賽靈思 SEM 內(nèi)核中高度集成的硬件和固件的 IPC 方法。在統(tǒng)一的驗證環(huán)境中，用 1700 個并行驗證的屬性對 SEM 內(nèi)核進行了全面驗證。在驗證過程中，采用了最新形式驗證技術(shù)和工具。驗證結(jié)果則能讓您對 SEM 內(nèi)核的功能準(zhǔn)確性信心大增，同時突現(xiàn)了賽靈思繼續(xù)致力于打造高質(zhì)量 IP。