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

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

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

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

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