集成電路的邏輯等價(jià)性驗(yàn)證研究.pdf

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

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

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