內容提要：本文討論了一種自動化形式安全驗證方法，該方法使用形式屬性檢查，并包括故障注入以驗證硬件安全機制的正確實施，并總結了對新英飛凌MCU產品系列組件的應用。

摘要

汽車MCU為駕駛輔助提供了新的先進且高度安全關鍵的功能。因此，它們配備了各種安全機制，其整個設計過程遵循ISO 26262標準。根據目標安全完整性級別，必須證明可檢測到可能違反安全目標的隨機故障，并提供可配置的響應，以便將MCU系統驅動到安全狀態。如果安全應用需要，則需要在發生故障時更正重要數據。還必須保證在后期設計階段插入的安全增強功能不會破壞MCU的正常功能行為。本文討論了一種自動化形式安全驗證方法，該方法使用形式屬性檢查，并包括故障注入以驗證硬件安全機制的正確實施，并總結了對新英飛凌MCU產品系列組件的應用。

1. 簡介

本文組織如下。在本節中，討論了這項工作的動機，并提供了背景信息。第二部分總結了近期英飛凌MCU中包含的一些適合形式化驗證的硬件安全機制。第三部分詳細介紹了我們相應的形式化安全驗證方法。第四部分描述了我們如何確保在后續添加安全措施時保留任務功能。第五部分討論了應用和結果，第六部分得出結論。

A. ISO 26262的影響

ISO 26262標準專注于3.5噸以下批量生產乘用車中安全相關電氣和電子系統的功能安全，防止因電子和電子系統故障及其相互作用而產生的潛在危害。自2012年1月推出以來，該標準要求汽車制造商及其供應商（包括芯片供應商）根據標準的工作產品中的安全要求開發所有新產品。該標準對安全相關系統開發過程中部署的流程、文檔和技術產生了重大影響，涵蓋了從初始開發階段到最終產品退役的整個生命周期。

該標準規定了4個汽車安全完整性等級（風險等級）ASIL A-D，這些等級源自暴露度（危害事件暴露的概率）、嚴重性（造成傷害的概率）和可控性（駕駛員避免傷害的機會），并對項目的要求進行分類以避免不合理的風險。對于每個風險等級，標準定義了隨機硬件失效目標值，范圍從ASIL D的 <10-8/小時=10 FIT（時間失效）到 <  10-6/小時=1000 FIT（時間失效）。

為了獲得認證，需要評估診斷覆蓋率，以表明根據ASIL分類，由實施的安全機制檢測或控制的安全相關元件失效百分比足夠高。對于ASIL D，所有可能違反安全目標的單點和殘留故障的百分比必須<=1%，即需要99%的診斷覆蓋率。

診斷覆蓋率通常由故障仿真確定，它使用故障注入，并使用不同的激活故障多次重新運行測試用例。這在計算上非常昂貴，即使現代故障仿真器采用保存相關故障仿真的算法和樣本統計而不是窮舉。一個有趣的問題是，形式化驗證對診斷覆蓋率計算有何貢獻，因為故障注入也可以在形式化模型中進行。雖然當今的形式化屬性檢查器無法像故障仿真那樣直接生成統計檢測率，但它們可以證明由特定安全機制完全保護的基本部件的100%診斷覆蓋率。

圖1. ISO 26262中的時間間隔定義

B. 形式安全驗證

除了驗證安全機制的有效性之外，形式安全驗證還可以確保最大診斷時間間隔（即故障發生和故障檢測之間的時間段）和故障反應時間（即故障檢測后驅動控制器處于安全狀態的時間）不超過安全概念中要求的最大值。在模型檢查中，不適用毫秒等時間單位，而是時鐘周期，物理延遲只能從形式工具之外的給定時鐘頻率間接計算。

