利用形式驗證找到更多‘Bug’

作者 : Mark Eslinger, Ping Yeung

本文介紹在形式驗證過程中找到最佳「釣魚點」的方法。這種所謂的「河釣法」(river fishing)並不是從一種初始狀態開始形式驗證,而是在功能模擬軌跡中找到有價值的「釣魚點」,開始進行形式驗證…

經常有這樣的事情發生,有些人總可以釣到很多魚,而其他人卻沒有這樣好的「運氣」。在很大程度上,這是因為那些厲害的釣手們知道最佳的釣魚點。他們知道魚兒一般都藏在哪裡,於是就會在那裡放線。

同樣地,驗證的方法也可以引導我們找到合適的「釣魚點」,顯著增加我們捕獲‘bug’的數量。

本文提出一種利用功能模擬活動的方法,從模擬軌跡中找到有價值的「釣魚點」,進行形式驗證。我們稱這種方法為「河釣法」(river fishing),但它並不是從一種初始狀態開始形式驗證,而是從功能模擬軌跡中挑選出一些可疑的點,然後從這些「釣魚點」開始形式驗證。

這種「河釣法」包含三個主要步驟:

  • 從模擬軌跡中辨識並提取出一組合適的「釣魚點」。
  • 根據形式驗證引擎執行狀況篩選並確定這些釣魚點的優先級。
  • 在運算伺服器上啓動並監測多個形式驗證的執行。

本文分享了我們最常用的釣魚點,這在許多設計都可以找到;文中並解釋如何使用形式驗證引擎來確定優先級、引導尋找bug的過程,從而在形式回歸環境中提高驗證結果的品質。

開始釣魚吧!

在河釣技術中,我們並不是從一種初始狀態開始形式驗證,而是從功能模擬軌跡中挑選出一些可疑的點,然後從這些點開始進行形式驗證。如果功能模擬已經進行了一些與目標有關的可疑活動,那麼就可以再找到其它一些不錯的釣魚點。此外,如果某些目標要求特定的前提條件,則可以利用不同的功能測試,為這些特定目標確定不同的釣魚點。

實際上,河釣法利用了功能模擬已經在執行的任務,以檢查那些盡可能接近最終目標的可疑初始狀態,如圖1所示。

圖1:從一些可疑的釣魚點啓動形式驗證。(來源:Mentor)

在以下章節中,我們將詳細描述利用河釣法尋找‘bug’的三項主要步驟(如圖2所示):辨識釣魚點、引擎狀態篩查,以及併發形式驗證執行。

圖2:使用河釣法進行形式驗證。(來源:Mentor)

尋找最佳釣魚點

專業釣手們都知道,最佳釣魚地點都位於河流中一些有著不尋常活動的特殊區域。從模擬軌跡中挑出值得關注的點進行形式驗證也與之相似。

圖3:找到值得關注的釣魚點。(來源:Mentor)

這裡介紹一個快速且全面的兩階層法,用於挑選出值得關注的釣魚點。該方法的主要標準包括:

  • 介面互動:模組間通訊和標準協議介面。
  • 控制和中斷:包括FSM、匯流排控制器、記憶體控制器、流程圖、演算法控制等。
  • 併發事件:包括設計中的仲裁器、排程器、開關、多工邏輯等。
  • 反饋、循環和計數:包括FIFO、定時器、計數器等,用於處理設計中的資料傳輸、突發和運算。
  • 用戶自定義斷言和覆蓋屬性。次要標準與主要標準的納入或排除有關。
  • 納入標準:在收集主要釣魚點時,應該標記價值較高的點,例如滿足多個標準的狀態、變化頻率較低的狀態,以及出現新活動的狀態等。
  • 排除標準:同時,要過濾掉價值不高的釣魚點,例如重覆的狀態、導致錯誤結果的異常狀態,以及上電、重設、初始化或配置序列期間的狀態等。

選擇最佳釣魚點

形式驗證不同於模擬。模擬執行是可預測且可完成的。而當針對大量的斷言進行形式驗證時,很難預測何時以及是否會完成。因此,瞭解形式驗證引擎的執行狀況,並利用它來衡量形式驗證取得的進展非常重要。

引擎執行狀況可用於衡量透過形式驗證取得的進展。同時,形式驗證引擎狀態是一個矩陣,可用於估計、確定優先級並監測形式驗證執行。利用形式驗證引擎狀態,我們可以評估釣魚點的成果,篩選出低品質的點,並對其餘點進行優先排序以進行形式驗證。在隨後的形式驗證執行期間,必須持續監控形式引擎狀態,以便盡早終止那些無效的執行,節省資源來執行新的形式驗證。

我們可以用一組參數來定義形式驗證引擎執行狀況:

  • 達成的形式驗證目標——已證明/被終止/被發現/無法發現(proven/fired/covered/uncoverable)。
  • 探索的序列深度或分析的影響錐(cone of influence)。
  • 獲取的形式驗證知識和引擎設定。

達成的目標和探索的序列深度是兩項完善的指標,已經普遍用於確定形式驗證的總體執行進度。

另一方面,如果想瞭解形式驗證在單項屬性或目標上的表現,就必須更深入地研究影響錐以及透過這些目標獲取的形式驗證知識。影響錐提供了關於每個目標探查深度的更多資訊,以及扇入(fan-in)邏輯及其對於目標依賴性的資訊。影響錐突顯出扇入邏輯中的「絆腳石」,形式驗證將會在此發生中斷,因而必須花費較多的時間進行分析,找出這些難解的設計元素,用戶也可以決定是否必須介入干預。有效分析並解決「絆腳石」的方法包括:添加切點、抽象出設計元素,或是啓用某些特殊引擎。

