從移動(dòng)設(shè)備到汽車乃至工業(yè)機(jī)械，越來越多的產(chǎn)品采用需要軟硬件協(xié)同工作的高級(jí)處理技術(shù)來執(zhí)行一系列艱巨的任務(wù)。不過，隨著系統(tǒng)日趨復(fù)雜性，設(shè)計(jì)人員在驗(yàn)證軟硬件是否能夠協(xié)同工作方面也面臨著日益嚴(yán)峻的挑戰(zhàn)。過去數(shù)十年來，企業(yè)和研究人員已推出一系列相關(guān)方法。不過，要想驗(yàn)證軟硬件是否能如愿協(xié)同工作，仍然困難重重。
10 多年來，形式驗(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)單元問題。[1] 形式驗(yàn)證技術(shù)隨后備受英特爾及眾多其它硬件設(shè)計(jì)公司推崇，不過這種技術(shù)仍是一種比較冷門的選擇。軟硬件協(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ì)人員越來越多地結(jié)合采用形式驗(yàn)證和較傳統(tǒng)的仿真驗(yàn)證技術(shù)，從而發(fā)揮二者的最佳優(yōu)勢(shì)。舉例來說，等效性檢驗(yàn)和斷言源于形式驗(yàn)證技術(shù)，不過現(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)的有效（或無效）邏輯行為。舉例來說，RESET 屬性斷言：當(dāng) RESET 信號(hào)處于活躍狀態(tài)，不管系統(tǒng)在一段時(shí)間內(nèi)轉(zhuǎn)換為何種狀態(tài)，都將返回 RESET 狀態(tài)。這些屬性能以熟悉的語言格式表達(dá)，如SystemVerilog 斷言或 SVA（見側(cè)欄：“間隔屬性檢查的工作原理”）。
一系列屬性構(gòu)成系統(tǒng)規(guī)范的抽象模型。模型檢驗(yàn)軟件負(fù)責(zé)處理每個(gè)屬性，為全面驗(yàn)證屬性，將涵蓋設(shè)計(jì)所有可達(dá)的狀態(tài)。如果屬性失效，那么模型檢測(cè)器會(huì)返回反例，說明屬性未滿足重設(shè)要求。
模型檢驗(yàn)工作自動(dòng)執(zhí)行，相對(duì)迅速。與仿真驗(yàn)證技術(shù)不同的是，它能全面測(cè)試系統(tǒng)模型，從而常常能夠發(fā)現(xiàn)隱蔽的問題。有時(shí)這些問題會(huì)出現(xiàn)在不起眼的角落里，有時(shí)那些為仿真測(cè)試臺(tái)創(chuàng)建刺激測(cè)試模型和斷言的驗(yàn)證工程師很容易忽視問題的起因。
現(xiàn)代系統(tǒng)有大量的狀態(tài)變量，通常會(huì)出現(xiàn)所謂“狀態(tài)空間爆炸”問題，可達(dá)的狀態(tài)呈幾何級(jí)數(shù)增長(zhǎng)。由于狀態(tài)空間非常復(fù)雜，很容易超出傳統(tǒng)模型檢測(cè)器的能力范圍，從而限制這種技術(shù)的實(shí)用性，所以才需要使用間隔屬性檢查等更新的模型檢驗(yàn)方法，也就是我們?cè)谶@項(xiàng)工作中所使用的方法 [2]。
IPC 是一種專用的有界模型檢測(cè)器。與其它有界模型檢測(cè)器一樣，IPC會(huì)將屬性范圍限制在有限的時(shí)鐘周期數(shù)之內(nèi)，從而控制整體復(fù)雜性，并采用布爾可滿足性 (SAT) 解算器來執(zhí)行實(shí)際的模型檢驗(yàn)工作。IPC 和傳統(tǒng)有界模型檢測(cè)器的區(qū)別在于，它的時(shí)鐘周期窗口能允許屬性斷言在任意時(shí)間點(diǎn)上啟動(dòng)。
IPC 還可提供一種解決狀態(tài)空間爆炸問題的簡(jiǎn)單方法。IPC 方法通過設(shè)計(jì)抽象來指導(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)換或操作。因此該方法就叫做間隔屬性檢查，也被稱作操作式間隔屬性檢查。
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í)斷言，并通過仿真或盡可能使用形式驗(yàn)證技術(shù)來進(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ù)（采用高效的布爾可滿足性解算器）來完成。
完整性證明能夠確保每個(gè)可能的輸入序列都有唯一的操作屬性鏈來確定設(shè)計(jì)行為。鏈的屬性通過 CSM 中的抽象開始狀態(tài)和結(jié)束狀態(tài)鏈接在一起，而輸入觸發(fā)器則匹配考慮中的各個(gè)輸入跡線。此外，分析過程中要檢查每個(gè)屬性是否分別指定了特定時(shí)間間隔內(nèi)所有相關(guān)的輸出信號(hào)，并確保各時(shí)間間隔彼此相連，不會(huì)存在輸出行為描述上的任何漏洞。
這樣，證明完整性時(shí)就能整體檢查屬性集。如果檢查通過，就不會(huì)出現(xiàn)屬性集無法確定設(shè)計(jì)行為的輸入情況。因此，屬性集也能涵蓋完整的設(shè)計(jì)功能。
隨著越來越多地要求對(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)證。不過近期調(diào)研發(fā)現(xiàn)，已找到將這種方法擴(kuò)展應(yīng)用于含有硬件和固件的更完整系統(tǒng)上的途徑。這項(xiàng)工作的重點(diǎn)就是通過將 IPC 應(yīng)用到賽靈思商用 IP 軟核（即軟錯(cuò)誤緩解 (SEM) 內(nè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è)、歸類并糾正賽靈思 FPGA 配置存儲(chǔ)器中的錯(cuò)誤，而且還可為測(cè)試目的注入錯(cuò)誤。
新型半導(dǎo)體產(chǎn)品容易受到高能級(jí)輻射的干擾。比方說，高能中子產(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í)輻射帶來的影響。SEM 內(nèi)核可通過賽靈思 FPGA 中的FRAME_ECC 端口來監(jiān)控糾錯(cuò)碼(ECC) 模塊的狀態(tài)，然后針對(duì)這些情況提供適當(dāng)?shù)慕鉀Q方案。
SEM 內(nèi)核采用賽靈思 PicoBlaze微控制器來監(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)證，不過應(yīng)當(dāng)指出的是，由于種種原因，該 IP 的驗(yàn)證確實(shí)非常艱難。
該內(nèi)核與 UART、前面提到的FRAME_ECC、FPGA 的內(nèi)部配置訪問端口 (ICAP) 和定制錯(cuò)誤注入接口等接口進(jìn)行通信。雖然我們對(duì)這些接口了如指掌，但卻很難以各種可能的輸入組合加以操作， 讓嵌入式PicoBlaze 微控制器唱重頭戲。SEM內(nèi)核功能的形式驗(yàn)證要求我們捕獲如下三者之間的互動(dòng)情況：用匯編代碼編寫的 PicoBlaze 固件、封裝邏輯以及規(guī)范文檔中所述系統(tǒng)資源的外部接口。
為完成上述任務(wù)，我們采用 IPC來驗(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)空間爆炸問題。
該團(tuán)隊(duì)的主要觀點(diǎn)是，利用間隔屬性抽象為有限狀態(tài)序列集，這些序列集用大量代碼行表示，在此基礎(chǔ)上進(jìn)行操作式屬性檢查。這樣，該技術(shù)可在單個(gè)概念狀態(tài)機(jī)中將軟硬件事件結(jié)合在一起。通用計(jì)算模型采用 IPC方法，首次支持軟硬件交互表示和調(diào)試。當(dāng)然，這種方法也存在局限性，也不適用于所有類型的軟件。特別需要指出的是，大量使用遞歸的代碼不在當(dāng)前討論范疇之中。
驗(yàn)證 SEM 內(nèi)核時(shí)，我們采用固件控制流程圖 (CFG) 來生成屬性模板?；灸K之間的每個(gè)轉(zhuǎn)換都被視為獨(dú)立的屬性，由 PicoBlaze 微控制器內(nèi)置的寄存器或外部事件所觸發(fā)。給定周期中描述抽象開始/ 結(jié)束狀態(tài)的功能僅取決于 PicoBlaze 架構(gòu)狀態(tài)及任何外部刺激。
IPC 需要描述 SEM 內(nè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)。不過，IPC 的擴(kuò)展使我們能在統(tǒng)一的驗(yàn)證環(huán)境中對(duì)包含硬件和固件的全系統(tǒng)的行為進(jìn)行建模。我們本來能在指令集仿真器中運(yùn)行固件并對(duì)其進(jìn)行編譯，但卻無法在一個(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)用無限遞歸。這是一般低級(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)證流程，因此無需全面驗(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)的特性來描述固件鏡像的狀態(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ì)超過設(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í)語言來實(shí)現(xiàn)固件，則編譯器可自動(dòng)生成 CFG。不過，借助（符號(hào)）指令集仿真器，我們同樣也可從匯編代碼中抽象 CFG。該技術(shù)還能支持僅提供匯編代碼的傳統(tǒng)平臺(tái)的協(xié)同驗(yàn)證。
驗(yàn)證 SEM 內(nèi)核時(shí)，我們采用固件CFG 來生成屬性模板。基本模塊間的每次轉(zhuǎn)換都視為 PicoBlaze 內(nèi)置寄存器或外部事件觸發(fā)的獨(dú)立屬性。任何給定周期中描述抽象開始/ 結(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 來檢查屬性，并探索整個(gè)屬性集的完整性。屬性能并行驗(yàn)證，服務(wù)器集群中屬性驗(yàn)證最長(zhǎng)大概需要 30 分鐘才能完成。
乍然一看，總共 1700 個(gè)屬性好像很多。不過，大多數(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)證來說，我們發(fā)現(xiàn)等待循環(huán)期間無法預(yù)見的負(fù)面效果不會(huì)破壞抽象狀態(tài)內(nèi)容。
總之，生成的屬性貫穿固件的整個(gè)控制流程，描述了相應(yīng)固件基本模塊執(zhí)行過程中設(shè)計(jì)的輸入/ 輸出行為。就本案例研究而言，上述屬性配合現(xiàn)有的驗(yàn)證測(cè)試平臺(tái)，可讓您對(duì)內(nèi)核功能的準(zhǔn)確性信心百倍。
生成的屬性還反映出一個(gè)情況，即 SEM 內(nèi)核錯(cuò)誤注入測(cè)試特性可將錯(cuò)誤注入到某個(gè)配置存儲(chǔ)器位置，不過只有在不按 SEM 內(nèi)核產(chǎn)品文檔建議的方式操作錯(cuò)誤注入端口時(shí)才會(huì)發(fā)生此類情況。雖然該問題在正常操作條件下不會(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)證過程中，采用了最新形式驗(yàn)證技術(shù)和工具。驗(yàn)證結(jié)果則能讓您對(duì) SEM 內(nèi)核的功能準(zhǔn)確性信心大增，同時(shí)突現(xiàn)了賽靈思繼續(xù)致力于打造高質(zhì)量 IP。