由于FMEDA結果（失效模式和影響診斷分析）包括對隨機硬件故障影響的分析和對失效率以及違反安全目標的概率和比率的估計，因此在常規功能已經實施和驗證后，可能會發現必須添加或加強安全機制。反過來，如果面積和功耗方面的開銷與獲得的整體安全水平不相符，或者MCU系列的特定衍生產品的應用對安全要求不那么嚴格，則也可能更換、減少或取消安全措施。后續的安全增強或修改不得破壞設計實施和先前驗證結果的合理性。任何功能安全修改都可以通過約束順序等效性檢查來驗證。但是，我們不是使用單獨的工具，而是增強現有的屬性檢查設置，并使用自己的專用方法來驗證先前驗證的功能的保留情況。

C. 工具環境

我們的形式安全驗證方法建立在Onespin Solutions的屬性檢查器之上（但不限于此），該屬性檢查器是一種有界模型檢查器。我們經常使用它對汽車MCU系統的系統控制模塊進行IP級功能驗證。Onespin的工具環境提供了一組豐富的功能，使我們能夠為安全驗證等特定目的創建自己的定制驗證自動化程序。

屬性檢查器360 DV-Verify多年來一直應用于眾多英飛凌模塊設計。對于大多數經過形式驗證的模塊，沒有執行額外的基于仿真的驗證，而仿真的功能覆蓋不足則通過對特定方面進行形式屬性檢查來補充。

Onespin的屬性檢查器具有VHDL、Verilog、SystemVerilog以及最近的SystemC的前端。它理解不同的屬性語言。

- SVA

- PSL

- ITL（InTeval Logic，Onespin的專有屬性語言）屬性，具有VHDL或Verilog語法中的狀態表達式

以ITL編寫的屬性集可以與SVA和PSL斷言集相結合，環境約束也可以混合使用。有幾種不同的證明引擎可供選擇，它們針對不同的目的進行了優化。例如，一個引擎專門用于生成可從reset實現的反例（失敗證明）或見證（成功證明）。另一個引擎從任何起始狀態證明屬性，但可能會返回無法到達的信號軌跡。調用屬性檢查時，用戶可以指定一組要并行或順序嘗試的證明引擎。

可以為任意數量的時鐘指定用戶定義的重置序列、周期性或自由運行的時鐘方案，并且可以輸入設計輸入的屬性?？梢栽诰幾g選項中指定所有信號的類型域，以便檢查可以限制為2值邏輯或包括Z值和X值，例如以調查X-propagation。

與其他商業屬性檢查器一樣，Onespin提供linting和形式一致性檢查器，可識別死代碼、冗余代碼、粘性信號、FSM檢查、從設計中提取的代碼內斷言以及其他幾個自動生成的斷言。幾個標準“應用程序”主要針對形式驗證背景不太深的驗證工程師。他們只需要運行預定義的自動屬性生成器和證明腳本，以對X-propagation、寄存器功能、連接性和時鐘域交叉進行標準檢查。

Onespin的廣泛調試功能對于通用屬性檢查非常有用。根本原因分析器允許GUI用戶跟蹤不同時鐘周期內的扇入和扇出。屬性和RTL源代碼使用來自計數器或見證跟蹤的信號值進行注釋，并突出顯示在波形查看器中選擇的時鐘周期內活動的代碼區域。

360 DV-Verify環境包含一個形式完整性檢查器，它應用最嚴格的無間隙驗證標準，例如對所有輸入場景進行全案例拆分和無縫輸出確定。如果滿足這些標準，則將共同建立屬性和設計的順序輸入輸出等效性。這種形式完整性概念與仿真環境中使用的覆蓋率指標不兼容，并且必須編寫一套嚴格結構化的形式操作屬性才能運行形式完整性檢查，這在緊張的項目時間表內并不總是可行的。因此添加了另一個稱為Quantify的功能，它執行的覆蓋率分析更接近仿真器中使用的經典概念。在進行功能驗證時，這種基于突變覆蓋率且不需要特定結構化的屬性集或用戶交互的“指標驅動驗證”功能對于識別尚未被屬性充分覆蓋的RTL區域非常有用。

由于Onespin GUI包含一個TCL-shell和一個豐富實用的TCL實用程序庫，允許評估和控制內部數據（例如過濾信號列表、位精度扇入、屬性和約束列表或屬性的當前證明狀態），因此用戶可以很好地添加自己的TCL函數以滿足他們的目的。

