RTL到門級(jí)設(shè)計(jì)的等價(jià)性驗(yàn)證的研究.pdf

1、超大規(guī)模集成電路的驗(yàn)證工作在產(chǎn)品設(shè)計(jì)周期中所占的比例已達(dá)到三分之二。等價(jià)性驗(yàn)證作為現(xiàn)代SoC設(shè)計(jì)流程的一個(gè)重要步驟，用于驗(yàn)證不同抽象層設(shè)計(jì)之間的功能等效性。包含算術(shù)電路的設(shè)計(jì)的驗(yàn)證工作則是等價(jià)性驗(yàn)證的熱點(diǎn)和難點(diǎn)之一。為了解決這個(gè)問題，本文作者結(jié)合自主研發(fā)等價(jià)性驗(yàn)證系統(tǒng)（ZDFV）的工作，在高效綜合引擎的研究與實(shí)現(xiàn)、單個(gè)模塊的相似性研究、數(shù)據(jù)通路的驗(yàn)證方法、結(jié)合半加圖的算術(shù)單元驗(yàn)證以及基于混合SAT引擎的RTL驗(yàn)證流程等五個(gè)方面開展了研究

2、： 1．高效綜合引擎的研究與實(shí)現(xiàn)：等價(jià)性驗(yàn)證的效率取決于兩個(gè)設(shè)計(jì)的相似性，綜合引擎的好壞決定了相似性。本文在充分研究Icarus Verilog可綜合子集及相關(guān)綜合算法的基礎(chǔ)上，以ZDFV的綜合引擎為代表，分析了高級(jí)程序語句的綜合方法，提出了一種高效的綜合流程，實(shí)現(xiàn)了模塊的重用，并支持多種宏定義和編譯向?qū)?。通過對(duì)Icarus Verilog和ZDFV的綜合引擎的對(duì)比分析，并以IWLS_2005_bechmarks_V_1．0為測(cè)

3、試基礎(chǔ)，實(shí)驗(yàn)結(jié)果顯示：在相同的測(cè)試平臺(tái)下，ZDFV的綜合引擎在處理多文件描述的Verilog設(shè)計(jì)時(shí)具有更好的兼容性，而對(duì)于不帶層次結(jié)構(gòu)描述的Verilog設(shè)計(jì)時(shí)間上的改善度可高達(dá)98％。 2．單個(gè)模塊的相似性研究：模塊相似性在等價(jià)性驗(yàn)證中具有重要的指引作用，對(duì)驗(yàn)證引擎的性能有著關(guān)鍵性的影響。本文提出了一種新的從RTL到門級(jí)網(wǎng)表的等價(jià)性驗(yàn)證流程：提取電路信息、綜合待驗(yàn)證的設(shè)計(jì)、匹配待驗(yàn)證設(shè)計(jì)的等價(jià)點(diǎn)、比較待驗(yàn)證設(shè)計(jì)的等價(jià)點(diǎn)。不同于

4、傳統(tǒng)驗(yàn)證流程，為獲得最好的電路相似性，此流程深入研究了綜合優(yōu)化等因素在不同層次上對(duì)電路相似性的破壞，提出了在綜合階段對(duì)比IP的不同實(shí)現(xiàn)方案，并進(jìn)行啟發(fā)式?jīng)Q策。以驗(yàn)證不同實(shí)現(xiàn)方案的乘法電路為例，本算法的驗(yàn)證準(zhǔn)確性更高，而驗(yàn)證時(shí)間可減少3％～28％。 3．?dāng)?shù)據(jù)通路的驗(yàn)證：數(shù)據(jù)通路由一系列的算術(shù)表達(dá)式在行為域里表示，可按具體的變換規(guī)則進(jìn)行優(yōu)化組合。依照不同描述級(jí)，本文討論了驗(yàn)證不同數(shù)據(jù)通路表示的各種算法，通過在寄存器傳輸級(jí)上比較重寫數(shù)

5、據(jù)通路以證明其等價(jià)性，提出了在數(shù)據(jù)通路級(jí)指導(dǎo)綜合過程，有效簡(jiǎn)化了網(wǎng)表級(jí)等價(jià)性驗(yàn)證的復(fù)雜度。比如針對(duì)加法和乘法連續(xù)運(yùn)算的表達(dá)式，算法從實(shí)現(xiàn)電路中提取變量順序和結(jié)合順序并加以利用，實(shí)驗(yàn)表明，在驗(yàn)證乘法連續(xù)運(yùn)算的表達(dá)式時(shí)減少了83％～99％的時(shí)間，加法連續(xù)運(yùn)算表達(dá)式的驗(yàn)證時(shí)間也可減少40％～89％。 4．結(jié)合半加圖的算術(shù)單元驗(yàn)證：論文研究了基于BMD驗(yàn)證乘法電路的方法，該方法使用矩分解（moment decomposition）方式，

6、在BMD的邊和節(jié)點(diǎn)上賦予權(quán)重信息，減少了圖的節(jié)點(diǎn)數(shù)。討論了一種新的電路表示方法——半加圖（HalfAdder Graph），提出在綜合階段使用半加圖表示算術(shù)電路，從中得到算術(shù)電路的實(shí)現(xiàn)方案，進(jìn)一步指導(dǎo)算術(shù)電路的綜合。統(tǒng)計(jì)提取電路實(shí)現(xiàn)和驗(yàn)證的時(shí)間花銷，以乘法電路為例，本算法能明顯提高驗(yàn)證引擎的性能（4％～63％）。 5．基于混合SAT引擎的RTL驗(yàn)證流程：傳統(tǒng)驗(yàn)證流程需要將電路綜合為門級(jí)網(wǎng)表，但門級(jí)驗(yàn)證引擎不能有效利用一些原始的電