這是形式驗證最佳實踐系列的最后一集。作為最后一步，讓我們來討論一下正式驗證和總結(jié)。在使用形式驗證驗證高速緩存控制器之后，我們的成果超出了預(yù)期。我們重現(xiàn)并驗證了已知死鎖的設(shè)計修復(fù)。我們還驗證了數(shù)據(jù)完整性和協(xié)議合規(guī)性。但是，我們在做這些工作時并沒有考慮高速緩存微體系結(jié)構(gòu)，因此我們沒有任何嵌入式斷言。

現(xiàn)在的問題是：我們完成了嗎？這樣的驗證是否足夠？通過一些小技巧，我們能夠獲得了證明，但我們是否觀察到了所有可能的漏洞？我們通常可以通過形式覆蓋來回答這些問題。

正式覆蓋分類法

在收集覆蓋率之前，我們首先需要定義我們想要觀察的內(nèi)容。與模擬中的代碼覆蓋類似，正式覆蓋可以觀察分支、語句、條件和表達(dá)式。它還可以觀察功能覆蓋所定義的覆蓋點。所有這些都被稱為 "覆蓋項"（CI）。在實踐中，我們發(fā)現(xiàn)如果存在分支、語句和覆蓋點，選擇它們就足夠有用了。

實際上，正式覆蓋有不同的類型。讓我們來看看它們。

可達(dá)性覆蓋

這需要進(jìn)行正式分析，以確定每個 CI 是否可以覆蓋。這與在模擬中測量代碼覆蓋率非常相似。它完全獨立于斷言。

靜態(tài)覆蓋率

靜態(tài)覆蓋也稱為 "影響范圍"（COI）覆蓋。它不需要運行任何形式分析。如果每個 CI 至少出現(xiàn)在一個斷言的 COI 中，則標(biāo)記為已覆蓋。

可觀察性覆蓋

這需要對斷言進(jìn)行形式分析。在分析過程中，證明引擎會報告對完成證明至關(guān)重要的 CI。

此時我們需要注意的是，有界證明也有助于提高覆蓋率。突變覆蓋率是一個非常相似的指標(biāo)，但使用的是不同的技術(shù)。它不能很好地擴展形式覆蓋率。

有界覆蓋率

如果某些斷言未被窮舉證明，則將證明約束與 COI 中 CI 的約束（通過可達(dá)性覆蓋率獲得）進(jìn)行比較。

現(xiàn)在，讓我們更詳細(xì)地了解前三種覆蓋類型。

誰擅長什么？

下表顯示了每種覆蓋都能檢測到哪些問題，括號中標(biāo)出了主要問題。

在時間/CPU 預(yù)算允許的情況下，可達(dá)性覆蓋率很好地說明了形式化工具分析設(shè)計的能力。如果覆蓋率不足，則意味著需要添加新的抽象概念。這種覆蓋率還能告訴你哪些代碼片段沒有被覆蓋，因為它們是死的（設(shè)計問題），或者因為約束條件阻止了覆蓋（形式化測試平臺問題）。

靜態(tài)覆蓋可以讓你快速了解設(shè)計中哪些部分肯定沒有被任何斷言檢查。如果必須對這些部分進(jìn)行形式驗證，則需要添加新的斷言。由于設(shè)計的性質(zhì)，這種覆蓋率通常很高，而且很容易實現(xiàn)。但這并不能讓您滿意！

可觀察性覆蓋率，也稱為 "證明覆蓋率"，可能是最重要的覆蓋率。它總是靜態(tài)覆蓋的一個子集。事實上，某些邏輯可能在特定斷言的 COI 中，但實際上并不在該斷言的可觀察性覆蓋范圍內(nèi)。這意味著，只看靜態(tài)覆蓋而不看可觀測性覆蓋是一種過度樂觀主義，也是一個巨大的錯誤！

例如，下面藍(lán)色氣泡中的邏輯非常龐大和復(fù)雜。斷言寫成

o_always_high: assert property(o)；

這個斷言很容易證明?？梢造o態(tài)覆蓋整個邏輯氣泡。但可觀察性覆蓋范圍實際上只包括所示的邏輯：3 個觸發(fā)器和 2 個門。其余邏輯與證明該屬性無關(guān)。

我們在高速緩存控制器上覆蓋了哪些內(nèi)容？

讓我們分三步來考慮高速緩存的驗證，由于死鎖驗證非常特殊，我們將其分開。首先，我們驗證了頂層接口是否符合 AHB 規(guī)范。然后，我們驗證了一個關(guān)鍵斷言，檢查是否發(fā)生多重命中。最后，我們驗證了數(shù)據(jù)完整性。

現(xiàn)在，讓我們看看覆蓋率如何。

可達(dá)性覆蓋率

我們首先測量了可達(dá)性覆蓋率，因為它與斷言無關(guān)。在這個相對較小的設(shè)計中，覆蓋率非常高。漏洞只是一些死代碼。如果我們移除抽象，尤其是無效計數(shù)器上的抽象，覆蓋率就會下降，從而證實了這些抽象的有用性。

使用 AHB 協(xié)議檢查器的覆蓋率