Onespin還允許用戶通過編譯選項將任意端口和任意層次的內部信號切割成扇入部分和扇出部分，從而實現模型變異，扇入部分具有原始信號的扇入功能，扇入部分成為模塊的新外部輸出，扇出部分由驅動信號扇出的外部輸入代替。在附加屬性假設中，可以假設人工輸入的任何行為，包括輸入和輸出部分剛連接時的正常信號行為。對于形式的故障注入，此切割信號功能至關重要，因為它允許以非常靈活的方式指定故障模型。

D. 形式安全驗證方法的總結

我們的方法包括用于驗證安全機制的自動證明功能，包括由軟件控制的錯誤檢測、錯誤更正和自檢功能，這些功能可生成預期警報，與真實故障引起的虛假警報區分開來。自檢功能無需故障注入即可驗證，方法是通過檢查自檢激活時是否發生預期警報以及正常運行期間是否沒有警報的屬性。為此，預定義且高度可重用的通用屬性由從設計中自動生成的宏提供。

通過另一個基于故障注入的屬性集，驗證了對自發故障的正確處理。同樣，這些屬性也由生成的宏填充。

為了證明安裝硬件安全措施不會影響常規功能，本文提出了另一種方法，該方法基于在自動生成的容器架構上證明的形式等效屬性，該架構具有兩個不同的原始和修改設計實例。

E. 相關工作

我們首次概述了我們的形式安全驗證方法，從那時起，這些方法已經得到了很大的發展并應用于更多模塊。我們介紹了基于SYNOPSYS的Certitude的測試臺鑒定方法與Onespin的形式屬性檢查器的組合。對于在安全性增強或修改，已通過形式屬性完全功能驗證的設計后運行屬性回歸，我們定期使用此方法。DVCON上的Onespin教程介紹了形式屬性完整性和覆蓋率的概念。我們詳細闡述了一種自動化形式驗證方法：其基于軟件可訪問的XML定義的功能寄存器和安全相關特殊功能寄存器。由于軟件背后隱藏的寄存器也可能具有重要功能，因此本文介紹的工作覆蓋任何內部寄存器的保護。

2.硬件安全機制

本節概述了為安全關鍵寄存器實施的基本寄存器監控架構。

我們將普通寄存器替換為嵌入冗余和自檢邏輯(SFF -安全觸發器)的寄存器，這些寄存器可以是單個位或任意寬度的寄存器。

為了實現較短的診斷時間間隔，我們提供了警報減少邏輯，該邏輯將來自不同安全寄存器的警報組合成不同層次的復合警報。

測試控制器(SFFTC)組合接收到的警報，在需要時執行一些同步到目標時鐘域，并將復合警報脈沖發送到安全管理單元(SMU)，該單元包含軟件可配置邏輯，用于在較短的故障反應時間內觸發適當的操作，從而將MCU系統驅動到安全狀態。

圖2.保護結構

SMU可以不時地啟用自檢(te)，以檢查安全機制是否仍然完全正常運行。在啟用自檢時，測試控制器將發出特殊控制信號，迫使寄存器監控邏輯生成預期警報(alarm)。如果預期警報與實際收到的警報不完全匹配，測試控制器將啟動一個不同的測試警報(talarm)，向SMU指示寄存器監控存在一些故障。然后，安全軟件可能會決定重置系統的一部分并重復自檢，以區分中間故障和永久故障。

由安全觸發器(SFF)構建的寄存器包含不同類型的冗余、一些本地故障檢測邏輯，即某種比較器、由測試輸入觸發的自檢邏輯，這些自檢邏輯將以明確定義的方式操控寄存器內容，并且在某些變體中還有故障校正邏輯。因此，在一些實施例中，存在針對可校正和不可校正錯誤的單獨警報。

冗余度可能從單個奇偶校驗位到雙重（DMR-雙模塊冗余）、三重（TMR-三重模塊冗余）、ECC等。

所有這些方法的共同點是至少檢測到單個位錯誤，但只有某些方法會在可糾正錯誤的情況下恢復寄存器內容，例如TMR（通過多數投票）和具有糾正能力的ECC版本。

