形式驗(yàn)證最佳實(shí)踐之五：收尾和總結(jié)

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

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

正式覆蓋分類法

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

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

可達(dá)性覆蓋

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

靜態(tài)覆蓋率

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

可觀察性覆蓋

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

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

有界覆蓋率

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

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

誰擅長什么？

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

在時(shí)間/CPU 預(yù)算允許的情況下，可達(dá)性覆蓋率很好地說明了形式化工具分析設(shè)計(jì)的能力。如果覆蓋率不足，則意味著需要添加新的抽象概念。這種覆蓋率還能告訴你哪些代碼片段沒有被覆蓋，因?yàn)樗鼈兪撬赖模ㄔO(shè)計(jì)問題），或者因?yàn)榧s束條件阻止了覆蓋（形式化測(cè)試平臺(tái)問題）。

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

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

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

o_always_high: assert property(o)；

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

我們?cè)诟咚倬彺婵刂破魃细采w了哪些內(nèi)容？

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

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

可達(dá)性覆蓋率

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

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

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

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

多個(gè)命中斷言的覆蓋率

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

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

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

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

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

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

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

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

設(shè)定覆蓋率目標(biāo)（百分比數(shù)字）似乎不是一個(gè)好主意?？梢钥隙ǖ氖牵罱K會(huì)留下一些漏洞，這沒有問題，因?yàn)槠渌?yàn)證方法已經(jīng)覆蓋了這些漏洞。但你不知道這些漏洞的相對(duì)大小。

良好的實(shí)踐

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

總結(jié)

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

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

順序等價(jià)檢查是一種多用途工具。它可用于驗(yàn)證時(shí)鐘門、ECO、設(shè)計(jì)優(yōu)化等。在我們的高速緩存中，等價(jià)檢查被用來確保我們?cè)谕暾咚倬彺媾渲茫?a target="_blank">IDCache）上所做的所有工作在純數(shù)據(jù)配置（DCache）上都是有效的。為此，我們將 IDCache 與 DCache 進(jìn)行了比較，條件是任何請(qǐng)求都不得以指令部分為目標(biāo)。對(duì)于純指令配置也是如此。

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

以上這些額外的知識(shí)點(diǎn)為Codasip的驗(yàn)證系列第二季提供了大量素材，期待有機(jī)會(huì)再跟大家分享和探討。