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

重現(xiàn)死鎖漏洞

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

can_respond: assert property(s_eventually design_can_respond)；

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

resp_ev：assert(s_eventually W_HREADY)；

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

擁抱故障

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

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

fair_maint: assume property(s_eventually maintenance_module.is_last_index);

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

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

從一種故障到另一種故障

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

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

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

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

驗(yàn)證RTL修復(fù)

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

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

使用過度約束

在迭代調(diào)試過程中，我們使用了過度約束來減少探索。這可以大大減少獲得反例或證明所需的時(shí)間，并有助于調(diào)試故障，因?yàn)樯傻姆桨父唵?。?dāng)然，這些過度約束必須在最終運(yùn)行時(shí)去除。

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

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

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

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

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

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

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

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

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

證明有效性斷言在計(jì)算上比證明安全性斷言更困難。因此有時(shí)最好采用不同的方法來驗(yàn)證死鎖。

使用有界斷言

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

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

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

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

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

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

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

故障再次出現(xiàn)

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

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

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

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

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

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

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

審核編輯：彭菁