決定采用哪種特定的保護方法并不簡單。具有三重寄存器位的TMR解決方案往往比需要更少冗余寄存器位的ECC解決方案需要更多的面積。然而，事情并沒有那么簡單。例如，ECC編碼和解碼邏輯需要更多的組合門，而組合傳播延遲在更高的時鐘頻率域中可能是一個問題。因此，最佳解決方案取決于不同基本庫單元的各種特性，如面積和電容，設計編譯器的優化能力、布局約束以及安全關鍵組件不同時鐘域的頻率范圍。此外，對各個元素真正需要的安全措施的評估，取決于不同抽象層次上的復雜因果分析。在布局完成之前，只能估計實際面積開銷和傳播延遲。

由此可見，為單個安全關鍵功能選擇特定的強化方法，可能并不適用于所有產品版本和衍生產品，并且需要驗證安全修改不會影響任何任務功能。

3. 硬件安全機制的功能驗證

寄存器監控的有效性驗證是在不同的設置中進行的，無論是否有故障注入。

A. 無故障注入的安全驗證

如果沒有故障注入，只能驗證安全機制的一部分。警報只能在自檢模式下觸發，并且只要安全機制已正確安裝，就不會出現意外警報。

基本上有三個相應的驗證目標需要證明。目標(1)指出，當測試模式至少在自檢間隔Tst內被禁用時，在此時間間隔加上額外的診斷時間間隔Tdti結束時不會發出警報。換句話說，在自檢被禁用一段時間后，此后不會發出警報：

第二個目標(2)指定在啟用自檢時，在自檢持續時間Tst的時間間隔內經過Tdti周期的延遲后標記警報：

目標（3）排除意外警報（無故障注入）

在所有這些公式中，t都是隱式全量化的。在(2)中，必須排除重置，否則可能會中斷自檢。在其他2個證明目標中，重置不會導致違反結論，因此重置與否并不重要，因為在這兩種情況下都不會激活警報或測試警報。

雖然看起來很簡單，但這些屬性可能具有巨大的扇入，因為數百個具有完全不同常規功能的寄存器可能由單個測試控制器保護，并且需要遍歷相應的巨大狀態空間。可能導致復雜性的不是自檢，而是可能不一致的狀態，這種狀態在活動測試警報中可見，可能發生在任何受保護的寄存器位中，可能具有非常高的順序深度。因此，我們采用歸納方法，將目標(3)分為基本情況和步驟情況。

這樣拆分的原因是，這樣可以使用從任意狀態開始的更便宜的證明引擎。

請注意，這里需要證明幾個周期的基準情況，并在步驟情況下做出相應的假設。目標(1)按以下方式拆分：

通過排除幾個周期的活動測試警報，可以確保不會出現不一致的先前狀態，并且對于(1b)也可以證明結果，而無需重置假設。

測試模式下警報的證明分為以下幾部分：

重置僅針對整個檢查窗口排除。這些屬性確保警報減少中包含的所有自檢和故障檢測邏輯都已正確安裝，并且電路不會產生誤報或測試警報。但是，僅憑它們并不能保證每個安全寄存器實際上都包含在警報減少中。

B. 使用故障注入進行安全驗證

只有通過將故障注入安全寄存器，才能檢查減少警報中是否實際捕獲了本地警報信號。與仿真相比，形式驗證的一大優勢是可以詳盡地進行故障注入，并且可以檢測到任何警報不會傳播到SMU的極端情況。

由于我們已經設計了所有安全寄存器，以便可以輕松地從所有信號列表中過濾它們，因此在屬性檢查器的HDL前端詳細說明設計后，我們已經能夠開發用于生成編譯選項的函數，以便精確地剪切與安全寄存器相關的信號。其他函數生成宏，根據要檢查的故障模型，這些宏表示各個生產性或冗余寄存器位是否已連接或處于某種故障狀態。通過將所有生產性和所有冗余位組合成向量，生成額外的故障建模向量，我們可以假設任何錯誤組合并檢查是否檢測到它們。

