VLSI設(shè)計中的形式驗證方法研究.pdf

1、超大規(guī)模集成電路(VLSI)的設(shè)計日趨復(fù)雜，驗證工作越來越繁重，驗證難度也越來越大。在復(fù)雜的VLSI設(shè)計中，驗證過程所需的時間約占整個設(shè)計周期的三分之二，設(shè)計過程所需要的專業(yè)驗證工程師人數(shù)大約是設(shè)計工程師的兩倍，功能驗證已成為VLSI設(shè)計的瓶頸。傳統(tǒng)的軟件模擬和硬件仿真需要花費大量的時間，且不能完全保證功能的正確性。形式驗證作為傳統(tǒng)驗證方法的補(bǔ)充，日益引起人們的關(guān)注。形式驗證使用嚴(yán)格的數(shù)學(xué)推理來證明設(shè)計滿足規(guī)范的部分或者全部屬性，所需要

2、的驗證時間比較少，是克服驗證瓶頸的可行途徑。本文對VLSI的形式驗證方法進(jìn)行了研究，主要工作如下： 1)針對數(shù)據(jù)密集型電路的等價性驗證，提出了WGL模型的改進(jìn)模型——W2GL。WGL的節(jié)點是位級變量，在字級算術(shù)運算表示方面具有局限性，而W2GL能有效地表示字級算術(shù)運算。本文還證明了一個有序的、簡化的W2GL模型是最小的和正則的，并提出了W2GL模型的變量排序方法及加法和乘法算法。運用這些方法和算法可以構(gòu)建寄存器傳輸級(RTL)電

3、路的有序的、簡化的和正則的W2GL模型，進(jìn)行電路優(yōu)化前后的等價性驗證。實驗結(jié)果表明，與*BMD和WGL模型相比，W2GL模型對數(shù)據(jù)密集型電路的等價性驗證不論在存儲空間還是在CPU運行時間上均有明顯的減少。 2)針對同時包含字級、位級變量算術(shù)運算和邏輯運算的復(fù)雜電路的等價性驗證，對W2GL模型進(jìn)行擴(kuò)充，提出了混合WGL模型—HWGL。W2GL模型能有效地表示字級算術(shù)運算，但在表示字級邏輯運算時比較復(fù)雜，需要把字級變量拆分成位級變量

4、。本文提出的HWGL模型既可以有效表示字級的算術(shù)運算和邏輯運算，又可以有效表示位級的算術(shù)運算和邏輯運算。對復(fù)雜電路構(gòu)建HWGL模型，可實現(xiàn)優(yōu)化前后電路的等價性驗證。HWGL模型的大小與字長無關(guān)，并且需要較少的節(jié)點和構(gòu)造時間。實驗結(jié)果表明，對復(fù)雜的包含字級變量和位級變量的電路，HWGL比W2GL和*BMD更有效。 3)針對性質(zhì)檢驗問題，本文在HWGL模型的基礎(chǔ)上，提出了一種分支WGL模型—BWGL。BWGL模型是對HWGL模型的擴(kuò)

5、充，模型中用到的變量節(jié)點是HWGL，并在模型中增加了分支節(jié)點、Union節(jié)點和Intersect節(jié)點。把BWGL模型應(yīng)用于性質(zhì)檢驗，把設(shè)計中的性質(zhì)描述成一個線性時間邏輯，根據(jù)時間片選擇不同的檢驗過程驗證性質(zhì)是否滿足。把基于BWGL的性質(zhì)檢驗與基于BDD的VIS系統(tǒng)進(jìn)行比較，實驗結(jié)果表明，在處理器驗證方面，基于BWGL的性質(zhì)檢驗比VIS系統(tǒng)更有效，可以利用較少的資源在較短的時間內(nèi)完成驗證。另外，基于BWGL的性質(zhì)檢驗可以同時驗證數(shù)據(jù)通路和