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

基本屬性

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

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

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

查找標記方式

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

引入 CAM 組件

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

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

我們可以看到，真實標記圖在索引 2 處包含一個有效標記。但在 CAM 中卻沒有。為了避免因緩存讀取索引 2 而導致錯誤失敗，我們只需限制所有讀?。ê蛯懭耄┒急仨氃?CAM 中存在的索引處進行：

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

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

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

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

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

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

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

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

對死循環狀態存有敬意！

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

深度漏洞查找

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

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

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

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

如何消除死鎖狀態

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

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

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

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

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

審核編輯：黃飛