集成電路的邏輯等價性驗證研究.pdf

1、集成電路規(guī)模的快速增長使得驗證的難度越來越大，傳統(tǒng)的模擬和仿真不但需要花費大量的時間，而且不能保證完全的驗證覆蓋率，已經(jīng)不能滿足現(xiàn)時集成電路設(shè)計的要求。形式驗證利用數(shù)學的方法隱式遍歷所有可能的情況，能保證完全的驗證覆蓋率，所需要的驗證時間也大幅減少，是克服驗證瓶頸的可行途徑。等價性驗證作為一種實用化的形式驗證方法，常被用于綜合后和人工修改后電路的功能驗證，本論文圍繞等價性驗證在以下三個方面展開了有價值的研究： 1．在驗證組合電路

2、的等價性時，直接構(gòu)建原始輸出的BDD并進行比較的方法已經(jīng)不再適用，需要發(fā)掘出兩個待驗證電路中等價的內(nèi)部結(jié)點，利用這些結(jié)點組成割集，將原有的驗證問題分割成一系列小而簡單的子問題。針對割集在組合等價性驗證中的運用，本文創(chuàng)新性地提出了結(jié)合通用割集和專用割集的驗證方法，針對由割集引起的誤判，本文提出了一種注重消除高層次結(jié)點間依賴關(guān)系的處理策略?；贗SCAS85電路的實驗結(jié)果表明本文中的方法可以有效加快組合電路的等價性驗證。 2．在驗證

3、時序電路的等價性時，常需要通過前時間幀計算(pre-image computation)判斷某個狀態(tài)是否由初始狀態(tài)可達，它占用了全部驗證時間中的很大一部分，針對這種情況，本文創(chuàng)新性地提出了一種利用狀態(tài)緩存的時序驗證方法，將模擬過程中到達的狀態(tài)緩存為可達狀態(tài)，同時緩存驗證過程中被確認為不可達的狀態(tài)，利用它們避免重復的前時間幀計算，基于MCNC91的實驗結(jié)果表明了本方法的有效性。 3．可滿足性問題是近十多年來的一個研究熱點，它已經(jīng)超