形式化驗(yàn)證最佳實(shí)踐之三：實(shí)現(xiàn)端到端屬性

在本系列的前兩集中，我們看到了如何為高速緩存建立一個(gè)高效的正式測試平臺，如何發(fā)現(xiàn)一個(gè)真正的漏洞以及如何重現(xiàn)一個(gè)死鎖漏洞和找到一個(gè)設(shè)計(jì)修復(fù)方法。在這一點(diǎn)上，我們確信不存在其死鎖漏洞。本集將介紹我們?nèi)绾悟?yàn)證強(qiáng)大的斷言，怎么準(zhǔn)備正式測試平臺以驗(yàn)證端到端屬性（端到端屬性將根據(jù) DUT 的輸入檢查 DUT 的輸出），以及新的最佳實(shí)踐。

基本屬性

實(shí)際上，讓我們從一個(gè)不是端到端但對高速緩存至關(guān)重要的屬性開始。該屬性是我們唯一需要檢查內(nèi)部細(xì)節(jié)的屬性。它可以驗(yàn)證緩存中的命中請求是否只有一種命中方式。如果不遵守這一點(diǎn)，那么在讀取或?qū)懭肽姆N數(shù)據(jù)時(shí)就會非常模糊。

hit_onehot: assert property(i_ucache.i_hit_stage.is_hit |-> $onehot(i_ucache.i_hit_stage.hit_way);

在緩存中執(zhí)行查找時(shí)，地址會被分割成一個(gè)標(biāo)記（下圖中為 123）、一個(gè)索引（1）和一個(gè)偏移量。索引用于尋址標(biāo)記方式。如果該索引的內(nèi)容有效，而標(biāo)簽在兩種方式（下圖中的 0 和 2）中相同，這就是 "多重命中"，也是一個(gè)嚴(yán)重的問題。許多潛在的設(shè)計(jì)錯(cuò)誤都可以看作是對這一屬性的違反。

查找標(biāo)記方式

然而，要摒棄對這一斷言的錯(cuò)誤失效，需要幾個(gè)約束條件。如第一集所述，我們抽象了不同的 RAM 陣列，包括 tagram。這意味著緩存讀取 tagram 的結(jié)果是 "隨機(jī) "的。這一點(diǎn)都不好，會導(dǎo)致斷言很快失敗。

引入 CAM 組件

這就是內(nèi)容可尋址內(nèi)存（CAM）發(fā)揮作用的地方。CAM 是內(nèi)存的縮小版。它不能容納數(shù)千個(gè)單元（每個(gè)地址一個(gè)單元），而只能容納少數(shù)幾個(gè)選定的地址，但這些地址不受任何限制。這實(shí)際上是某種固定長度的關(guān)聯(lián)數(shù)組，其長度遠(yuǎn)遠(yuǎn)小于實(shí)際數(shù)組的大小。

下圖左邊顯示的是一個(gè)真實(shí)的 tagram，右邊顯示的是一個(gè) CAM 抽象。

我們可以看到，真實(shí)標(biāo)記圖在索引 2 處包含一個(gè)有效標(biāo)記。但在 CAM 中卻沒有。為了避免因緩存讀取索引 2 而導(dǎo)致錯(cuò)誤失敗，我們只需限制所有讀?。ê蛯懭耄┒急仨氃?CAM 中存在的索引處進(jìn)行：

request_in_cam: assume property(request |-> there_exists_one_in_cam(req_index))；

這是一個(gè)很強(qiáng)的過約束，我們可以通過正確調(diào)整 CAM 的大小來緩解這個(gè)問題。為此，我們定義了覆蓋屬性，以確定使用了多少個(gè)不同的索引。通過對這些屬性的證明，我們可以確定哪些 CAM 大小過大，無法充分利用，因?yàn)樾问椒治鰰兊眠^于復(fù)雜。我們通常使用 FV 無法充分利用的最小 CAM 大小。

我們使用一個(gè) CAM 實(shí)例數(shù)組來表示所有標(biāo)簽陣列。此外，使用 CAM 可以抽象出緩存的初始內(nèi)容。我們只需讓數(shù)組中的值不受限制即可。事實(shí)上，并非完全無約束！hit_onehot 斷言仍然會在一個(gè)簡單的情況下失效：讀取請求進(jìn)來后，會以兩種方式命中，因?yàn)槊總€(gè) CAM 的初始狀態(tài)允許在同一索引中有兩種方式擁有相同的有效標(biāo)記。我們需要添加僅適用于復(fù)位后第一個(gè)周期的約束：

這給形式分析增加了很多復(fù)雜性，所以只有在需要時(shí)才使用這些約束。不幸的是，我們還沒有完成 hit_onehot 斷言，還需要使用 CAM 內(nèi)容的新約束：

