從小眾走向普及，形式化驗(yàn)證對系統(tǒng)級芯片開發(fā)有多重要？

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

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

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

這種擴(kuò)張一定程度是因?yàn)轵?yàn)證結(jié)果比以往更加容易獲取，以及可以被更好地量化?！皯?yīng)用程序”概念的出現(xiàn)極大地縮短了有效驗(yàn)證的學(xué)習(xí)曲線，對覆蓋率定義的改進(jìn)也讓開發(fā)者們更加相信，形式化驗(yàn)證以得到有效衡量。此外，屬性檢查證明了形式化驗(yàn)證可以解決仿真所無法解決的難題。

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

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

• 一致性網(wǎng)格結(jié)構(gòu)的正確性
• CPU集群上運(yùn)行的固件的正確性

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

形式化驗(yàn)證未來展望

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

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