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

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

正式覆蓋分類法

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

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

可達性覆蓋

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

靜態覆蓋率

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

可觀察性覆蓋

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

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

有界覆蓋率

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

現在，讓我們更詳細地了解前三種覆蓋類型。

誰擅長什么？

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

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

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

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

例如，下面藍色氣泡中的邏輯非常龐大和復雜。斷言寫成

o_always_high: assert property(o)；

這個斷言很容易證明。可以靜態覆蓋整個邏輯氣泡。但可觀察性覆蓋范圍實際上只包括所示的邏輯：3 個觸發器和 2 個門。其余邏輯與證明該屬性無關。

我們在高速緩存控制器上覆蓋了哪些內容？

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

現在，讓我們看看覆蓋率如何。

可達性覆蓋率

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

使用 AHB 協議檢查器的覆蓋率

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

但從可觀察性覆蓋率來看，其覆蓋率相當低。事實上，協議斷言非常 "本地化"，只需要靠近頂層接口的邏輯。例如，處理查找、命中/未命中計算、觸發補線和驅逐的邏輯在這里就沒有涉及。這并不奇怪。

多個命中斷言的覆蓋率

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

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

數據完整性斷言覆蓋

我們添加了端到端斷言，以驗證數據完整性。同樣，靜態覆蓋率保持不變。可觀察性覆蓋率略有增加。通過觀察差異，我們可以發現數據傳輸的邏輯已被覆蓋。

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

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

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

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

設定覆蓋率目標（百分比數字）似乎不是一個好主意。可以肯定的是，最終會留下一些漏洞，這沒有問題，因為其他驗證方法已經覆蓋了這些漏洞。但你不知道這些漏洞的相對大小。

良好的實踐

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

總結

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

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

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

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

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