RTL到門級設(shè)計的等價性驗證的研究.pdf

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

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

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

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

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

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