下圖中，我們展示了雙模塊和三模塊冗余安全寄存器的切割模型，后者包括通過多數決定糾正單個位錯誤。

圖3.用于檢測（DMR）和校正（TMR）的安全觸發器

將所有這些可能大量的SFF位組合成自動生成的向量后，我們可以通過布爾函數指定翻轉n位：

因此，be(0)表示所有切割信號都已連接，be(1)表示1位被翻轉，be(n)表示n位被翻轉。

相應地，對于三重模態冗余，兩個冗余位向量被連接到具有生產位的向量。

XOR函數生成差異向量，其中1位置的數量表示注入了多少錯誤。可以明確地迭代差異向量的所有位置，并單獨檢查每次是否發出警報。相反，經過僅通過be(n)指定n個錯誤以任何組合發生，一次性完成所有這些檢查會更有效率。

顯然，如果僅假設

被添加。

如果我們假設單比特錯誤，我們現在可以證明警報和測試警報被標記

同樣，我們可以假設任意數量的故障。但是，在雙模冗余的情況下，我們必須確保不僅生產位和相應冗余位對被翻轉，因為不會檢測到此類錯誤。這是通過形成所有冗余位和所有生產位的差向量的差向量來實現的。然后我們可以實際證明，如果這個二階差向量至少有一個1位置，則會發出警報和測試警報。

相應地，我們為TMR生成保護高階差向量，以確保并非所有三元組都被翻轉或不被翻轉。

當然，問題是阿爾法粒子恰好擊中DMR對或TMR觸發器三元組，從而所有觸發器都一致翻轉的可能性有多大。通過某些措施，這種情況非常不可能，例如，一個冗余位的反轉實現和不同的測試邏輯導致布局中的物理分離。

雖然我們到目前為止一直專注于警報生成，但還需要檢查具有校正的寄存器安全機制以恢復失真數據。

由于我們使用統一的校正機制，我們能夠自動過濾掉代表校正邏輯背后的寄存器值且功能正在使用的信號。這些寄存器讀取信號再次組合成可以與差異向量相關的向量。為此，我們引入了另一個布爾函數來處理三元組中的多個位錯誤：

這里我們首先計算每個三元組的每個位中的錯誤數，并檢查這個位和是否等于參數m。如果是，我們將所有有m個錯誤的位置的總和加1。如果這個總和是n，則布爾函數返回true，否則返回false。在總和表達式中，我們忽略了布爾、位和自然數之間的類型轉換。有了這個定義，我們可以寫一個屬性，假設n個三元組有單比特錯誤，并且沒有發生雙比特或三比特錯誤。

在此假設下，可以證明修正后的讀取向量與故障注入之前的實際功能寄存器值相同。

除了DMR/TMR保護之外，寄存器還可以通過ECC（糾錯碼）進行保護。通常，ECC碼用于具有各種數據寬度的安全關鍵數據的SRAM。不過，我們也通過ECC保護一些安全寄存器。

圖4. 寄存器的ECC保護

當使用ECC保護寄存器時，我們原則上可以安裝與圖2所示相同的警報減少架構。如果選擇了適當的ECC方法，這里可以區分可糾正和不可糾正的錯誤。SECDED（單錯誤糾正，雙錯誤檢測）已經很成熟，從數學上可以理解為能夠糾正代碼字中所有單比特錯誤的100%，并能夠檢測代碼字中任何2比特錯誤組合的100%，這在為已安裝的安全機制的診斷覆蓋提供證據方面非常有利。通過應用適當的ECC方法，我們可以向SMU發送可糾正和不可糾正錯誤的單獨減少警報。通常，所需的冗余寄存器位比二重甚至三重要少。例如，如果要通過SECDED保護32個寄存器位或32位SRAM數據字的位，則ECC寬度為7就足夠了。然而，獲得了更多的組合編碼和解碼邏輯，這增加了需要仔細考慮的傳播延遲，尤其是對于更高的頻率。根據可用的ECC代碼，可以保護不同大小的安全寄存器。安全寄存器也可以連接起來，以便通過通用ECC邏輯保護它們。