在添加協(xié)議檢查器驗證 AHB 合規(guī)性后，靜態(tài)覆蓋率已經(jīng)非常高了。事實上，一個斷言，例如在等待確認(rèn)時檢查數(shù)據(jù)總線的穩(wěn)定性，其 COI 中幾乎包含了整個設(shè)計。即使是與維護(hù)操作相關(guān)的邏輯（我們知道任何斷言都無法直接驗證），也被涵蓋在內(nèi)。這一指標(biāo)中唯一的漏洞出現(xiàn)在事件計數(shù)器上。

但從可觀察性覆蓋率來看，其覆蓋率相當(dāng)?shù)汀Ｊ聦嵣?，協(xié)議斷言非常 "本地化"，只需要靠近頂層接口的邏輯。例如，處理查找、命中/未命中計算、觸發(fā)補線和驅(qū)逐的邏輯在這里就沒有涉及。這并不奇怪。

多個命中斷言的覆蓋率

在添加了檢查是否存在多重命中的斷言后，我們再次測量了覆蓋率。靜態(tài)覆蓋率保持不變。幾乎已經(jīng)達(dá)到最大值。

然而，可觀察性覆蓋率顯著增加，尤其是在控制主導(dǎo)的代碼塊上。這是因為僅斷言一項就需要驗證大量邏輯。這些邏輯在上一步中沒有涉及。但仍存在一些漏洞：事件計數(shù)器以及處理數(shù)據(jù)傳輸?shù)皆O(shè)計中的邏輯（雖然規(guī)模不大，但卻是必不可少的）仍未涵蓋。這些邏輯包括一些多路復(fù)用器和緩沖器，用于保存數(shù)據(jù)并在不同位置之間傳播。

數(shù)據(jù)完整性斷言覆蓋

我們添加了端到端斷言，以驗證數(shù)據(jù)完整性。同樣，靜態(tài)覆蓋率保持不變。可觀察性覆蓋率略有增加。通過觀察差異，我們可以發(fā)現(xiàn)數(shù)據(jù)傳輸?shù)倪壿嬕驯桓采w。

唯一的漏洞還是關(guān)于事件計數(shù)器。這很容易解釋：根本沒有關(guān)于這些計數(shù)器的斷言。而且，除了在外部提供其值外，設(shè)計內(nèi)部并沒有使用它們。使用斷言和形式來驗證這一點可能不是一個好主意。這需要對命中、未命中、驅(qū)逐等條件進(jìn)行繁瑣的建模。這最好使用仿真測試平臺來完成。

您可以構(gòu)建一個 "覆蓋率熱圖"，并在添加新屬性、抽象或約束時對其進(jìn)行更新。對于我們的高速緩存，在我們考慮的三個步驟中，代表可觀察性覆蓋范圍的熱圖如下所示。綠色區(qū)域已覆蓋，紅色區(qū)域未覆蓋。

截止到目前，驗證任務(wù)正式完成了嗎？對于這次緩存驗證來說，可以肯定地說 "是的"。覆蓋率指標(biāo)顯示，我們打算驗證的內(nèi)容確實已經(jīng)驗證。剩下的部分則更適合基于仿真的驗證。

為形式化定義目標(biāo)，并用不同的覆蓋率指標(biāo)來衡量它們，這是件好事。附加值其實不在于數(shù)字，而在于檢測到的漏洞。你必須仔細(xì)觀察這些漏洞，并了解它們是否在預(yù)料之中。如果不是，就改進(jìn)你的正式測試平臺，添加新的斷言等。如果它們是預(yù)料之中的，你就必須采用一種或多種其他驗證技術(shù)來解決它們。

設(shè)定覆蓋率目標(biāo)（百分比數(shù)字）似乎不是一個好主意?？梢钥隙ǖ氖?，最終會留下一些漏洞，這沒有問題，因為其他驗證方法已經(jīng)覆蓋了這些漏洞。但你不知道這些漏洞的相對大小。

良好的實踐

在最后一集中，我們探討了如何確保在形式化方面做得足夠好。以下是一些收獲供大家參考。

總結(jié)

至此希望大家喜歡Codasip所分享的形式驗證最佳實踐系列。還有一些其他的形式化技術(shù)并沒有在這個系列中提到，但它們也非常有用。

例如，X-傳播驗證可以告訴您是否存在僅在門級，甚至僅在硅片上可見的漏洞風(fēng)險。這些漏洞尤其難以通過仿真發(fā)現(xiàn)。

順序等價檢查是一種多用途工具。它可用于驗證時鐘門、ECO、設(shè)計優(yōu)化等。在我們的高速緩存中，等價檢查被用來確保我們在完整高速緩存配置（IDCache）上所做的所有工作在純數(shù)據(jù)配置（DCache）上都是有效的。為此，我們將 IDCache 與 DCache 進(jìn)行了比較，條件是任何請求都不得以指令部分為目標(biāo)。對于純指令配置也是如此。

安全特性也可以通過形式來驗證。例如，對于緩存來說，這意味著作為安全請求寫入的數(shù)據(jù)永遠(yuǎn)不會作為非安全請求的一部分從緩存中流出。側(cè)信道攻擊的漏洞也可以用形式來驗證。

以上這些額外的知識點為Codasip的驗證系列第二季提供了大量素材，期待有機會再跟大家分享和探討。