隨著信息產(chǎn)業(yè)的發(fā)展，超大規(guī)模集成電路和數(shù)字系統(tǒng)幾乎占據(jù)了我們生活的所有領(lǐng)域。而且，由于芯片設(shè)計復(fù)雜性與日俱增，新產(chǎn)品的功能驗證難度也逐漸加大。由于這些原因，在設(shè)計階段早期發(fā)現(xiàn)錯誤顯得十分必要。因此，開發(fā)形式化驗證技術(shù)來處理那些或許會引起功能不正確的設(shè)計階段是非常重要的。等價性驗證是形式化驗證方法之一，它主要解決驗證兩個電路是否功能等價的問題�，F(xiàn)在電路設(shè)計經(jīng)常包含某些功能未知的模塊，這些模塊被稱作黑盒。為了在早期階段發(fā)現(xiàn)設(shè)計錯誤，我們對帶黑盒的實現(xiàn)電路進行等價性驗證。本文主要研究了集成電路的等價性驗證理論及其在帶黑盒電路上的應(yīng)用，進而提出一種基于邏輯錐分割和SAT的帶黑盒電路的等價性驗證方法。主要包括以下三方面的內(nèi)容：1．等價性驗證：等價性驗證技術(shù)證明兩個被給定電路具有相同的功能。例如，一個優(yōu)化的設(shè)計與其早期版本是功能等價的。在驗證過程中，驗證方法被分為兩類：（1）符號方法，（2）增量方法。符號方法是指依賴于使用BDD符號技術(shù)的那些方法；增量方法是指在驗證中，開發(fā)兩個電路的結(jié)構(gòu)相似性。2．帶黑盒的等價性驗證：在假設(shè)規(guī)范電路和帶黑盒的實現(xiàn)電路具有組合性質(zhì)的基礎(chǔ)上，提出帶黑盒的等價性驗證方法... 

【文章來源】：蘭州大學甘肅省 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：65 頁

【學位級別】：碩士

【部分圖文】：

EDA驗證需求

驗證工作占用的時間最多，特別是進入深亞微米領(lǐng)域，幾乎80%的時間都花費在驗證方面(如圖2.1所示)。造成這種局面的原因有二:一方面，設(shè)計的規(guī)模正如摩爾定律所指出的呈指數(shù)增長(如圖2.2所示)。如果使用設(shè)計中的狀態(tài)數(shù)目來衡量功能復(fù)雜度的話，則設(shè)計的功能復(fù)雜度隨著設(shè)計規(guī)模又呈指數(shù)增長。如此驚人的速度，對驗證技術(shù)的處理能力提出了巨大挑戰(zhàn)。另一方面，歷史上對設(shè)計流程中的其它環(huán)節(jié)，如邏輯綜合、布局布線和測試產(chǎn)生等問題關(guān)注頗多，而對驗證重視不夠，造成驗證成為目前集成電路設(shè)計的瓶頸，如果沒有重大突破，驗證將成為未來集成電路設(shè)計工業(yè)【19}流程中的重大障礙。傳統(tǒng)的模擬仿真等驗證技術(shù)，己經(jīng)越來越不能適應(yīng)日益復(fù)雜的設(shè)計要求。

功能屬性有效或無效，因此能夠?qū)λ锌赡艿倪\行狀態(tài)進行完全徹底的探查。一般來說，功能驗證方法主要有模擬(simulation)、硬件仿真(HardwareEmulation)、形式化方法 (FormalMethod)(如圖2.4所示)。其中形式化驗證方法大致可以分為等價性檢驗 (EqulvaleneeCbeeking){3，20}、定理證明(TheoremProving)和模型檢測 (ModelCheeking)。等價性檢驗是目前在工業(yè)實踐中廣泛使用的一種形式化驗證方法，而且已經(jīng)被應(yīng)用于驗證大型復(fù)雜系統(tǒng)的設(shè)計。等價性檢驗的基本思想是對照設(shè)計的形式化規(guī)范來驗證它的實現(xiàn)的功能正確性。等價性檢驗使驗證工程師節(jié)省了大量的時間，因為它使用形式化方法而不需要產(chǎn)生測試向量，此外，這種方法對于檢測設(shè)計錯誤也很有效。等價性檢驗可以用來驗證兩個相同或者不同抽象級別設(shè)計的等價性，如


本文編號：3548224