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

【文章來(lái)源】：蘭州大學(xué)甘肅省 211工程院校 985工程院校 教育部直屬院校

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

【學(xué)位級(jí)別】：碩士

【部分圖文】：

EDA驗(yàn)證需求

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

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


本文編號(hào)：3548224