基于BDD和SAT的形式驗(yàn)證方法的研究.pdf

1、隨著集成電路的設(shè)計(jì)規(guī)模越大越大、復(fù)雜度越來越高，產(chǎn)品上市時(shí)間卻越來越緊迫，集成電路的驗(yàn)證變得越來越困難。2003年度的國(guó)際半導(dǎo)體技術(shù)發(fā)展報(bào)告(Intemational Technology Roadmap for Semi-conductor,ITRS2003)指出，驗(yàn)證已經(jīng)成為集成電路設(shè)計(jì)流程中最大瓶頸。傳統(tǒng)的模擬驗(yàn)證因其測(cè)試周期長(zhǎng)、不能完全覆蓋，已經(jīng)不適合當(dāng)前對(duì)集成電路的驗(yàn)證。過去二十年中，人們發(fā)展了一種新方法一形式化驗(yàn)證(Form

2、al Verification)方法。這是VLSI(Very Imrge Scale Integration)設(shè)計(jì)驗(yàn)證的一種有希望的方法。 形式驗(yàn)證意味著驗(yàn)證過程是數(shù)學(xué)化的，而不是如模擬技術(shù)那樣，是試驗(yàn)性質(zhì)的。數(shù)學(xué)化的驗(yàn)證克服了模擬的不足，因?yàn)樗母采w是完全的。形式驗(yàn)證可以對(duì)電路描述進(jìn)行自動(dòng)化的驗(yàn)證，減少了驗(yàn)證的復(fù)雜度。形式驗(yàn)證作為傳統(tǒng)基于模擬的驗(yàn)證方法的補(bǔ)充，日益引起人們的關(guān)注。它的特點(diǎn)是使用嚴(yán)格的數(shù)學(xué)推理來證明一個(gè)系統(tǒng)滿足全

3、部或部分規(guī)范。 本文研究基于BDD及布爾可滿足(SAT)算法的形式化驗(yàn)證方法。本文針對(duì)布爾可滿足性SAT算法中存在的搜索空間大且復(fù)雜度高等問題，對(duì)SAT算法進(jìn)行了相應(yīng)的改進(jìn)，并提出了一種新的SMT的全局搜索算法-DC&DS算法。其搜索空間比現(xiàn)有的布爾可滿足性算法搜索空間都低得多，從而大大提高了算法的效率。并將該算法應(yīng)用到結(jié)合BDD和SAT算法的形式驗(yàn)證中，并且進(jìn)行了實(shí)驗(yàn)分析。 理論研究和實(shí)驗(yàn)結(jié)果驗(yàn)證了文中提出的新算法的有