在上一部分中，我們重點討論了在組件上設置形式驗證的最佳實踐。那么現在設置已經準備就緒，協議檢查器可以避免不切實際的情況（這也有助于發現一個新漏洞），基本抽象也可以提高性能。現在的任務便是如何處理重現使用仿真發現的死鎖漏洞？

重現死鎖漏洞

重現死鎖漏洞要確保設計無死鎖，其中一種方法是驗證它是否 "最終 "能夠響應請求。”最終“這個措辭很重要，無論當前狀態如何，也無論我們必須等待多少個周期，設計都必須在未來做出響應。而這可以很好地通過一種稱為 "有效性屬性 "的 SystemVerilog 斷言來實現：

can_respond: assert property(s_eventually design_can_respond)；

對于正在驗證的緩存，我們在Worker端口上定義了該屬性：

resp_ev：assert(s_eventually W_HREADY)；

由于 W_HREADY 在 Worker 接口上永遠保持 LOW 時也會出現死鎖 bug，因此我們認為這個斷言是最簡單、最通用的檢查方法。注：與安全屬性相比，有效性屬性的概念背后有很多理論依據。這里不需要討論這個問題與驗證有效性斷言的正式算法之間的差異，同時也不在本文的討論范圍之內。

擁抱故障

然而通過證明上述斷言，我們很快就敗下陣來。這促使了我們使用方法和工具的支持。當發現死鎖是 "可逃脫的"。換句話說，對失效計數器的抽象（見第 1 部分）使其永遠不會達到終值。在這種情況下緩存 "最終 "沒有響應，因為它永遠停留在無效循環中。這是一個可逃逸的死鎖，因為存在一個逃逸事件（計數器達到其終值，失效停止）。

這是一個錯誤的“故障”，我們最終放棄了這個“故障”，增加了一個 "公平性約束"：一個用作約束的有效性屬性。

fair_maint: assume property(s_eventually maintenance_module.is_last_index);

同樣，必須將管理器接口上的M_HREADY約束為 "始終最終 "為高。否則，緩存可能會永遠處于等待響應的狀態。這在下面的波形中可以看到。

在LOOP區域，如果管理器端口上的M_HREADY在請求飛行時也保持LOW，那么Worker端口上的W_HREADY可能會永遠保持LOW。這個LOOP區域可以無限大，但 Escape 區域表明，如果環境最終使管理器端口上的M_HREADY升高，那么它就會解除鎖定狀態，Worker端口上的相同信號也會升高。這就是 "逃逸事件"。

從一種故障到另一種故障

在修復了這些錯誤的“故障”后，我們又遇到了 resp_ev 斷言故障。

結果更有趣：它顯示為 "無法逃脫的死鎖"。這意味著我們不必再嘗試找出其他缺失的公平性約束。有一種狀態在于無論之后發生什么，設計都不會響應。

形式化工具顯示了一個在LOOP區以無限LOOP結束的波形。由于不存在任何逃逸事件，該區域總是向右無限延伸。

這時設計師們便可以確認 "這就是漏洞！"。最酷的是我們在不到一周的時間里，從零開始重現了這個故障。

驗證RTL修復

我們已經有了一個RT 修復方案，所以很快就可以嘗試......結果發現它并不完整！我們仍然遇到了無法擺脫的死鎖。在經過幾次迭代后，情況有所改善，此類的故障也沒有再出現......但同時也沒有證據可以證明已經徹底擺脫死鎖。

增加時間限制后，我們在 iCache 總線上得到了 resp_ev 斷言的完整證明（見實踐之一）。通過對dCache 總線上的瓶頸分析，發現它是由于標準緩存請求與 CSU 動態更改緩存配置請求的混合功能造成的。這使得狀態空間變得非常大。為了避免這種情況，我們對環境進行了限制從而使證明趨于一致。

使用過度約束

在迭代調試過程中，我們使用了過度約束來減少探索。這可以大大減少獲得反例或證明所需的時間，并有助于調試故障，因為生成的方案更簡單。當然，這些過度約束必須在最終運行時去除。

在正式設置中以簡單的方式允許過度約束是很重要的。為了安全起見，最好的做法是禁止在正式測試平臺中直接編寫約束條件（即假設屬性）。這樣做的風險太高，可能會在最后留下一些已啟用的屬性。相反，所有屬性都必須寫成斷言，有些屬性可以通過顯式運行選項轉換成約束。同時Codasip的形式框架允許我們這樣做。

其它死鎖檢測技術