對于ECC邏輯的安全驗證，我們指定一個類似的布爾函數來表示發生了多少位錯誤：

使用此定義，可糾正錯誤的屬性指定如下，這里假設ECC具有單位錯誤糾正和不同的可糾正錯誤標志alarm_ce和talarm_ce。

如果ECC檢測到雙位錯誤，則無法確定ECC或數據位是否受到影響。因此，只能證明向SMU標記了減少的不可糾正錯誤：

對于單個故障，所有這些保護方法以及檢測和可選的糾正，都允許自動證明任何受保護寄存器位中的單個故障具有100%的診斷覆蓋率。但是，雖然可以對檢測率低于100%的多位錯誤(>2)仿真進行統計評估，但形式驗證不能直接提供這樣的診斷覆蓋率數字。例如，典型的SECDED算法可以實現高達70%的3位錯誤檢測率，并將其正確分類為不可糾正錯誤。在這里，例如，在可以證明其余70%的正確不可糾正錯誤警報的屬性之前，生成并迭代排除30%的所有可能故障的反例效率太低。

4. 安全修改的功能保留

每當添加或修改安全機制時，常規功能都可能受到新引入的極端情況的影響。例如，安全評估人員可能會要求對特別關鍵的寄存器位進行糾正，而不是僅僅進行檢測。但是，如果糾正或自檢邏輯本身存在缺陷，即使只有少數潛在組合，也可能會引入系統性錯誤，而這些錯誤會超過預期的安全收益。因此，非常充分地驗證此類安全邏輯修改非常重要。

如果有完整的屬性集，則可以在安全增強設計上重新運行屬性檢查回歸?？梢酝ㄟ^應用Onespin的形式完整性檢查器來形式證明屬性集的完整性。使用Onespin的形式覆蓋率檢查器Quantify或通過故障檢測工具Certitude可以對屬性集進行不太嚴格的評估。因此，這些經過完整性檢查的屬性集，可以高可靠性地排除后期安全增強的意外功能副作用。如果使用仿真測試臺驗證模塊，則基于Certitude的方法適用于未經形式驗證的模塊。

但是，將設計的功能驗證和安全性增強保障的責任分攤給獨立的專業驗證小組可能是可取的。當尚未進行完整的形式驗證時，已經適用的替代方法是使用故障注入進行順序等效性檢查。我們設計了一個專用程序，其中包括預分析步驟、生成具有兩個設計版本的容器架構以及生成用于等效性檢查的不變屬性。

預分析步驟使用標準文本比較函數檢查哪些RTL源文件已更改。

包含所有修改組件的組件實例層次結構中的最低實例被選為等效性檢查的頂層。我們也可以決定將此子架構中未更改的組件放入黑盒中。

在下一步中，生成一個容器架構，其中包括原始設計和修改后設計的所選子架構。容器實體將兩個子架構的輸入的并集作為輸入端口，將兩個子架構的兩組輸出作為輸出端口。如果采用黑盒處理，則黑盒組件的輸入將被視為相應子架構的輸出，而黑盒組件的輸出將被視為子架構的輸入。在容器架構中，從子架構的公共輸入繼承的包裝器輸入連接到兩個子架構。其余輸入僅連接到兩個子架構之一的相應輸入。

圖5.帶有原始模塊和安全增強模塊的容器架構

A. 無故障注入的等效性檢查

等效性檢查首先通過以下證明目標進行無故障注入設置，該證明目標指出，先前和安全增強架構的所有輸出在任何時候都是等效的：

如果從單獨指定的重置序列到達狀態空間的證明半徑較長，則該證明目標通常過于復雜，因此用歸納法代替，該方法針對基本情況（8a）和步驟情況（8b）設置單獨的目標，其中包括原始設計和增強設計的內部狀態。

可以理解的是，由于安全性增強而產生的額外輸出不予考慮。除了輸出ipx_o、ipx’_o 之外，寄存器讀取信號q、q’也包含在不變證明中。因此，即使兩種架構中具有不同或沒有冗余和自檢邏輯的寄存器的內部實現不同，輸入到扇出邏輯中的寄存器值也必須相同。

