形式化驗證作為一種全新的驗證方法，近年來在芯片開發中快速發展，正逐漸取代傳統的仿真方法。

雖然仿真在系統級驗證方面仍然發揮著重要的作用，但對于單元級的signoff而言，形式化驗證已經成為首選。據估計，在未來五年內仿真將逐漸被取代，僅用于子系統和系統級驗證。與此同時，形式化驗證方法已經開始處理一些系統級任務，隨著技術的不斷創新，形式化驗證將逐步開始處理更多系統級任務。

形式化驗證的普及

近五年來，更多機構和設計驗證人員更廣泛地參與到了整體驗證目標之中。除了率先在半導體設計中采用形式化驗證技術的英特爾公司以外，還有很多其他半導體和系統公司的開發者們開始積極地嘗試這一技術。

這種擴張一定程度是因為驗證結果比以往更加容易獲取，以及可以被更好地量化。“應用程序”概念的出現極大地縮短了有效驗證的學習曲線，對覆蓋率定義的改進也讓開發者們更加相信，形式化驗證以得到有效衡量。此外，屬性檢查證明了形式化驗證可以解決仿真所無法解決的難題。

這些成功的案例激發了開發者們對形式化驗證更深入的思考：作為一種有效的驗證技術，形式化驗證是否只適用于特殊情況，或者是否有可能顯著提高整體驗證任務的貢獻？

形式化signoff的挑戰

對形式化技術而言，如果其能夠取代動態技術，以更低的成本實現更高質量的signoff，那將是又一重大突破。

近年來商業形式化驗證方法的積極應用，以及通過C到RTL等價性檢查所做的規范級別比較，對于實現這一目標有著標志性的意義。現如今有多個模塊僅通過形式化驗證即可進行signoff，動態調試對signoff而言，雖仍然重要，但作用已被削弱。

考慮到數據路徑元件在GPU、DSP、AI和當今許多其他加速器中的重要性，突破數據路徑邊界是利用形式化驗證技術完成絕大多數單元signoff任務的關鍵一步。這種從動態signoff到形式化signoff的變化，大大提升了生產力。而以往的實驗證明，用這一方法signoff的一些關鍵模塊在多代產品中沒有出現一個錯誤。運用形式化技術達到了更高的生產率和更高的質量，這一點已然被證實。

擴大形式化驗證方法的ROI：架構驗證

在架構驗證領域，形式化驗證方法也取得了很大的成功。其相關應用主要包括：

• 一致性網格結構的正確性
• CPU集群上運行的固件的正確性

形式化驗證方法的ROI不斷得到驗證和擴大。目前，這些技術主要依賴于開發者們在抽象化設計方面的開發經驗和專業知識，以及各種開源工具和一些商業產品。隨著時間推移，會有更多類似的功能實現標準化。

形式化驗證開發人才需求增加

相比于動態測試，形式化驗證的本質要求開發者對設計有更詳細的了解。隨著工業界對形式化驗證提出更多需求，許多頭部公司和一些掌握尖端科技的初創公司都在努力提高形式化驗證的能力，這就對開發者的能力提出了更高且更新的要求。

目前企業傾向于開展基礎培訓來幫助應屆畢業生了解和進入行業，在接受培訓后，形式化驗證開發者往往對工作的熱情要遠高于其他人，而在大學校園內，亦設置了EE/CS本科相關課程來支持行業對形式化驗證開發人才的需求，期待相關專家人才迅速增多，去探索自己職業所面臨的挑戰和機遇。

形式化驗證未來展望

五年前，有人可能認為形式化驗證是解決專門問題的小眾技術，但這種觀點現在已經逐漸被改變。現在，大型系統和半導體公司將形式化驗證視為任何可信驗證策略的重要組成部分。更重要的是，形式化驗證方法現在已經發展到可在某些領域中取代仿真的地步。形式化驗證開始為系統級領域做出貢獻，而在以前，形式化驗證在這些領域被認為是不切實際的。

對于形式化驗證和形式化驗證團隊來說，這是一個令人興奮的時代。由于貢獻不斷增大和在業務關鍵型需求上為人們帶來的更多信心，形式化驗證技術對所有數字設計領域的產品設計和開發變得越來越重要。

掃描下方二維碼，下載白皮書《形式化驗證探索指南》，詳細了解形式化驗證的更多相關內容。