英特爾(Intel)在SNUG的主題演講：拓展形式化驗證之思維

智慧理解與樣本測試

各種形式的測試驅動模擬(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比對後出現不相符的結果，這也是它應該要執行的任務。然而，仰賴未定義的行為具有高度風險。

超越等效性檢測

DPV 的主要目的似乎是檢測 C 或 RTL 參考與 RTL 實作之間的等效性。但是這種需求相對罕見，而且還有其他實用方法可以應用於此(儘管有點超出常規應用範圍)。首先，實作領域中的經典案例：「我進行了一項變更，修復一個錯誤」，那麼我是否因此而引入任何新的錯誤？有點類似新增時脈閘控(clock gating)後的SEQ 檢測。在某些案例中，模塊輸出的可達性分析(reachability analysis)可能是另一種有效的應用。

總結

Theo Drane博士在總結時探討了針對生產應用的重要方法，內容包括限制(constraint)、迴歸(regression)以及與傳統 RTL 模型的比對(comparison)。此外，他也探討瞭解正在檢測的內容是否確實符合最高層級自然語言標準所面臨的挑戰。