數(shù)字電路后端的形式驗(yàn)證方法研究及應(yīng)用.pdf

1、隨著集成電路設(shè)計(jì)領(lǐng)域的發(fā)展，芯片集成度越來(lái)越高，功能越來(lái)越強(qiáng)大，驗(yàn)證的地位也越來(lái)越高。其中形式驗(yàn)證中的等價(jià)性檢查貫穿于整個(gè)后端設(shè)計(jì)流程之中。有代碼與綜合后網(wǎng)表之間的驗(yàn)證等價(jià)性檢查；綜合后的網(wǎng)表與布局布線后設(shè)計(jì)之間的等價(jià)性檢查。論文描述了數(shù)字電路后端驗(yàn)證的發(fā)展和流程。研究了等價(jià)性檢查的方法，包括組合電路檢查方法、時(shí)序電路檢查方法。 論文通過(guò)macphy_d1加速器模塊完成了等價(jià)性檢查。檢查首先準(zhǔn)備了加速器模塊RTL，代碼與網(wǎng)表的信

2、息。加速器網(wǎng)表的面積，RTL代碼標(biāo)準(zhǔn)庫(kù)(startlib_lphvt_9t)中各個(gè)模塊的面積、數(shù)量等參數(shù)。 其次完成了模塊驗(yàn)證流程。1.由準(zhǔn)備過(guò)程產(chǎn)生流程與編譯腳本，等價(jià)性檢查在操作系統(tǒng)linux底下的目錄。2.由抽取過(guò)程從加速器模塊RTL代碼中得到需要編譯的代碼，并且產(chǎn)生編譯腳本。3.在編譯過(guò)程中檢查RTL代碼與網(wǎng)表，并且得到要進(jìn)行比較的gat文件。4.在比較過(guò)程中加上約束，給各個(gè)狀態(tài)機(jī)賦輸入與狀態(tài)初值，查看下一狀態(tài)與輸出值。