VLSI設(shè)計(jì)中的形式驗(yàn)證方法研究.pdf

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

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

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

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

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