基于邏輯錐和SAT的帶黑盒電路等價(jià)性驗(yàn)證方法.pdf

1、隨著信息產(chǎn)業(yè)的發(fā)展，超大規(guī)模集成電路和數(shù)字系統(tǒng)幾乎占據(jù)了我們生活的所有領(lǐng)域。而且，由于芯片設(shè)計(jì)復(fù)雜性與日俱增，新產(chǎn)品的功能驗(yàn)證難度也逐漸加大。由于這些原因，在設(shè)計(jì)階段早期發(fā)現(xiàn)錯(cuò)誤顯得十分必要。因此，開發(fā)形式化驗(yàn)證技術(shù)來(lái)處理那些或許會(huì)引起功能不正確的設(shè)計(jì)階段是非常重要的。 等價(jià)性驗(yàn)證是形式化驗(yàn)證方法之一，它主要解決驗(yàn)證兩個(gè)電路是否功能等價(jià)的問題?，F(xiàn)在電路設(shè)計(jì)經(jīng)常包含某些功能未知的模塊，這些模塊被稱作黑盒。為了在早期階段發(fā)現(xiàn)設(shè)計(jì)錯(cuò)誤

2、，我們對(duì)帶黑盒的實(shí)現(xiàn)電路進(jìn)行等價(jià)性驗(yàn)證。 本文主要研究了集成電路的等價(jià)性驗(yàn)證理論及其在帶黑盒電路上的應(yīng)用，進(jìn)而提出一種基于邏輯錐分割和SAT的帶黑盒電路的等價(jià)性驗(yàn)證方法。主要包括以下三方面的內(nèi)容： 1．等價(jià)性驗(yàn)證：等價(jià)性驗(yàn)證技術(shù)證明兩個(gè)被給定電路具有相同的功能。例如，一個(gè)優(yōu)化的設(shè)計(jì)與其早期版本是功能等價(jià)的。在驗(yàn)證過程中，驗(yàn)證方法被分為兩類：(1)符號(hào)方法，(2)增量方法。符號(hào)方法是指依賴于使用BDD符號(hào)技術(shù)的那些方法；增

3、量方法是指在驗(yàn)證中，開發(fā)兩個(gè)電路的結(jié)構(gòu)相似性。 2．帶黑盒的等價(jià)性驗(yàn)證：在假設(shè)規(guī)范電路和帶黑盒的實(shí)現(xiàn)電路具有組合性質(zhì)的基礎(chǔ)上，提出帶黑盒的等價(jià)性驗(yàn)證方法。這些方法包括Local Check，Output Exact Check和Input Exact Check。使用這些方法相繼地增加了算法的準(zhǔn)確性和復(fù)雜性。 3．一個(gè)有效的帶黑盒電路的驗(yàn)證方法：我們提出了一種基于邏輯錐分割和可滿足性的檢驗(yàn)算法。根據(jù)“分而治之”的方法，把