所有必需的信號都自動過濾，以便可以自動生成相應的屬性和檢查。

B. 帶故障注入的等效性檢查

帶故障注入的等效性檢查有幾種用例：

1. 將第一個原始無保護架構與第二個安全增強架構進行比較，在第二個架構中注入了可糾正的故障。

2. 將第一個安全架構與第二個修改的安全架構進行比較，在兩個架構中都注入了可糾正的故障。架構中注入的故障可以完全獨立；它們必須只能是可糾正的。

3. 將安全架構與僅在一個實例中注入可糾正故障的自身進行比較。

用例2的一個例子是用ECC或奇偶校驗位保護方法替換TMR。如果修正真的有效，根據第3節的規定，它應該已經在安全架構上得到證明，如果安全修改是合理的，那么所有功能輸出都應該是等效的。

對于等效性檢查，可以通過兩種不同的方式執行故障注入：

1. 使用如上所示的be / mbe謂詞來表示只發生可糾正的錯誤。

2. 假設發生可糾正錯誤警報。

由于已經證明1.）意味2），而非1.）意味非2.），所以這兩個版本都可以使用，但2.）往往會增加更多的復雜性。

對于無法糾正的故障，安全機制不會要求保留該功能，因此通常不會使用無法糾正的故障注入進行等效性檢查。只有在特殊情況下，即應排除特定無法糾正的故障對輸出子集的任何影響，配置并運行相應的等效性檢查才有意義。

特定的等效性檢查方法并非旨在取代成熟的順序等效性檢查器。盡管如此，對于檢查本地安全增強功能的實施，通過注入故障獲得最大的靈活性是有利的。此外，我們可以使用我們熟悉的形式化驗證環境，以及通用形式化屬性檢查的所有調試支持。由于分層警報減少架構，可以通過首先將等效性檢查限制在實例層次結構的較低級別，直至安裝保護邏輯的子組件來控制復雜性。

5. 經驗和結果

我們已將這套驗證自動化例程應用于不同的系統控制模塊，包括內存測試和控制單元、安全管理單元、系統寄存器單元、時鐘控制和復位控制單元的部分以及其他模塊，最大的模塊大約有40 k行VHDL代碼和1500個受保護的安全寄存器位。

本文總結的所有屬性的運行時間都是可以接受的：復位基本情況證明范圍從幾秒到21分鐘，步驟情況從幾分鐘到大約2小時。應該強調的是，在這些證明中，數千個寄存器位中的大量任意故障組合僅通過一個屬性來覆蓋，而無需指定故障位置和故障數量。在故障仿真中，不可能在有限的時間內實現故障場景的同比覆蓋率。

表1給出了較大系統控制模塊的驗證時間。

表1.典型系統控制模塊的證明結果

每個屬性都對應模塊所有安全寄存器位的一個同時證明。名為sff_0_* 的屬性假設沒有錯誤，名為sff_1_* 的屬性假設任意單個位有錯誤，名為sff_any_* 的屬性組甚至假設任意數量和組合的位同時翻轉。事實上，sff_any_* 屬性包含sff_1_* 屬性。因此，乍一看，sff_any_* 的時間并沒有明顯增加，這令人驚訝。

ECC邏輯的證明取決于受保護的代碼字長度。在這里，最長的屬性證明在具有10個ECC位的256位數據字中安全檢測任意組合的3位錯誤需要01:44:49小時。

由于證明是在具有數千個不同大小和動態加載的主機的LSF計算場中同時運行的，因此一個屬性的證明時間可能會有很大差異，具體取決于當前可用的資源。因此，從表1給出的證明時間可以推斷出的唯一可靠信息是，復合形式安全驗證非常高效，但在實際項目情況下產生的結果不能直接作為基準，這不是我們生產性驗證工作的目的。

故障注入屬性使我們能夠填補與測試警報生成相關的所有功能覆蓋空白。如果沒有故障注入，根本無法實現此功能。具有故障注入但零故障假設的屬性，比沒有故障檢測的常規模型的相應屬性運行時間長約30%。

