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

基本屬性

實際上，讓我們從一個不是端到端但對高速緩存至關重要的屬性開始。該屬性是我們唯一需要檢查內部細節(jié)的屬性。它可以驗證緩存中的命中請求是否只有一種命中方式。如果不遵守這一點，那么在讀取或寫入哪種數(shù)據(jù)時就會非常模糊。

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

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

查找標記方式

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

引入 CAM 組件

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

下圖左邊顯示的是一個真實的 tagram，右邊顯示的是一個 CAM 抽象。

我們可以看到，真實標記圖在索引 2 處包含一個有效標記。但在 CAM 中卻沒有。為了避免因緩存讀取索引 2 而導致錯誤失敗，我們只需限制所有讀取（和寫入）都必須在 CAM 中存在的索引處進行：

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

這是一個很強的過約束，我們可以通過正確調整 CAM 的大小來緩解這個問題。為此，我們定義了覆蓋屬性，以確定使用了多少個不同的索引。通過對這些屬性的證明，我們可以確定哪些 CAM 大小過大，無法充分利用，因為形式分析會變得過于復雜。我們通常使用 FV 無法充分利用的最小 CAM 大小。

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

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

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

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

CAM 中的地址必須在內存映射寄存器范圍之外。

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

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

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

深度漏洞查找

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

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

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

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

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

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

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

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

關于這次的收獲可以來回顧一下。

我們已經看到了如何大大增強（或復雜化！）我們的正式測試平臺。這需要驗證一個基本的控制斷言，之后還需要驗證數(shù)據(jù)完整性斷言。以下是我們確定的最佳實踐。

審核編輯：黃飛