組合電路等價驗證預處理算法研究.pdf

1、隨著大型集成電路設計和SOC芯片設計的不斷進步,電路的規(guī)模,硬件的復雜度不斷增大。今天,70％的設計時間是花費在驗證錯綜復雜的系統(tǒng)上,傳統(tǒng)的驗證方法已經不能完全滿足現(xiàn)今的要求,而形式驗證則變得越來越重要,現(xiàn)在2種使用最廣泛的形式驗證技術相等性檢查和模塊檢查成為研究的突破方向。
　　 本文研究工作是針對可滿足問題(SAT)在組合電路驗證和測試中的應用展開的。本文提出了一種能提高基于SAT的組合相等性檢測,研究出一個低損耗的預處理器

2、,可以靜念地引入全局信號關系到原先的需要驗證的Miter電路CNF公式,來減低SAT語句的復雜性,有效快速的建立蘊涵圖,產生大量的直接,非直接和擴展回溯蘊含,加入到Miter電路的CNF公式中,來減少分析的時間。
　　 本文主要的價值之處在于:(1)通過全局信號關系引入恰當?shù)恼Z句,快速建立蘊含圖,并且轉換蘊含表達式為二進制子句。(2)利用加入的子句來約束SAT解決器的搜索空間,提供各個變量之間的關系,來增強布爾約束傳遞,大幅減少