對于 CAM 中已經(jīng)存在的地址，高速緩存不得收到 "非高速緩存 "請求。

我們還需要用 CAM 為 dirtyram 陣列建模，并使標(biāo)簽和 dirty CAM 的內(nèi)容保持一致（即 dirty 行必須有效）。

CAM 中的地址必須在內(nèi)存映射寄存器范圍之外。

其中一些約束用于確保 CAM 的初始內(nèi)容正確無誤。我們還可以使用非常類似的屬性作為斷言來檢查任何循環(huán)。只需刪除 "init_cycle "項(xiàng)即可：

對死循環(huán)狀態(tài)存有敬意！

正如前面提到的，我們需要限制到達(dá) tagram（實(shí)際上是 CAM）的請求，使它們只針對 CAM 中存在的索引。這有一個(gè)隱藏的缺點(diǎn)。為了說明這一點(diǎn)，讓我先總結(jié)一下什么是 FV 中的 "深度錯(cuò)誤查找"。

深度漏洞查找

有多種不同的查找方法，所有方法都是 "半正式 "的，這意味著它們并非詳盡無遺。但是它們在查找故障方面非常出色。

除了從復(fù)位狀態(tài)開始進(jìn)行形式分析外，主要技術(shù)還使用軌跡末端來啟動形式分析。首先根據(jù)用戶定義的覆蓋屬性或自動生成的覆蓋屬性生成軌跡。然后，從這一跟蹤的最后一個(gè)周期（或最后幾個(gè)周期）開始，執(zhí)行另一項(xiàng)形式分析，找到其他跟蹤，用于啟動其他形式分析等。它們也可能會發(fā)現(xiàn)錯(cuò)誤。這種方法能夠發(fā)現(xiàn)需要大量循環(huán)才能出現(xiàn)的錯(cuò)誤，而標(biāo)準(zhǔn)（窮舉）FV 是無法發(fā)現(xiàn)這些錯(cuò)誤的。

下面以窮舉式 FV 為例進(jìn)行說明：窮舉式 FV 僅從重置狀態(tài)開始探索，在探索了所有狀態(tài)直至幾個(gè)周期后就達(dá)到了極限。相反，深度錯(cuò)誤查找從復(fù)位狀態(tài)開始探索，但也會探索一些其他狀態(tài)（綠色），并且可以深入設(shè)計(jì)，可能會發(fā)現(xiàn)錯(cuò)誤狀態(tài)（紅色），但也會遺漏一些狀態(tài)（灰色）。

在深度錯(cuò)誤查找中，當(dāng)從跟蹤結(jié)束處開始新的形式分析時(shí)，跟蹤前綴會被凍結(jié)。我們所說的 "死循環(huán)狀態(tài) "是指由于某些約束條件在其后適用，因此無法進(jìn)入下一個(gè)狀態(tài)。死端狀態(tài)越多，深度錯(cuò)誤查找的效率就越低。

如何消除死鎖狀態(tài)

假設(shè)高速緩存接收到一個(gè)地址 A 的請求。然后，該請求觸發(fā)了對 CAM 的訪問，訪問的索引 I 取決于 A。針對 A 的請求本應(yīng)在幾個(gè)周期前就避免。

遵循這個(gè)簡單的規(guī)則可以大大緩解死鎖狀態(tài)問題：盡快對事物進(jìn)行約束。在本例中，它包括對高速緩存輸入端的地址進(jìn)行限制，這樣對于可緩存請求，只有在 CAM 中匹配地址的請求才會被發(fā)出。

為 tagram 和 dirtyram 添加 CAM 以及相關(guān)限制并不容易。只有在調(diào)試重要斷言（如 hit_onehot 斷言）失敗時(shí)，才能逐步添加抽象和約束。不過，這也是一種投資。你會看到，我們在緩存驗(yàn)證的其余部分中都使用了它。最后，我們沒有發(fā)現(xiàn)任何關(guān)于 hit_onehot 的失敗，但即使過了很長時(shí)間，也沒有得到任何證明。這并不奇怪，因?yàn)檫@個(gè)斷言幾乎驗(yàn)證了設(shè)計(jì)的全部控制（在分析覆蓋率時(shí)可以看到......在下一集中）。然而，手動添加一些令人討厭的錯(cuò)誤，很快就會被視為該斷言的失敗，這是一個(gè)好兆頭。

關(guān)于這次的收獲可以來回顧一下。

我們已經(jīng)看到了如何大大增強(qiáng)（或復(fù)雜化?。┪覀兊恼綔y試平臺。這需要驗(yàn)證一個(gè)基本的控制斷言，之后還需要驗(yàn)證數(shù)據(jù)完整性斷言。以下是我們確定的最佳實(shí)踐。

審核編輯：黃飛