一直以來,形式驗證引擎狀態被用於監測運算密集型的形式驗證執行。直到最近,我們才意識到它也可以是篩選釣魚點的好方法。由於要在有限的運算資源(和授權)上執行大量形式驗證,我們發現經常需要不斷地終止執行那些可能徒勞無功的釣魚點。形式驗證引擎狀態參數可以用於確定運算伺服器是否被分配來徹底探測這些釣魚點。

圖4:採用引擎狀態來篩檢釣魚點。(來源:Mentor)

放置多條釣魚線

有了釣魚點優先級列表,就可以在伺服器叢集環境中同時啓動大規模形式驗證測試了。主伺服器將管理並監測所有形式驗證過程,持續不斷地從每個形式驗證執行中收集形式驗證引擎的狀態參數。圖5擷取到一個形式驗證執行開始時的目標分佈,用戶可以由此知道已經取得的進展。最初,33個目標中的大多數都是不確定的 ,即‘inconclusive’(I)。在多核心併發的情況下,形式驗證逐漸驗證目標,並將其劃分為以下幾個類別之一:firing (F)、vacuous (V)、uncoverable (U)、covered (C)和proof (P)。

圖5:形式驗證目標通過驗證或滿足目標的快照。(來源:Mentor)

一款全面的形式驗證工具擁有一組形式化引擎,可用於處理不同結構的設計。隨著形式驗證的執行,用戶可以檢查引擎的狀態,瞭解哪些引擎可以得出結果,而哪些引擎可能不會有收穫。如果某個引擎對於當前的任何結果都不會有貢獻,就可以將該引擎替換掉以節省資源,並將其它引擎集中在當前任務上。圖6是一個分佈式形式驗證執行期間的引擎快照。

圖6:形式驗證引擎知識庫快照。(來源:Mentor)

‘Proven/Unsatisfiable’列顯示了哪些引擎可解決安全性、使用壽命、空白以及涵蓋類型檢查。‘Fired/Satisfied’列顯示哪些引擎產生了反例。引擎7在查找大量證據和終止(firing)方面貢獻很大。引擎0 (管家引擎)和引擎10也找到了一些證據。另一方面,引擎12和17 (針對某些難題設計)雖然也致力於解決問題,但並沒有什麼產出。‘Inconclusive Targets’列(Good, Fair, Poor)則顯示工作中(WIP)目標的單個引擎狀態。引擎12正在研究75個健康狀況良好的目標,也就是說進展順利,只有三個目標狀況中等和不良。同樣地,引擎10在51個屬性上執行情況良好,但在其它更多目標上的執行無效。

釣魚收穫如何?

在以下案例中,我們捕獲了兩種代表性的‘bug’情況。而且只有在我們從模擬軌跡深處的釣魚點開始形式驗證之後,才可能成功捕獲。形式驗證引擎狀態篩檢也被用來清除許多不成功的驗證執行,這在開始或驗證過程中都可能發生。

圖7:比率同步資料傳輸介面。(來源:Mentor)

案例一:為了節省能耗,當今的設計中都採用了許多比率同步時脈,盡可能緩慢地執行每個元件。因此,比率同步介面很常見。當資料有效條件確定時,這些介面中的快速時脈域被設計為在慢時脈週期結束時對資料進行採樣。然而,在某些特殊情形下(設計團隊最初不知道),即使未聲明有效條件,資料也會被採樣。結果,損壞的資料被註冊並在系統內傳遞。根據兩個介面、計數器和控制邏輯上的活動,就可以確定釣魚點。在初始化設計之後,以及兩個介面之間的資料經過數百個週期的正確傳輸之後,即可挑選出幾個釣魚點。形式驗證有助於揭示兩個介面之間的不完整交握訊息——這種不完整的交握導致資料採樣無效。

案例二:在此資料傳輸控制器中,設置了動態傳輸通道以處理具有不同優先級的資料封包。 在這種情況下,當多個通道同時完成傳輸時,一組位址指標將被解除分配兩次,而另一組位址指標卻未被解除分配,從而導致記憶體洩漏和資料損壞。根據併發事件、計數器和複雜控制邏輯的活動,就可以確定釣魚點。在這種類型的設計中,形式驗證很難設定這些資料傳輸,但它們很容易在模擬回歸中取得。形式驗證利用了模擬執行深處的多個釣魚點,並根據引擎狀態對其進行優先排序,因而能夠暴露通道去分配邏輯中的弱點,並同步兩個通道以同時完成資料傳輸。

圖8:資料傳輸控制器。(來源:Mentor)

河釣技術

河釣技術利用了功能模擬活動,從模擬軌跡中找到可疑的釣魚點開始形式驗證。要找到一組合適釣魚點的標準有很多,包括介面互動、控制和中斷、併發事件、反饋循環和計數、用戶自定義斷言以及涵蓋的屬性等。然後,根據形式驗證引擎狀態對這些釣魚點進行篩選和優先級排序,可以被定義為:已證明或已摒棄的驗證目標、已探查的序列深度,以及所獲取的形式驗證知識庫。之後,當集中式資料庫將所有結果匯整在一起時,使用一組釣魚點來初始化多個形式驗證執行。根據得出的結果以及所發現的複雜‘bug’,我們將會發現,在形式驗證回歸環境中,河釣技術確實有助於提高驗證結果的品質。

— 本文作者:

  • Mark Eslinger, Mentor IC驗證系統部產品工程師
  • Ping Yeung,Mentor功能驗證部總工程師

(本文同步刊登於《電子工程專輯》雜誌2020年5月號;參考原文: Catch More Bugs with Formal Verification)

掃描或點擊QR Code立即加入 “EETimes技術論壇” Line 群組 !

 EET-Line技術論壇-QR

發表評論