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

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

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

這種擴張一定程度是因為驗證結果比以往更加容易獲取，以及可以被更好地量化?！皯贸绦颉备拍畹某霈F(xiàn)極大地縮短了有效驗證的學習曲線，對覆蓋率定義的改進也讓開發(fā)者們更加相信，形式化驗證以得到有效衡量。此外，屬性檢查證明了形式化驗證可以解決仿真所無法解決的難題。

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

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

• 一致性網(wǎng)格結構的正確性
• CPU集群上運行的固件的正確性

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

形式化驗證未來展望

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

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