DSO.ai
由人工智慧驱动的设计应用
瞭解更多 →
英特尔(滨苍迟别濒)在厂狈鲍骋的主题演讲：拓展形式化验证之思维
英文原文：
2023年3月22日於《厂别尘颈奥颈办颈》刊登
英特爾(Intel)圖形事業部(Graphics) Theo Drane 博士以資料路徑等效性檢測(equivalency checking)為題在新思科技年度使用者大會上發表的精彩演講內容，已在新思科技 網站上公開。或許此主題聽起來就像是對新思科技 VC Formal DPV 的另一次背書，但無論如何您都應該深入瞭解這場可以拓展思維的演說內容；其中針對形式化验证(formal)的應用與注意面向各方面的討論，都已超越常規的用戶指南，而是引領使用者進入一個更加精采的領域。
智慧理解与样本测试
各種形式的測試驅動模拟(test-driven verification)在验证设计規格或實作的正確性方面都相當出色，且通常是不可取代的。啟動模拟也很容易上手，只需要編寫測試程式即可開始模拟。但是事情總是一體兩面，簡易性的背後代表著我們不需要完整理解正在測試的內容就可以開始進行測試。我們說服自己已經詳細閱讀規格，並瞭解所有的極端案例(corner case)，但事實上，即使沒有太複雜，我們的認知也都能被輕鬆擊潰。
形式化验证讓您可以深入瞭解功能 (至少在您想要交付有價值的結果的情況下)。舉例來說，試問一個簡單的問題「Z 是否可以全為1？」在此情況，即使模拟運行超過數十億次週期，都無法演示出一個範例。這並不足為奇，因為這就是一個極端案例。相較之下，形式化验证測試在 188 秒內即可提供一個非常不顯著的具體範例，並可以在更少的時間內證明這是唯一的案例。
是的，形式验证可實現動態檢測無法達成的目標，但更重要的是，您能夠瞭解到模拟器可能永遠無法告訴您的內容。那就是，只有一種可能的情況會產生這種結果。形式验证讓您可以聰明妥善地理解设计，而不僅止於識別有限測試案例組合的機率总结。
规格问题
Theo Drane博士接著探討的範例是「bug自動販賣機」(如此稱呼的原因是因為當您按一下按鈕，就會得到一個錯誤的結果)。這看起來似乎是非常簡單的 C 到 RTL 等效性檢測問題，C 模型在左側，而 RTL模型在右側。在Drane博士針對形式验证的早期研究階段，令其驚訝的是即使 gcc具備合理的行為表現，但是C 模型的右移(shift-right)行為卻並未被完整定義在C 語言中。在此情況下資料路徑验证 (Datapath Validation, DPV)理所當然會指出與 RTL比對後出現不相符的結果，這也是它應該要執行的任務。然而，仰賴未定義的行為具有高度風險。
C 與 RTL之間的規格比對還存在著其他風險因素，尤其是在位寬(bit width)周圍。截斷或失去中間訊號的進位位元(carry bit)就是很好的範例(請見上圖#3)。這些可以稱之為规格问题嗎？也許規格與實作選項之間存在灰色地帶。
超越等效性检测
DPV 的主要目的似乎是檢測 C 或 RTL 參考與 RTL 實作之間的等效性。但是這種需求相對罕見，而且還有其他實用方法可以應用於此(儘管有點超出常規應用範圍)。首先，實作領域中的經典案例：「我進行了一項變更，修復一個錯誤」，那麼我是否因此而引入任何新的錯誤？有點類似新增時脈閘控(clock gating)後的SEQ 檢測。在某些案例中，模塊輸出的可達性分析(reachability analysis)可能是另一種有效的應用。
Drane博士甚至更有創意，要求受訓人員使用反例來更好地瞭解设计、或。他坦言使用 DPV處理該類問題很奇怪，但是也指出其用意是打破 DPV 只能用於等效性檢測的錯覺。這是一項有趣的想法，而且在此類難題的思考過程中也必定能拓展思維。(我承認，當他一提到數獨問題，我就立即開始思考了。)
总结
Theo Drane博士在总结時探討了針對生產應用的重要方法，內容包括限制(constraint)、迴歸(regression)以及與傳統 RTL 模型的比對(comparison)。此外，他也探討瞭解正在檢測的內容是否確實符合最高層級自然語言標準所面臨的挑戰。