基于BDD和SAT的形式驗證方法的研究.pdf

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

2、al Verification)方法。這是VLSI(Very Imrge Scale Integration)設計驗證的一種有希望的方法。 形式驗證意味著驗證過程是數學化的，而不是如模擬技術那樣，是試驗性質的。數學化的驗證克服了模擬的不足，因為它的覆蓋是完全的。形式驗證可以對電路描述進行自動化的驗證，減少了驗證的復雜度。形式驗證作為傳統(tǒng)基于模擬的驗證方法的補充，日益引起人們的關注。它的特點是使用嚴格的數學推理來證明一個系統(tǒng)滿足全

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