基于屬性的等效性檢查沒有出現復雜性問題，因為每當添加新的寄存器保護時，我們都可以將它們本地應用于子組件。

驗證極大地受益于在驗證設計中實施的統一保護方法，這大大簡化了從設計中提取關鍵信息的自動程序。反過來，使用封裝安全邏輯進行安全增強使設計工程師能夠安全地在短時間內增強他們的設計。由于驗證程序自動生成宏并使用了預定義的安全屬性，因此立即發現了一些錯誤，這些錯誤涉及在警報減少中未包含單個本地警報，以及自檢控制器和連接的安全寄存器位的時鐘和復位域不一致。安裝時鐘門控以節省電量導致額外的復雜性，這需要在自檢激活和警報處理期間仔細分析時鐘門控條件。

6. 結論

一般來說，對于ISO 26262認證，提供安全機制已經過詳盡驗證的證據是非常有利的。這是應用形式化驗證的強大動機，尤其是對安全關鍵型C組件。定義明確的統一安全機制可節省大量的設計和驗證工作。此外，一旦該安全機制通過認證，重復使用實例的認證就會容易得多，理想情況下可以用理論取代重復的安全驗證。

在本演示中，我們展示了基于屬性的形式化安全驗證具有許多優勢。特別是，

- 能夠確認安全機制的100%診斷覆蓋率，這得益于形式化工具非常靈活的故障注入功能（通過設計變異，在本例中是在詳細模型中），而動態仿真中通常采用的強制波形值則不然。

- 通過同時覆蓋大量故障，效率極高。即使對于非常長的級聯寄存器向量，這種高性能也是通過扇入分析實現的。

- 允許在不引入功能缺陷的情況下進行后期安全或功能修改。

- 利用與形式驗證基礎設施并行開發的特別易于驗證的統一設計方法。這種統一性對設計有積極影響。由于安全功能的封裝，設計工程師不必關心安全機制的內部實現，從而節省了大量精力。反過來，通過觀察信號及其重復的簡單命名約定，設計工程師可以在插入預定義屬性的宏生成器和證明自動化功能中使用自動過濾功能。

我們針對安全增強設計的特定等效性檢查方法，并非旨在取代成熟的順序等效性檢查器。盡管如此，它提供了

- 由于容器生成器進行了靈活的層次化和本地化，并將等效性檢查限制在實例層次結構的較低級別，直至安裝了保護邏輯的子組件，因此具有很高的計算效率。

- 最高可靠性，與屬性集的完整性無關，將應用范圍擴展到通常不經過形式驗證的模塊。

- 廣泛的調試支持，具有屬性檢查環境提供的所有功能，這些功能在通用功能屬性檢查中眾所周知。

- 最大程度地靈活注入故障，這是標準等效性檢查器幾乎無法提供的。

鑒于工業MCU開發的緊張時間表和成本限制，我們既不能自己設計全新的形式驗證技術，也不能大規模試驗不熟悉的驗證工具并將其集成到我們的產品開發流程中，除非我們能獲得巨大的優勢，以至于熟悉、集成和適應、許可等方面的成本和額外努力是合理的。相反，我們在經常使用的形式驗證流程中開發自己的驗證自動化腳本。由于該工具環境一方面提供了非常高效的內部驗證算法以及豐富便捷的用戶功能，正如商業終端用戶產品所期望的那樣，另一方面又足夠開放，允許我們在自己的腳本中使用一整套預定義的實用功能，因此這種設置為我們提供了足夠的靈活性，可以使用與生產設計和形式驗證工作并行開發并直接由其驅動的定制解決方案來處理特定的驗證問題。

雖然在早期設計階段檢測安全機制的缺陷很重要，因為設計修正比產品流片后便宜得多，但未來的工作還將通過標準建議的形式安全驗證來解決門級問題，以確保綜合沒有刪除冗余邏輯。為此，我們希望重用在RTL級證明的安全屬性和驗證自動化功能，只需在門級進行少量調整即可。

詳詢“牛小喀”微信：NewCarRen

作者：?？W專欄作者
牛喀網文章，未經授權不得轉載！