在該系列的第一部分我們已經介紹了形式驗證工具如何區分可逃逸和不可逃逸的死鎖。然而并非所有工具都能提供這種功能，下面是一種模仿這種功能的技術：

以 s_eventually expr 的形式編寫一個有效性斷言A。

用工具來證明A。如果被證明就意味著大功告成：沒有死鎖。

如果出現了反例，就會產生一個以無限循環結束的跟蹤T，以防止 expr 再次為真。

運行A、WA的見證證明，使用T來初始化設計，而不是正常的重置序列。形式分析將從LOOP狀態開始。

如果證明的結果是WA不可達，則意味著T顯示了不可避免的死鎖。

如果WA被覆蓋，則意味著T是一個可逃逸的死鎖，并且WA的跟蹤顯示了該逃逸事件。

證明有效性斷言在計算上比證明安全性斷言更困難。因此有時最好采用不同的方法來驗證死鎖。

使用有界斷言

有一種方法是用有界斷言代替有效性斷言。可以寫成 !expr [*N] |=> expr 來代替 s_eventually expr。這意味著expr預計不會在超過N個LOOP的時間內為假。這種特性在仿真測試平臺中非常常見。難點在于將N設置得足夠大，但又不能太大！如果將N設置為數百或數千個周期，FV就不太可能得到結果。如果將N設得很小，可能會發生一些事件導致N太小，從而導致錯誤故障。因此在驗證有效性斷言時，所遇到的困難類似于尋找公平性約束，以摒棄所有可逃逸的死鎖。

使用進度計數器

另一種方法是使用進度計數器。首先必須定義一個計數器，每當設計中發生一些事情，例如更接近任務完成時，計數器就會遞增。然后安全斷言可以檢查并在必須取得進展的情況下取得進展。以緩存為例，我們可以將進度計數器定義為在一個管理器端口上發出請求時遞增。但一般來說，定義所有必須使計數器遞增的事件是很困難的。

進一步驗證死鎖的方式

在重現了目標錯誤并驗證了建議的 RTL 修正后，我們希望更進一步。我們了解到，只有在使用 "寫透 "高速緩存配置時才會出現該錯誤。因此，在完成上述工作時，我們限制只啟用這種配置。當然，我們還想確保在 "回寫 "配置中不會出現該問題，因此我們重復了上述過程，取消了這一限制。

然后，我們要驗證是否存在其他死鎖。這些死鎖不會出現在HREADY上，而是出現在設計的內部有限狀態機（FSM）上。事實上，死鎖可能出現在FSM永遠阻塞在某個特定狀態時，盡管HREADY并沒有像LOW那樣被阻塞。為此，我們確定了設計中的主要FSM，并生成了有效性斷言，檢查所有狀態是否最終都能達到。例如

fsm_dcache_miss: assert(s_eventually dcache.fsm_state == MISS)；

故障再次出現

我們很快就遇到了許多故障，而且都是可以逃脫的死鎖。

例如，如果Worker端口接收到對同一地址的連續請求流。第一個請求可能未命中，也可能命中。但接下來的請求都會命中。如果請求流 "足夠密集"，那么每次命中之間就不會有等待周期，因此FSM的狀態始終是 HIT，無法達到任何其他狀態，包括MISS。這就是上述斷言失敗的原因。

幸運的是，工具顯示該失敗是由于可逃逸的死鎖造成的。逃脫的方法是在請求流中騰出一些空間，或者更改地址。為了掩蓋這種情況，我們需要添加公平性約束。但它們似乎限制過多，大大縮小了驗證范圍。

我們最終決定不這么做。相反，我們讓工具在不同的配置下運行了幾天（這對正式版來說是很長的時間！）。它報告了許多我們忽略的可逃脫死鎖，但沒有發現無法逃脫的死鎖，至此，這些收獲即使沒有得到完整的證明，但也大大增強了我們的信心。

在本次的死鎖漏洞調查案中，我們探討了驗證死鎖的形式化最佳實踐。以下是三個主要收獲：

在本次的死鎖漏洞調查案中，我們探討了驗證死鎖的形式化最佳實踐。以下是三個主要收獲。

通過故障重現和RTL修復驗證，大大提高了我們對形式化驗證的信心，相信并沒有其他真正的死鎖存在。當然Codasip并沒有就此止步，作為專業的bug獵人，在下一集中，將為大家介紹Codasip如何驗證設計的其他方面，包括高級屬性等。敬請期待！

審核編輯：彭菁