1、隨著集成電路設計的規(guī)模變得越來越大、功能越來越復雜，功能驗證已經(jīng)成為設計流程的主要瓶頸。據(jù)統(tǒng)計，設計驗證的時間已占到整個設計周期的一半以上。基于模擬的功能驗證方法非常費時，難以達到100％的功能覆蓋率。形式驗證方法使用嚴格的數(shù)學推理來證明設計滿足規(guī)范的部分或全部屬性，引起學術界和產(chǎn)業(yè)界的廣泛關注。等價性檢驗是一種形式驗證方法，用來驗證一個設計的不同描述形式之間的功能等價性。本文的工作涵蓋邏輯電路等價性檢驗的幾個關鍵問題：如何提高增量等價

2、性檢驗算法的效率；如何驗證包含黑盒的電路設計；如何有效地結合布爾推理中的不同引擎以提高布爾推理算法的效率：如何提高設計錯誤診斷的效率。通過系統(tǒng)深入的理論分析和扎實的實驗研究，取得了如下創(chuàng)新性成果： 1．提出了一種基于增量可滿足性的等價性檢驗方法。利用兩個電路內(nèi)部的結構相似性，將整個電路的驗證分解成一些較小的任務，增量地完成。與同類方法相比，具有三個新的特點：(1)有選擇地消除一些容易影響性能的候選等價信號對，減小可滿足性程序的調(diào)

3、用頻度。(2)采用等價結點置換方法消除誤判，并且增加相應的表示等價關系的合取范式公式，有效縮小可滿足性程序的搜索空間。(3)使用增量可滿足性算法，大幅度節(jié)省計算資源。通過對ISCAS'85電路的驗證實驗研究表明，對各基準電路，該方法產(chǎn)生的候選等價結點數(shù)比同類方法要少1個數(shù)量級，算法速度比同類方法平均要快3倍至1個數(shù)量級。 2．提出了一種針對包含黑盒電路的設計驗證方法。將模擬與形式化的布爾比較相結合，使用并行邏輯模擬來檢測黑盒外部

4、可能的設計錯誤，通過基于布爾可滿足性(SAT)的布爾比較增強模擬算法。與基于二叉判決圖(BDD)的方法相比，該方法具有更強的處理能力，有效降低了算法的空間復雜度。該方法已成功地應用于提高設計錯誤診斷的效率。通過ISCAS'85電路的實驗研究表明，在具有與同類方法相當?shù)腻e誤檢測能力的情況下，該方法對于各實驗電路平均要快1至2個數(shù)量級，而且錯誤診斷的準確性更高。 3．提出了有效結合多引擎的啟發(fā)式策略。通過計算相關電路的寬度，在進行布