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

基本屬性

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

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

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

查找標(biāo)記方式

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

引入 CAM 組件

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

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

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

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

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

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

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

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

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

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

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

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

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

深度漏洞查找

有多種不同的查找方法，所有方法都是 "半正式 "的，這意味著它們并非詳盡無(wú)遺。但是它們?cè)诓檎夜收戏矫娣浅３錾?/p>

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

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

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

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

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

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

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

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

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

審核編輯：黃飛