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

重現(xiàn)死鎖漏洞

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

can_respond: assert property(s_eventually design_can_respond)；

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

resp_ev：assert(s_eventually W_HREADY)；

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

擁抱故障

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

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

fair_maint: assume property(s_eventually maintenance_module.is_last_index);

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

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

從一種故障到另一種故障

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

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

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

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

驗證RTL修復(fù)

我們已經(jīng)有了一個RT 修復(fù)方案，所以很快就可以嘗試......結(jié)果發(fā)現(xiàn)它并不完整！我們?nèi)匀挥龅搅藷o法擺脫的死鎖。在經(jīng)過幾次迭代后，情況有所改善，此類的故障也沒有再出現(xiàn)......但同時也沒有證據(jù)可以證明已經(jīng)徹底擺脫死鎖。

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

使用過度約束

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

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

其它死鎖檢測技術(shù)

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

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

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

如果出現(xiàn)了反例，就會產(chǎn)生一個以無限循環(huán)結(jié)束的跟蹤T，以防止 expr 再次為真。

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

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

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

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

使用有界斷言

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

使用進(jìn)度計數(shù)器

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

進(jìn)一步驗證死鎖的方式

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

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

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

故障再次出現(xiàn)

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

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

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

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

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

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

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

審核編輯：彭菁