基于有限環(huán)上多項(xiàng)式的數(shù)字電路形式驗(yàn)證方法.pdf

1、隨著集成電路的規(guī)模變得越來(lái)越大、功能越來(lái)越復(fù)雜，功能驗(yàn)證已經(jīng)成為設(shè)計(jì)流程的主要瓶頸。據(jù)統(tǒng)計(jì)，設(shè)計(jì)驗(yàn)證的時(shí)間已占到整個(gè)設(shè)計(jì)周期的一半以上。傳統(tǒng)的基于模擬的驗(yàn)證方法不但需要花費(fèi)大量的時(shí)間，而且不能保證完全的驗(yàn)證覆蓋率，已經(jīng)不能滿足現(xiàn)時(shí)集成電路設(shè)計(jì)的要求。形式驗(yàn)證利用數(shù)學(xué)的方法隱式遍歷所有可能的情況，能保證完全的驗(yàn)證覆蓋率，所需要的驗(yàn)證時(shí)間也大幅減少，是克服驗(yàn)證瓶頸的可行途徑。本文以有限環(huán)上多項(xiàng)式為基礎(chǔ)模型，圍繞算術(shù)密集型設(shè)計(jì)(例如數(shù)字信號(hào)處

2、理(DSP)電路)的等價(jià)性檢驗(yàn)和定界模型檢驗(yàn)，進(jìn)行了深入研究，取得了如下創(chuàng)新性成果： (1)針對(duì)實(shí)現(xiàn)多項(xiàng)式運(yùn)算的定點(diǎn)數(shù)據(jù)通路的邏輯門級(jí)與寄存器傳輸級(jí)(RTL)之間的等價(jià)性檢驗(yàn)，提出一種將定點(diǎn)數(shù)據(jù)通路的位級(jí)描述抽象為字級(jí)描述的方法。首先采用算術(shù)轉(zhuǎn)換描述定點(diǎn)數(shù)據(jù)通路的邏輯門級(jí)功能，采用多項(xiàng)式函數(shù)描述定點(diǎn)數(shù)據(jù)通路的RTL功能，然后采用牛頓插值方法迭代地將算術(shù)轉(zhuǎn)換抽象為多項(xiàng)式函數(shù)，以實(shí)現(xiàn)定點(diǎn)數(shù)據(jù)通路的邏輯門級(jí)模型與RTL模型之間的等價(jià)性

3、檢驗(yàn)。實(shí)驗(yàn)結(jié)果表明，該方法的速度與已有方法相比對(duì)乘法器的驗(yàn)證平均要快1至2倍，對(duì)一些實(shí)現(xiàn)多項(xiàng)式運(yùn)算的定點(diǎn)數(shù)據(jù)通路的驗(yàn)證平均要快1個(gè)數(shù)量級(jí)。 (2)針對(duì)定點(diǎn)數(shù)據(jù)通路的設(shè)計(jì)規(guī)范與RTL實(shí)現(xiàn)或優(yōu)化后的RTL實(shí)現(xiàn)之間的等價(jià)性檢驗(yàn)，構(gòu)建vanishing多項(xiàng)式環(huán)的理想的極小強(qiáng)Grobner基，并在此基礎(chǔ)上提出一種高效的等價(jià)性檢驗(yàn)算法。通過(guò)使用多項(xiàng)式函數(shù)建模定點(diǎn)數(shù)據(jù)通路的設(shè)計(jì)規(guī)范和RTL實(shí)現(xiàn)，將等價(jià)性檢驗(yàn)問題轉(zhuǎn)化為判斷一個(gè)多項(xiàng)式函數(shù)是否為v

4、anishing多項(xiàng)式的問題，進(jìn)而采用vanishing多項(xiàng)式環(huán)的理想的極小強(qiáng)Grobner基來(lái)有效地解決該問題。理論分析表明該算法的時(shí)間復(fù)雜度的上界比已有方法的時(shí)間復(fù)雜度的上界小。實(shí)驗(yàn)結(jié)果表明，對(duì)一些實(shí)現(xiàn)多項(xiàng)式運(yùn)算的定點(diǎn)數(shù)據(jù)通路的等價(jià)性檢驗(yàn)，該方法比已有方法平均要快2倍。 (3)針對(duì)DSP電路的高層次設(shè)計(jì)驗(yàn)證的定界模型檢驗(yàn)，提出一種基于有限環(huán)上多項(xiàng)式理想的Grobner基的定界模型檢驗(yàn)方法。通過(guò)使用有限環(huán)上多項(xiàng)式等式建模高層次