邏輯電路的等價(jià)性檢驗(yàn)方法研究.pdf

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

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

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

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