基于邏輯錐和SAT的帶黑盒電路等價性驗證方法.pdf

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

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

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