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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

正確操作 SEM 內(nèi)核至關(guān)重要，因?yàn)槠湮ㄒ荒康木褪谴_保用戶 FPGA電路的準(zhǔn)確性,。賽靈思已對(duì)該內(nèi)核進(jìn)行了全面驗(yàn)證,，不過(guò)應(yīng)當(dāng)指出的是，由于種種原因,，該 IP 的驗(yàn)證確實(shí)非常艱難,。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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