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

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

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

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

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

一系列屬性構成系統規范的抽象模型。模型檢驗軟件負責處理每個屬性，為全面驗證屬性，將涵蓋設計所有可達的狀態。如果屬性失效，那么模型檢測器會返回反例，說明屬性未滿足重設要求。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

為完成上述任務，我們采用 IPC來驗證 SEM 內核中與硬件相關的軟件的準確性。

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

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

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

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

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

SEM 內核還涉及到更深層次的設計因素，也有助于降低屬性復雜性。SEM 內核固件和 PicoBlaze 微架構的有關方面以及如何實施以簡化屬性創建等，都與此相關。

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

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

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

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

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

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

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

描述某個周期內處理器的狀態時，架構狀態數量的描述相對簡單。這種可管理的狀態描述可直接向 OneSpin360 MV 的屬性生成工具提供信息。

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

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

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

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

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

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

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

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

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

致力于打造高質量
在我們的調研中，我們演示了用于形式驗證賽靈思 SEM 內核中高度集成的硬件和固件的 IPC 方法。在統一的驗證環境中，用 1700 個并行驗證的屬性對 SEM 內核進行了全面驗證。在驗證過程中，采用了最新形式驗證技術和工具。驗證結果則能讓您對 SEM 內核的功能準確性信心大增，同時突現了賽靈思繼續致力于打造高質量 IP。