（計(jì)算機(jī)應(yīng)用技術(shù)專業(yè)論文）通信芯片驗(yàn)證方法的研究.pdf

哈爾濱工程大學(xué)碩士學(xué)位論文 摘要 芯片的驗(yàn)證工作，對(duì)提高投片成功率起到關(guān)鍵性作用。有資料顯示，造成 芯片一次投片成功率低于5 0 的主要原因就是功能驗(yàn)證還不夠完善。根據(jù)不同 領(lǐng)域的驗(yàn)證對(duì)象和不同層次的驗(yàn)證模塊，功能驗(yàn)證有很多研究方向，如針對(duì) c p u 、片上總線、存儲(chǔ)器等的驗(yàn)證。由此可見(jiàn)根據(jù)研究對(duì)象制定驗(yàn)證策略和驗(yàn)證 方法對(duì)于提高投片成功率具有很大指導(dǎo)意義。 通信芯片一般具有實(shí)現(xiàn)收發(fā)幀、重傳、競(jìng)爭(zhēng)信道、退避等功能。根據(jù)這些 特點(diǎn)，它的功能驗(yàn)證需要模擬網(wǎng)絡(luò)環(huán)境中的情況來(lái)設(shè)計(jì)測(cè)試用例，驗(yàn)證范圍不 僅包括芯片自身在競(jìng)爭(zhēng)到信道后的模塊處理情況，還包括在網(wǎng)絡(luò)中的多站點(diǎn)競(jìng) 爭(zhēng)的情況。針對(duì)這些要求論文提出了分階段的驗(yàn)證策略，第一階段采用單向施 加激勵(lì)觸發(fā)的白盒驗(yàn)證方法，第二階段模擬多站點(diǎn)的網(wǎng)絡(luò)環(huán)境，施加多站點(diǎn)競(jìng) 爭(zhēng)發(fā)送數(shù)據(jù)等測(cè)試用例，并應(yīng)用站點(diǎn)的處理結(jié)果觸發(fā)下一事務(wù)的發(fā)生，達(dá)到循 環(huán)自觸發(fā)的半自動(dòng)化測(cè)試。 目前驗(yàn)證技術(shù)的發(fā)展都是要達(dá)到抽象化、自動(dòng)化、可重用性和可形式化驗(yàn) 證等目標(biāo)。論文研究通信芯片的驗(yàn)證方法也是從上述幾方面出發(fā)，驗(yàn)證環(huán)境采 用層次化結(jié)構(gòu)，封裝接口引腳并實(shí)現(xiàn)功能的事務(wù)級(jí)抽象；采用加約束的隨機(jī)生 成器產(chǎn)生測(cè)試用例，提高驗(yàn)證自動(dòng)化程度；驗(yàn)證層次中各模型功能獨(dú)立，便于 重用到其他通信芯片或下一代研發(fā)產(chǎn)品的驗(yàn)證中；采用s y s t e m v e r i l o g 語(yǔ)言搭建 驗(yàn)證模型，使用斷言來(lái)驗(yàn)證協(xié)議屬性或要求，能夠?qū)崿F(xiàn)部分形式化驗(yàn)證。最后 使用結(jié)構(gòu)覆蓋率和功能覆蓋率相結(jié)合的方法分析驗(yàn)證情況，使驗(yàn)證達(dá)到工程要 求。 關(guān)鍵詞：驗(yàn)證技術(shù)；功能驗(yàn)證；通信協(xié)議；斷言；隨機(jī)化 哈爾濱二r 程大學(xué)碩士學(xué)位論文 a b s t r a c t c h i pv e r i f i c a t i o np l a y sak e yp a r tt oi n c r e a s et h er a t i oo ft a p i n g o u ts u c c e s s f u l l y s o m ed a t ai n d i c a t et h a tt h em a j o rr e a s o nw h yt h er a t i oo ft a p i n g - o u ts u c c e s s f u l l y o n e t i m ei sb e l o w5 0 i st h a tf u n c t i o nv e r i f i c a t i o ni sn o tw e l ld o n e a c c o r d i n gt o v e r i f i e do b j e c t si nd i f f e r e n ta r e a sa n dv e r i f i e dm o d u l e si nd i f f e r e n tl e v e l s ，t h e r ea r e m a n yf u n c t i o nv e r i f i c a t i o nd i r e c t i o n s ，s u c ha sc p u ，o n - c h i pb u s ，m e m o r ya n ds oo i l s om a k i n gv e r i f i c a t i o ns t r a t e g i e sa n dm e t h o d sa c c o r d i n gt oi n v e s t i g a t e do b j e c t sh a sa g r e a tg u i d i n gs i g n i f i c a n c e g e n e r a l l y , c o m m u n i c a t i o nc h i p s h a v et h e s ef u n c t i o n s ：f r a m e e x c h a n g e ， r e t r a n s m i s s i o n ，c h a n n e lc o m p e t i t i o n ，b a c ko f fa n ds oo n b a s e do nt h e s ec h a r a c t e r s ， t e s tc a s e sm u s tb ed e s i g n e db ys i m u l a t i n gn e t w o r ke n v i r o n m e n ti nt h ef u n c t i o n v e r i f i c a t i o n n o t o n l y t h ec h i p p r o c e s s i n g c o n d i t i o n sa f t e r g e t t i n g c h a n n e l c o m p e t i t i o nb u ta l s ot h ec o m p l i c a t e dc o n d i t i o n so fm u l t i s t a t i o nc o m p e t i t i o na r e c o n t a i n e di nt h ev e r i f i c a t i o n o nt h e s er e q u i r e m e n t s ，p e r i o d so fv e r i f i c a t i o nm e t h o d a r ep r e s e n t e di nt h i st h e s i s w h i t eb o xv e r i f i c a t i o nm e t h o dw i t hs i n g l ed i r e c t i o nt e s t c a s e si st a k e ni nt h ef i r s tp e r i o d m u l t i s t a t i o nn e t w o r ke n v i r o n m e n ti ss i m u l a t e di n t h es e c o n dp e r i o d t e s tc a s e si m i t a t i n gt r a n s m i t t i n gu n d e rm u l t i s t a t i o nc o m p e t i t i o n a r ea d d e d t h en e x tt r a n s a c t i o ni st r i g g e r e db yt h er e s u l t sw h i c hg e n e r a t e db yt h e s t a t i o n s h a l fa u t o m a t i o ni si m p l e m e n t e db ys e l f - t r i g g e r e dc i r c u l a r l y a t p r e s e n t ，a b s t r a c t i o n , a u t o m a t i o n ，r e u s a b i l i t y a n d e a s y i n g t of o r m a l v e r i f i c a t i o na r et h ev e r i f i c a t i o nt e c h n i q u e s g o a l s i nt h i s t h e s i s ，r e s e a r c h o n c o m m u n i c a t i o nc h i p s v e r i f i c a t i o nm e t h o d ss t a r t sf r o mt h e s ea s p e c t st o o m u l t i - l e v e l h i e r a r c h yi sb u i l ti nt h ev e r i f i c a t i o n ，i n t e r f a c ep i n sa r ep a c k a g e da n df u n c t i o n sa r e a b s t r a c t e di n t ot r a n s a c t i o nl e v e l t e s tc a s e sa l eg e n e r a t e db yt h er a n d o mn u m b e r g e n e r a t o rw i t hc o n s t r a i n t s ，w h i c hi n c r e a s e st h ea u t o m a t i o no fv e r i f i c a t i o n e a c h m o d u l ei nt h ev e r i f i c a t i o nh i e r a r c h yi sf u n c t i o n - i n d e p e n d e n t i ti se a s yt ob er e u s e d i n t oo t h e rc o m m u n i c a t i o nc h i p s v e r i f i c a t i o no rn e x tg e n e r a t i o np r o d u c t s v e r i f i c a t i o n v e r i f i c a t i o nm o d u l e sa led e s c r i b e db ys y s t e m v e r i l o g ，a n dp r o t o c o lp r o p e r t i e sa n d r e q u k e m e n t sa r e v e r i f i e db ya s s e r t i o n s ，w h i c hc a nr e a l i z ef o r m a lv e r i f i c a t i o n 哈爾濱工程大學(xué)碩士學(xué)位論文 p a r t i a l l y f i n a l l y , s t r u c t u r ec o v e r a g ea n df u n c t i o nc o v e r a g er r ec o m b i n e dt oa n a l y z e t h ev e r i f i c a t i o n ，w h i c hc a l lm a k ev e r i f i c a t i o nm e e tt h ee n g i n e e r i n gr e q u i r e m e n t s k e y w o r d s ：v e r i f i c a t i o nt e c h n o l o g y ；f u n c t i o nv e r i f i c a t i o n ；c o m m t m i c a t i o n p r o t o c o l ；a s s e r t i o n ；r a n d o m i z a t i o n 哈爾濱工程大學(xué) 學(xué)位論文原創(chuàng)性2 聲明 本人鄭重聲明：本論文的所有工作，是在導(dǎo)師的指導(dǎo) 下，由作者本人獨(dú)立完成的。有關(guān)觀點(diǎn)、方法、數(shù)據(jù)和文 獻(xiàn)的引用已在文中指出，并與參考文獻(xiàn)相對(duì)應(yīng)。除文中已 注明引用的內(nèi)容外，本論文不包含任何其他個(gè)人或集體己 經(jīng)公開(kāi)發(fā)表的作品成果。對(duì)本文的研究做出重要貢獻(xiàn)的個(gè) 人和集體，均己在文中以明確方式標(biāo)明。本人完全意識(shí)到 本聲明的法律結(jié)果由本人承擔(dān)。 作者( 簽字) ：么捆 日期：d 咖莎年月廠萬(wàn)日 哈爾濱工程大學(xué)碩士學(xué)位論文 1 1 選題的目的和意義 第1 章緒論 由于信息技術(shù)的飛速發(fā)展，使得人們對(duì)網(wǎng)絡(luò)通信的需求也隨之不斷提高， 擁有更快的通信速度、更好的通信質(zhì)量、更大的通信流量、更便捷的通信方式， 這些都是目前網(wǎng)絡(luò)通信的研究方向。蜂窩移動(dòng)通信系統(tǒng)、無(wú)線局域網(wǎng)、藍(lán)牙技 術(shù)、家庭網(wǎng)絡(luò)、紅外線技術(shù)等移動(dòng)通信技術(shù)紛紛涌現(xiàn)。這些技術(shù)的出現(xiàn)，不僅 極大的方便人們的生活，同時(shí)也推動(dòng)了通信技術(shù)的發(fā)展。 由于硬件某些時(shí)候有比軟件速度更快等特點(diǎn)，使得集成電路設(shè)計(jì)廠商不斷 研制新的通信芯片和通信設(shè)備，比如無(wú)線通信網(wǎng)卡、手機(jī)芯片、交換機(jī)、路由 器等。由于這些通信產(chǎn)品或設(shè)備都具有收發(fā)、路由選擇等功能，使得他們具有 一些共性，那么在設(shè)計(jì)和驗(yàn)證這些通信芯片的過(guò)程中必然也有一些相近之處。 課題選擇對(duì)通信芯片進(jìn)行驗(yàn)證，是因?yàn)榇蟛糠滞ㄐ判酒甲袷豬 e e e 網(wǎng)絡(luò) 協(xié)議規(guī)范，根據(jù)網(wǎng)絡(luò)五層或七層結(jié)構(gòu)的特點(diǎn)來(lái)設(shè)計(jì)產(chǎn)品。在協(xié)議的控制下，兩 個(gè)對(duì)等實(shí)體間的通信使得本層能夠向上一層提供服務(wù)。要實(shí)現(xiàn)本層協(xié)議，還需 要使用下面一層所提供的服務(wù)。而芯片硬件設(shè)計(jì)的部分往往集中在物理層和數(shù) 據(jù)鏈路層，物理層的任務(wù)是透明地傳送比特流；數(shù)據(jù)鏈路層的任務(wù)是發(fā)送上層 交付的數(shù)據(jù)到物理層，接收下層提交的數(shù)據(jù)，分析幀內(nèi)數(shù)據(jù)和控制信息( 如同 步信息、地址信息、差錯(cuò)控制，以及流量控制信息) 等。目前對(duì)于通信芯片的 驗(yàn)證方法大多是采用功能驗(yàn)證中自盒測(cè)試與原型驗(yàn)證方法相結(jié)合。在白盒測(cè)試 中模擬網(wǎng)絡(luò)競(jìng)爭(zhēng)情況下的測(cè)試用例比較復(fù)雜，而使用原型驗(yàn)證方法往往由于硬 件平臺(tái)容量的限制，要同時(shí)模擬多個(gè)站點(diǎn)需要很多個(gè)原型板，增加了驗(yàn)證成本。 課題研究了目前的驗(yàn)證方法學(xué)，并分析其中的層次結(jié)構(gòu)和指導(dǎo)原則，針對(duì) 通信芯片的驗(yàn)證提出了驗(yàn)證平臺(tái)的搭建方法，該方法的意義主要體現(xiàn)在以下五 個(gè)方面。 第一，采用基于斷言的驗(yàn)證方法，把斷言插入到設(shè)計(jì)中去，便于隨時(shí)隨處 檢查砌m 代碼功能及時(shí)序。它可以檢查一些邊角情況，為驗(yàn)證人員提高覆蓋率 提供了捷徑。 哈爾濱工程大學(xué)碩士學(xué)位論文 第二，采用抽象化的層次結(jié)構(gòu)搭建驗(yàn)證平臺(tái)，具有封裝，繼承，遞歸等面 向?qū)ο筇匦?。一旦低層次的功能得到?yàn)證，就能借助于層次結(jié)構(gòu)化的測(cè)試平臺(tái) 在更高的層面上進(jìn)行驗(yàn)證工作，突破了總線功能模型很難添加新的協(xié)議層的單 一結(jié)構(gòu)特點(diǎn)。 第三，采用單向測(cè)試激勵(lì)觸發(fā)和雙向循環(huán)觸發(fā)網(wǎng)絡(luò)相結(jié)合的驗(yàn)證策略，使 驗(yàn)證更加全面，驗(yàn)證平臺(tái)更能測(cè)試出真實(shí)網(wǎng)絡(luò)競(jìng)爭(zhēng)環(huán)境下芯片的功能。 第四，使用隨機(jī)仿真模擬自動(dòng)化。精心設(shè)計(jì)信號(hào)源，使隨機(jī)激勵(lì)生成一些 目前也許還不能預(yù)知的有顯著意義的測(cè)試信號(hào)和條件。當(dāng)隨機(jī)激勵(lì)源不能生成 所需的激勵(lì)信號(hào)時(shí)，或者所需的激勵(lì)不能用無(wú)側(cè)重的隨機(jī)信號(hào)源來(lái)產(chǎn)生時(shí)，可 以對(duì)激勵(lì)信號(hào)源施加約束，產(chǎn)生人為規(guī)定的激勵(lì)概率( 一般為1 0 0 ) 。 第五，層次結(jié)構(gòu)分明，使得功能模型和實(shí)例化模型分開(kāi)，便于重用功能模 型。對(duì)于通信芯片而言，由于其共有許多功能特性，使得驗(yàn)證平臺(tái)的移植、重 用功能模型具有更加重要的意義。 綜上，研究目前正在火熱發(fā)展的通信芯片的共有特性，并針對(duì)這些特性來(lái) 說(shuō)明采用驗(yàn)證方法學(xué)的指導(dǎo)思想來(lái)搭建驗(yàn)證平臺(tái)是具有很大意義的。 1 2 目前驗(yàn)證技術(shù)研究現(xiàn)狀 集成電路驗(yàn)證研究?jī)?nèi)容很多，如：口核模塊級(jí)驗(yàn)證( b l o c k l e v e l v e r i f i c a t i o n ) 、仿真驗(yàn)證( s i m u l a t i o n ) 、系統(tǒng)級(jí)驗(yàn)證( s y s t e m l e v e lv e r i f i c a t i o n ) 、 軟硬件協(xié)同驗(yàn)證( h a r d w a r e s o f t w a r ec o v e r i f i c a t i o n ) 、快速原型驗(yàn)證( r a p i d s y s t e mp r o t o t y p e ) 、等價(jià)性檢查( e q u i v a l e n tc h e c k i n g ) 、靜態(tài)時(shí)序分析和時(shí)序 驗(yàn)證( s t a t i ct i m i n ga n a l y s i s & t i m i n gv e r i f i c a t i o n ) 、物理驗(yàn)證( p h y s i c a l v e r i f i c a t i o n ) 等。隨著驗(yàn)證技術(shù)的逐步發(fā)展，驗(yàn)證方法由最初的直接測(cè)試向量 生成( d i r e c t e dt e s tv e c t o rg e n e r a t i o n ) ，到約束隨機(jī)測(cè)試( c o n s t r a i n t e dr a n d o m t e s t ) ，再到覆蓋率驅(qū)動(dòng)驗(yàn)h 正( c o v e r a g e d r i v e nv e r i f i c a t i o n ) ，一直到最新的基于 斷言的驗(yàn)證方法( a s s e r t i o n - b a s e dv e r i f i c a t i o n ) ，各種驗(yàn)證方法都在不斷創(chuàng)新發(fā) 展。 芯片驗(yàn)證的任務(wù)包括對(duì)設(shè)計(jì)的驗(yàn)證和對(duì)實(shí)現(xiàn)的驗(yàn)證f 1 j 。對(duì)設(shè)計(jì)的驗(yàn)證是檢 查設(shè)計(jì)的描述是否與設(shè)計(jì)要求一致；對(duì)實(shí)現(xiàn)的驗(yàn)證是檢查綜合后的電路結(jié)構(gòu)是 2 哈爾濱工程大學(xué)碩士學(xué)位論文 否與抽象層次的設(shè)計(jì)一致。前者主要側(cè)重于功能驗(yàn)證，采用軟件搭建驗(yàn)證平臺(tái) 進(jìn)行驗(yàn)證和基于f p g a 的模擬驗(yàn)證。而后者大部分為等價(jià)性檢驗(yàn)。 由于功能驗(yàn)證是設(shè)計(jì)過(guò)程中比較重要的步驟，對(duì)檢驗(yàn)設(shè)計(jì)起到關(guān)鍵的作 用，因此它也成為目前驗(yàn)證工程師和學(xué)術(shù)界研究的熱點(diǎn)。功能驗(yàn)證用于檢查集 成電路設(shè)計(jì)是否符合設(shè)計(jì)計(jì)劃制定的功能要求。正在發(fā)展和使用的功能驗(yàn)證方 法有如下幾種： 1 ) 基于總線結(jié)構(gòu)的驗(yàn)證方法。開(kāi)發(fā)各種總線功能模型( b f m ) ，這些模 塊具有可重用性，可以移植或嵌入到驗(yàn)證平臺(tái)中。 2 ) 覆蓋率觸發(fā)的驗(yàn)證方法。根據(jù)工具提供的代碼覆蓋率，分支覆蓋率等 信息評(píng)佶驗(yàn)證策略，指導(dǎo)驗(yàn)證過(guò)程和測(cè)試用例的范圍。 3 ) 基于斷言的驗(yàn)證方法i 硼。使用斷言可以很方便的對(duì)一個(gè)給定輸入設(shè)計(jì)的 期望行為進(jìn)行精確的描述，從而可以很方便的描述輸入輸出行為、總線協(xié)議以 及設(shè)計(jì)中的一些復(fù)雜的關(guān)系。 另外還有動(dòng)態(tài)模擬、形式驗(yàn)證、軟硬件協(xié)同驗(yàn)證等方法，都是驗(yàn)證人員經(jīng) 常使用的驗(yàn)證方法。 1 3 課題的主要研究?jī)?nèi)容 課題是結(jié)合了目前正在發(fā)展的各種驗(yàn)證技術(shù)，以驗(yàn)證方法學(xué)為指導(dǎo)，采用 s y s t e m v e r i l o g 語(yǔ)言來(lái)搭建驗(yàn)證平臺(tái)，驗(yàn)證通信芯片。通過(guò)對(duì)一個(gè)符合無(wú)線通信 協(xié)議8 0 2 1l b 的設(shè)計(jì)模型來(lái)搭建驗(yàn)證平臺(tái)的方法來(lái)說(shuō)明此驗(yàn)證方法的益處。驗(yàn) 證結(jié)果表明該驗(yàn)證方法達(dá)到了預(yù)期的目的，使驗(yàn)證平臺(tái)具有較好的驗(yàn)證覆蓋率， 很高的可重用性，較少的驗(yàn)證代碼量。 主要的研究?jī)?nèi)容有以下幾個(gè)方面。 1 ) 詳細(xì)分析當(dāng)前常用的芯片驗(yàn)證技術(shù)及其特點(diǎn)，研究正在發(fā)展的驗(yàn)證方 法?？偨Y(jié)目前驗(yàn)證通信芯片的方法，并分析他們的優(yōu)缺點(diǎn)。 2 ) 對(duì)通信芯片的設(shè)計(jì)進(jìn)行研究，分析其協(xié)議規(guī)范，研究他們?cè)谑瞻l(fā)幀、 競(jìng)爭(zhēng)退避等方法中數(shù)據(jù)的傳輸和控制功能的設(shè)計(jì)共性。通過(guò)歸納通信芯片所共 有的這些特性，設(shè)計(jì)了一個(gè)擁有上述共性的通信芯片，它符合i e e e 8 0 2 1 1 b 協(xié) 議i b s s 模式下的通信方式。具有檢測(cè)信道回避碰撞、支持節(jié)能方式、a e k 應(yīng)答 機(jī)制及支持可重傳等功能。片內(nèi)采用a r m 公司的高速a h b 總線作為連接控制模 3 哈爾濱工程大學(xué)碩士學(xué)位論文 塊和存儲(chǔ)器等模塊的總線。 3 ) 對(duì)通信芯片的設(shè)計(jì)進(jìn)行驗(yàn)證：提出了基于抽象化層次結(jié)構(gòu)的驗(yàn)證環(huán)境 搭建方法。該層次結(jié)構(gòu)包括信號(hào)層、功能層、場(chǎng)景層等。每一層都對(duì)應(yīng)不同的 抽象層次，高層次具有很高的事務(wù)抽象層次，便于在高層次加入事務(wù)級(jí)的測(cè)試 用例。根據(jù)層次結(jié)構(gòu)各模塊的可重用性，提出在測(cè)試過(guò)程采用單向測(cè)試激勵(lì)和 雙向自觸發(fā)激勵(lì)的方法相結(jié)合。單向測(cè)試即為在上層施加激勵(lì)，檢測(cè)被測(cè)設(shè)計(jì) 的結(jié)果是否符合設(shè)計(jì)的要求，但這種情況對(duì)于信道的競(jìng)爭(zhēng)和退避不能做到隨機(jī) 化。因而采用雙向自觸發(fā)的方法對(duì)上述情況進(jìn)行補(bǔ)充測(cè)試，使驗(yàn)證更加全面和 隨機(jī)化。 4 ) 產(chǎn)生測(cè)試用例采用加約束的隨機(jī)數(shù)生成方法，實(shí)現(xiàn)了測(cè)試的半自動(dòng)化。 采用基于覆蓋功能點(diǎn)和基于斷言相結(jié)合的功能覆蓋率統(tǒng)計(jì)方法，并根據(jù)工具提 供的結(jié)構(gòu)覆蓋率和驗(yàn)證人員編寫的驗(yàn)證環(huán)境產(chǎn)生的功能覆蓋率來(lái)分析驗(yàn)證工作 的情況，提出基于各種覆蓋率結(jié)果不高的改進(jìn)方法，通過(guò)逐漸完善驗(yàn)證環(huán)境或 者修改設(shè)計(jì)來(lái)使覆蓋率達(dá)到設(shè)計(jì)要求。 1 4 論文的結(jié)構(gòu) 論文的結(jié)構(gòu)安排如下： 第一章說(shuō)明課題的目的和意義，并介紹目前驗(yàn)證技術(shù)的研究現(xiàn)狀。闡述了 課題的主要研究?jī)?nèi)容以及論文的結(jié)構(gòu)安排。 第二章介紹驗(yàn)證技術(shù)的相關(guān)知識(shí)，詳細(xì)分析了驗(yàn)證的常用技術(shù)、方法、驗(yàn) 證策略，以及驗(yàn)證技術(shù)的發(fā)展趨勢(shì)。說(shuō)明了目前對(duì)于通信芯片采用的驗(yàn)證方法 和策略，并總結(jié)這些方法的特點(diǎn)。 第三章分析通信協(xié)議的發(fā)展趨勢(shì)，總結(jié)通信芯片設(shè)計(jì)共有的功能特性，針 對(duì)這些特性設(shè)計(jì)了符合8 0 2 1 1 b 協(xié)議的i b s s 模式下通信規(guī)范的設(shè)計(jì)模型。該模 型具有基本收發(fā)數(shù)據(jù)幀、隨機(jī)退避算法競(jìng)爭(zhēng)信道、支持節(jié)能方式、支持重傳功 能等通信芯片的特點(diǎn)。 ， 第四章為通信芯片的設(shè)計(jì)模型搭建層次化的驗(yàn)證平臺(tái)，采用單向觸發(fā)和雙 向自觸發(fā)的驗(yàn)證策略，把驗(yàn)證工作分為兩個(gè)階段，兩個(gè)階段的模塊移植性和重 用性很強(qiáng)，不需要編寫大量的重復(fù)代碼，而且可以達(dá)到很高的隨機(jī)化測(cè)試用例 的生成，使驗(yàn)證更加接近真實(shí)環(huán)境。采用了功能覆蓋率和結(jié)構(gòu)覆蓋率統(tǒng)一的分 4 哈爾濱工程大學(xué)碩士學(xué)位論文 析方法，根據(jù)得到的不同結(jié)果更改驗(yàn)證的測(cè)試用例，逐步完善測(cè)試用例，使其 達(dá)到驗(yàn)證要求的覆蓋率。根據(jù)實(shí)驗(yàn)結(jié)果分析，這種針對(duì)通信芯片的驗(yàn)證方法不 僅減少了驗(yàn)證代碼的編寫，提高了驗(yàn)證工作進(jìn)展的速度，而且加約束的隨機(jī)化 提高了芯片功能驗(yàn)證的效率。 結(jié)論是對(duì)課題研究?jī)?nèi)容的總結(jié)，并對(duì)通信芯片驗(yàn)證工作的發(fā)展趨勢(shì)進(jìn)行討 論，指出下一步需要研究的內(nèi)容，以及課題設(shè)計(jì)和研究的不足之處。 5 哈爾濱工程大學(xué)碩士學(xué)位論文 第2 章集成電路驗(yàn)證方法和技術(shù)的研究 驗(yàn)證是集成電路設(shè)計(jì)工作中十分重要的一環(huán)，電路規(guī)模越大系統(tǒng)越復(fù)雜， 占用驗(yàn)證時(shí)間越長(zhǎng)。目前集成電路的驗(yàn)證方法和技術(shù)不斷更新和發(fā)展，不斷完 善了驗(yàn)證方法學(xué)的體系結(jié)構(gòu)和內(nèi)容。 2 1 驗(yàn)證流程 目前的驗(yàn)證工作大體分以下幾個(gè)層次：系統(tǒng)驗(yàn)證，功能驗(yàn)證，邏輯驗(yàn)證， 版圖驗(yàn)證。 2 1 1 基本的驗(yàn)證工作層次 基本的驗(yàn)證工作層次如圖2 1 所示。在芯片設(shè)計(jì)的過(guò)程中，每一個(gè)層次都 要進(jìn)行驗(yàn)證，驗(yàn)證工作是對(duì)設(shè)計(jì)的保障。在各層次驗(yàn)證的手段和目的不同，采 用的方法也不同。由于驗(yàn)證層次的差異使得驗(yàn)證工作的流程也不相同舊。 l 設(shè)計(jì)規(guī)倍 1 l 刊 ，+ 系統(tǒng)設(shè)計(jì)和描述 系統(tǒng)驗(yàn)證hl 系統(tǒng)劃分 ， 子系統(tǒng)功能描述 功能驗(yàn)證卜一； 綜合 ， 邏輯描述 邏輯驗(yàn)證h1 版圖綜合 ，t 版圖描述 版圖驗(yàn)證hl 芯片 圖2 1 基本驗(yàn)證層次示意圖 6 哈爾濱工程大學(xué)碩士學(xué)位論文 2 1 2 驗(yàn)證工作的流程 從圖2 1 可以看出驗(yàn)證工作分段獨(dú)立是很明顯的特征。每個(gè)任務(wù)都在其階 段使用獨(dú)立的工具、環(huán)境、用戶接口和模型。由于驗(yàn)證的目的不同使得縱向的 復(fù)用是有限的或者基本不可能。有些相同的信息在每一層都有，而這些信息在 這一階段的驗(yàn)證后就不再被使用了。 分段獨(dú)立的特性也存在于工程與工程之間，很少有公司有一個(gè)對(duì)于所有工 程都適用的通用驗(yàn)證環(huán)境。一旦派生出新的工程，就需要建立新的驗(yàn)證環(huán)境。 因?yàn)槊總€(gè)工程都各不相同，重用模型或信息是不可能的。 驗(yàn)證被認(rèn)為是設(shè)計(jì)的一部分f f - a l 。驗(yàn)證策略也是由設(shè)計(jì)小組來(lái)制定，傳統(tǒng)的 驗(yàn)證工作在代碼完成后才開(kāi)始，由設(shè)計(jì)人員來(lái)寫驗(yàn)證代碼。這種方法適合于小 規(guī)模設(shè)計(jì)，驗(yàn)證只占據(jù)整個(gè)設(shè)計(jì)很小的比例。隨著設(shè)計(jì)規(guī)模的增加j 復(fù)雜性的 增大，驗(yàn)證已經(jīng)占據(jù)設(shè)計(jì)中很大的比例。開(kāi)發(fā)人員已經(jīng)意識(shí)到驗(yàn)證必須作為獨(dú) 立的開(kāi)發(fā)工作來(lái)做了。 把驗(yàn)證過(guò)程從設(shè)計(jì)過(guò)程中獨(dú)立出來(lái)不僅提高了工程效率，也提高了工作質(zhì) 量。當(dāng)前的大規(guī)模設(shè)計(jì)不僅需要多重復(fù)雜的測(cè)試激勵(lì)，而且需要不同層次的集 合。在設(shè)計(jì)之后才開(kāi)始驗(yàn)證工作增加了開(kāi)發(fā)時(shí)間。把驗(yàn)證工作獨(dú)立出來(lái)，使他 并行于設(shè)計(jì)過(guò)程，在設(shè)計(jì)工作進(jìn)行的時(shí)候就開(kāi)始設(shè)計(jì)驗(yàn)證平臺(tái)，在設(shè)計(jì)工作結(jié) 束后可以立即執(zhí)行驗(yàn)證平臺(tái)來(lái)驗(yàn)證設(shè)計(jì)。 項(xiàng)目設(shè)計(jì)人員通常描述設(shè)計(jì)和驗(yàn)證的軟件和硬件流程如圖2 2 所示“v 字 型結(jié)構(gòu)。在設(shè)計(jì)流程中，工程是從設(shè)計(jì)開(kāi)始，設(shè)計(jì)結(jié)束后是測(cè)試和驗(yàn)證，設(shè)計(jì) 從高級(jí)系統(tǒng)級(jí)設(shè)計(jì)到低級(jí)芯片到模塊級(jí)，然后在集成在一起。驗(yàn)證是從模塊級(jí) 到芯片級(jí)再到系統(tǒng)級(jí)的層次。 系統(tǒng) 集成 圖2 2 傳統(tǒng)的驗(yàn)證工作進(jìn)展情況 7 統(tǒng)驗(yàn)證系 芷 系 靴 嘶瓤 | 馴 c 哈爾濱工程大學(xué)碩士學(xué)位論文 目前的高級(jí)驗(yàn)證流程改變了傳統(tǒng)“v ”字型的結(jié)構(gòu)。在基本的“v ”字型結(jié) 構(gòu)中，驗(yàn)證任務(wù)包括設(shè)計(jì)測(cè)試用倒，編寫測(cè)試代碼，運(yùn)行和調(diào)試測(cè)試環(huán)境。所 有的這些任務(wù)都等待設(shè)計(jì)集成的完成，整個(gè)流程是線性的。高級(jí)驗(yàn)證流程的方 法使測(cè)試用例和驗(yàn)證環(huán)境的開(kāi)發(fā)平行于設(shè)計(jì)的開(kāi)發(fā)，所以在設(shè)計(jì)完成后就可以 進(jìn)行調(diào)試工作。如圖2 3 所示高級(jí)驗(yàn)證流程。 系統(tǒng)設(shè)計(jì) 集成 統(tǒng)測(cè)試 圖2 3 高級(jí)驗(yàn)證流程 從圖2 3 中可以清晰看出，采用高級(jí)的驗(yàn)證流程，不僅沒(méi)有影響驗(yàn)證質(zhì)量， 而使得項(xiàng)目完成時(shí)間大大縮短。 2 2 驗(yàn)證方法 根據(jù)驗(yàn)證階段的不同和驗(yàn)證對(duì)象的差異，采用的驗(yàn)證方法是不同的。歸納 起來(lái)，功能驗(yàn)證的方法有三種：黑盒法、自盒法和灰盒法陋t 。 1 ) 黑盒法 黑盒驗(yàn)證的示意圖如圖2 4 所示。它不考慮設(shè)計(jì)內(nèi)部的實(shí)現(xiàn)細(xì)節(jié)，所有驗(yàn)證 的內(nèi)容都是通過(guò)設(shè)計(jì)對(duì)外接口完成的。被驗(yàn)證的黑盒可以是整個(gè)系統(tǒng)，- 二個(gè)芯 片，一個(gè)芯片的一個(gè)單元，也可能是一個(gè)模塊。驗(yàn)證工程師不關(guān)心設(shè)計(jì)的內(nèi)部 結(jié)構(gòu)和設(shè)計(jì)內(nèi)部的狀態(tài)，只需要根據(jù)輸入預(yù)測(cè)出輸出，然后與黑盒的輸出進(jìn)行 比較即可。 黑盒驗(yàn)證的優(yōu)點(diǎn)是測(cè)試用例獨(dú)立于設(shè)計(jì)實(shí)現(xiàn)，有利于設(shè)計(jì)和驗(yàn)證分離，讓 驗(yàn)證工程師在不了解設(shè)計(jì)實(shí)現(xiàn)的情況下，從設(shè)計(jì)規(guī)格出發(fā)去檢查被測(cè)電路，這 樣有利于不受設(shè)計(jì)的思維限制，增加驗(yàn)證的可信度，缺點(diǎn)是出現(xiàn)錯(cuò)誤很難定位， 缺乏可觀察性。 8 哈爾濱 t 程大學(xué)碩士學(xué)位論文 l l l i i i l 圖2 4 黑盒驗(yàn)證示意圖 2 ) 白盒法 白盒驗(yàn)證的示意圖如圖2 5 所示，它要求對(duì)所要驗(yàn)證的設(shè)計(jì)內(nèi)部結(jié)構(gòu)和實(shí) 現(xiàn)細(xì)節(jié)都非常清楚，驗(yàn)證的內(nèi)容包括設(shè)計(jì)內(nèi)部的狀態(tài)機(jī)、觸發(fā)器、存儲(chǔ)器等， 并可以對(duì)設(shè)計(jì)內(nèi)部進(jìn)行完全的控制和觀測(cè)【l j 。 l l i i i i l 一一。i 圖2 5 自盒驗(yàn)證示意圖 這種方法的優(yōu)點(diǎn)是可以迅速建立想要的電路狀態(tài)，隔離特定的功能，能夠 很容易地觀察設(shè)計(jì)每個(gè)部分對(duì)激勵(lì)的響應(yīng)情況，及時(shí)報(bào)告驗(yàn)證結(jié)果與預(yù)期結(jié)果 的差異。缺點(diǎn)在于需要驗(yàn)證工程師知道設(shè)計(jì)實(shí)現(xiàn)的細(xì)節(jié)，容易落入通過(guò)實(shí)現(xiàn)過(guò) 程來(lái)設(shè)計(jì)測(cè)試激勵(lì)的思維定式中i l o j 。 3 ) 灰盒法 灰盒驗(yàn)證是黑盒驗(yàn)證和白盒驗(yàn)證的折衷，是在知道設(shè)計(jì)細(xì)節(jié)的情況下采用 9 哈爾濱工程大學(xué)碩士學(xué)位論文 黑盒驗(yàn)證的測(cè)試用例。它不僅調(diào)試效率比黑盒驗(yàn)證高，又能對(duì)設(shè)計(jì)內(nèi)部進(jìn)行控 制和觀察，易于錯(cuò)誤定位，而且具有很好的移植性?；液序?yàn)證測(cè)試的方式同黑 盒驗(yàn)證一樣也是通過(guò)設(shè)計(jì)的對(duì)外接口、特殊引腳或性能寄存器、測(cè)試寄存器等 輸出結(jié)果判斷設(shè)計(jì)的正確性。 2 3 驗(yàn)證策略 單元驗(yàn)證要驗(yàn)證的模塊很小或者功能單一，因此它的驗(yàn)證策略比較簡(jiǎn)單。 只要結(jié)合驗(yàn)證功能編寫測(cè)試用例即可。系統(tǒng)驗(yàn)證的策略有以下幾種：自頂向下 的驗(yàn)證、自底向上的驗(yàn)證、基于平臺(tái)的驗(yàn)證和基于系統(tǒng)接口的驗(yàn)證。 1 ) 自頂向下的驗(yàn)證 一般的驗(yàn)證策略都是采用自頂向下的驗(yàn)證方法，如圖2 6 所示。 圖2 6 自項(xiàng)向f 的驗(yàn)證 驗(yàn)證工作首先研究開(kāi)發(fā)要求，制定系統(tǒng)規(guī)范，然后并行于系統(tǒng)設(shè)計(jì)的驗(yàn)證 工作為系統(tǒng)級(jí)驗(yàn)證，它從系統(tǒng)規(guī)范中提取出設(shè)計(jì)所需要驗(yàn)證的所有特性。把這 些特性結(jié)合系統(tǒng)規(guī)范，制定出詳細(xì)的驗(yàn)證計(jì)劃。系統(tǒng)驗(yàn)證的主要內(nèi)容包括建立 系統(tǒng)行為模型并把它放到系統(tǒng)級(jí)的測(cè)試環(huán)境中進(jìn)行驗(yàn)證。系統(tǒng)級(jí)的測(cè)試環(huán)境應(yīng) 該是模塊化的，可以很方便的移植到對(duì)設(shè)計(jì)的功能驗(yàn)證和網(wǎng)表驗(yàn)證，對(duì)于不同 1 n 哈爾濱工程大學(xué)碩士學(xué)位論文 的抽象層次可根據(jù)該層次的具體要求增強(qiáng)相應(yīng)的測(cè)試功能。利用基于事務(wù)的模 擬技術(shù)建立系統(tǒng)級(jí)測(cè)試環(huán)境，一方面它可以很方便地進(jìn)行系統(tǒng)級(jí)的驗(yàn)證，另一 方面可以直接用于對(duì)設(shè)計(jì)頂層模塊間直接連接關(guān)系的驗(yàn)證，從系統(tǒng)級(jí)驗(yàn)證移植 到功能驗(yàn)證，這樣的系統(tǒng)級(jí)測(cè)試環(huán)境只需相應(yīng)的總線功能模型代替基于指令的 或基于事務(wù)的數(shù)據(jù)模型即可1 9 1 。在綜合、芯片的布局布線設(shè)計(jì)要通過(guò)網(wǎng)表驗(yàn)證 來(lái)保證質(zhì)量，一般既可以采用形式驗(yàn)證手段，也可以采用門級(jí)模擬的手段來(lái)驗(yàn) 證設(shè)計(jì)的綜合實(shí)現(xiàn)和物理實(shí)現(xiàn)是否正確。驗(yàn)證的最后一階段是用時(shí)序分析和物 理驗(yàn)證來(lái)確保芯片的正確性。 2 ) 自底向上的驗(yàn)證 自底向上的驗(yàn)證如圖2 7 所示。這種方法的驗(yàn)證首先針對(duì)設(shè)計(jì)輸入的每個(gè) 模塊獨(dú)立進(jìn)行0 級(jí)驗(yàn)證，一在0 級(jí)驗(yàn)證無(wú)誤后針對(duì)設(shè)計(jì)輸入的模塊間內(nèi)部連接進(jìn) 行1 級(jí)驗(yàn)證，成功后針對(duì)設(shè)計(jì)輸入的功能和接口實(shí)現(xiàn)2 級(jí)驗(yàn)證，最后上升到驗(yàn) 證系統(tǒng)級(jí)功能的3 級(jí)驗(yàn)證工作階段o 在全面的芯片功能驗(yàn)證后，對(duì)布局布線后 的綜合設(shè)計(jì)進(jìn)行網(wǎng)表驗(yàn)證，最后是物理驗(yàn)證。 其中0 至3 級(jí)驗(yàn)證內(nèi)容如下： 圖2 7 官底向上的驗(yàn)證 哈爾濱工程大學(xué)碩十學(xué)位論文 0 級(jí)驗(yàn)證由設(shè)計(jì)工程師負(fù)責(zé)，進(jìn)行仔細(xì)的模塊驗(yàn)證( 包括直接驗(yàn)證和隨機(jī) 驗(yàn)證) 。設(shè)計(jì)工程師提交給驗(yàn)證工程師的設(shè)汁一方面要通過(guò)代碼質(zhì)量檢查( 其內(nèi) 容包括沒(méi)有初始化的變量、綜合器不支持的數(shù)據(jù)類型或行為級(jí)描述、模塊例化 時(shí)端口不匹配等) ：另一方面要通過(guò)測(cè)試覆蓋率檢查，保證行測(cè)試覆蓋率達(dá)到 1 0 0 。對(duì)礤宏模塊的測(cè)試，測(cè)試的環(huán)境有口提供者給出，測(cè)試的結(jié)果可以作 為口選擇的依據(jù)i 0 1 。 1 級(jí)驗(yàn)證用于驗(yàn)證系統(tǒng)存儲(chǔ)器的映射和模塊間互聯(lián)的正確性。測(cè)試內(nèi)容包 括通過(guò)片上處理器或片外處理器模型對(duì)設(shè)計(jì)各個(gè)模塊中的寄存器進(jìn)行讀寫操 作，對(duì)于設(shè)計(jì)中的每個(gè)數(shù)據(jù)通路，通過(guò)外部接口寫入激勵(lì)數(shù)據(jù)，經(jīng)過(guò)設(shè)計(jì)中各 個(gè)模塊間的接口傳送，在設(shè)計(jì)的輸出端口采集結(jié)果。驗(yàn)證系統(tǒng)存儲(chǔ)器映射和設(shè) 計(jì)對(duì)象的內(nèi)部互連關(guān)系。這些測(cè)試可以手工建立，也可以由工具在讀入系統(tǒng)級(jí) 互連關(guān)系和存儲(chǔ)器映射關(guān)系之后自動(dòng)生成。 2 級(jí)驗(yàn)證主要驗(yàn)證設(shè)計(jì)對(duì)象的基本功能和外部互連關(guān)系。編寫的測(cè)試都是 用來(lái)檢驗(yàn)每一個(gè)功能塊的主要功能路徑和每一個(gè)i o 引腳。 3 級(jí)驗(yàn)證主要是驗(yàn)證整個(gè)芯片的系統(tǒng)功能。傳統(tǒng)的方法是采用窮舉式對(duì)集 成后的設(shè)計(jì)對(duì)象進(jìn)行功能測(cè)試?，F(xiàn)在可以采用加約束的隨機(jī)化方法將測(cè)試集進(jìn) 行分類命中，減少測(cè)試用例的運(yùn)行。在編寫測(cè)試用例時(shí)特別考慮那些邊角情況、 邊界情況、設(shè)計(jì)間斷點(diǎn)、錯(cuò)誤條件和異常處理，以確保測(cè)試全面。 3 ) 基于平臺(tái)的驗(yàn)證一 一一一一一一一一一一一一一一一一一一一、 圖2 8 基于平臺(tái)的驗(yàn)證 1 2 哈爾濱工烈大學(xué)碩十學(xué)位論文 基于平臺(tái)的驗(yàn)證如圖2 8 所示。這種驗(yàn)證方法一般適用于可移植的驗(yàn)證平 臺(tái)的再次驗(yàn)證。其中可移植的平臺(tái)是已經(jīng)驗(yàn)證過(guò)的，開(kāi)發(fā)過(guò)程中集成的硬件 和軟件i p 也是驗(yàn)證過(guò)的。驗(yàn)證的內(nèi)容主要是開(kāi)發(fā)平臺(tái)和新增加i p 模塊之間的 接口。 4 ) 基于系統(tǒng)接口的驗(yàn)證 基于系統(tǒng)接口的驗(yàn)證如圖2 9 所示。它是指在系統(tǒng)設(shè)計(jì)階段對(duì)設(shè)計(jì)對(duì)象中 所使用的功能模塊在其接口層次上進(jìn)行抽象，建立相應(yīng)的接口模型。這種接口 模型可以幫助設(shè)計(jì)工程師對(duì)模塊進(jìn)行充分驗(yàn)證，驗(yàn)證工程師也可以很方便地進(jìn) 行模塊間互連關(guān)系的驗(yàn)證和系統(tǒng)功能模擬。常見(jiàn)的接口包括基于片上總線的接 口，基于存儲(chǔ)器讀寫的接口等。 圖2 9 基于系統(tǒng)接口的驗(yàn)證 驗(yàn)證策略要隨著設(shè)計(jì)而制定。有時(shí)要采用幾種策略相結(jié)合的方法進(jìn)行驗(yàn) 證。由于軟件可以實(shí)現(xiàn)抽象級(jí)別較高的事務(wù)級(jí)功能模擬，所以有時(shí)也可以通過(guò) 編寫軟件程序來(lái)代替某些硬件環(huán)境，和硬件電路設(shè)計(jì)同時(shí)運(yùn)行進(jìn)行驗(yàn)證。 2 4 驗(yàn)證技術(shù) 目前正在發(fā)展的驗(yàn)證技術(shù)有如下幾種： 1 ) 基于事件的模擬 這種方法把輸入激勵(lì)的任何一個(gè)變化都視為一個(gè)事件，每一個(gè)模擬時(shí)間模 擬器處理一個(gè)事件1 1 3 l 。每發(fā)生一個(gè)事件，就對(duì)整個(gè)設(shè)計(jì)重新進(jìn)行計(jì)算直到模擬 出現(xiàn)穩(wěn)定狀態(tài)為止。如果輸入信號(hào)在一個(gè)時(shí)鐘周期內(nèi)到達(dá)，但是不同的輸入信 號(hào)到達(dá)的時(shí)間不盡相同，則基于事件的模擬機(jī)制決定模擬器在一個(gè)時(shí)鐘周期內(nèi) 計(jì)算多次。 1 3 哈爾濱工程大學(xué)碩士學(xué)位論文 基于事件的模型包括時(shí)序模型和功能模型。基于事件的模擬同時(shí)覆蓋了設(shè) 計(jì)的功能和時(shí)序模型，模擬結(jié)果精確，便于檢測(cè)出設(shè)計(jì)對(duì)象中的毛刺，尤其適 用于異步電路的模擬。缺點(diǎn)是模擬速度取決于設(shè)計(jì)對(duì)象的規(guī)模和模擬中行為的 抽象層次，如果設(shè)計(jì)對(duì)象規(guī)模很大，那么其模擬將會(huì)很慢。另外，因?yàn)榛谑?件的模擬器使用復(fù)雜算法調(diào)度各個(gè)事件，并且需要多次計(jì)算輸出量，模擬的速 度受到一定限制。 2 ) 基于周期的模擬 基于周期的模擬在時(shí)鐘周期內(nèi)沒(méi)有時(shí)間概念，它只在時(shí)鐘的上升沿或下降 沿進(jìn)行觸發(fā)，每一個(gè)時(shí)鐘周期的時(shí)間對(duì)電路計(jì)算一次。基于周期的模擬器只對(duì) 同步設(shè)計(jì)有效。 因?yàn)槊恳粋€(gè)邏輯元素在每個(gè)周期中只計(jì)算一次，基于周期的模擬顯著的提 高了模擬執(zhí)行的速度。它所提供的模擬速度是基于事件的模擬器的5 1 0 0 倍。 對(duì)于大型設(shè)計(jì)，模擬速度可以提高到每秒1 0 0 0 個(gè)時(shí)鐘周期 1 4 1 。最適用于那些需 要大型模擬向量的設(shè)計(jì)對(duì)象，如微處理器、專用集成芯片和系統(tǒng)芯片。它的缺 點(diǎn)是，因?yàn)樗豁憫?yīng)時(shí)鐘信號(hào)而無(wú)法檢測(cè)出設(shè)計(jì)對(duì)象中的毛刺。另外，它沒(méi)有 將設(shè)計(jì)對(duì)象的時(shí)序納入考慮范圍，因此需要使用時(shí)序靜態(tài)分析工具來(lái)進(jìn)行時(shí)序 驗(yàn)證。 3 ) 基于事務(wù)的驗(yàn)證 事務(wù)就是設(shè)計(jì)對(duì)象與事務(wù)處理器之間通過(guò)接口所作的一次數(shù)據(jù)或控制的傳 輸。事務(wù)可以是一個(gè)簡(jiǎn)單事務(wù)，如讀取某個(gè)存儲(chǔ)器單元，也可以是一個(gè)復(fù)雜事 物，如傳輸整個(gè)結(jié)構(gòu)式數(shù)據(jù)報(bào)文。 基于事務(wù)的驗(yàn)證對(duì)每個(gè)設(shè)計(jì)都要求有總線功能模型。總線功能模型采用常 用的驗(yàn)證語(yǔ)言來(lái)編寫，為在設(shè)計(jì)對(duì)象的硬件接口上運(yùn)行事務(wù)提供了一種手段。 它根據(jù)接口協(xié)議的要求來(lái)驅(qū)動(dòng)各個(gè)互連線信號(hào)，只檢測(cè)元件之間的事務(wù)i 停1 7 。 這種驗(yàn)證方法允許在信號(hào)或引腳級(jí)之外的事務(wù)級(jí)之上的設(shè)計(jì)對(duì)象進(jìn)行模擬 和調(diào)試。建立系統(tǒng)中各功能模塊之間所有可能的事務(wù)類型，并系統(tǒng)地加以測(cè)試。 這種驗(yàn)證不需要很細(xì)致的測(cè)試平臺(tái)及大型向量，因?yàn)槌橄髮哟翁岣叩搅耸聞?wù)級(jí) 而不是信號(hào)或引腳級(jí)；- 所以提高了驗(yàn)證速度，可以很容易的實(shí)現(xiàn)自檢查和定向 隨機(jī)測(cè)試。 4 ) 結(jié)構(gòu)覆蓋率驅(qū)動(dòng)的驗(yàn)證 1 4 哈爾溟工程大學(xué)碩士學(xué)位論文 。dj i 置暑；| e ；昌 結(jié)構(gòu)覆蓋狀況分析是對(duì)設(shè)計(jì)對(duì)象的寄存器傳輸級(jí)視圖的一種分析。它研究 的覆蓋類型有：語(yǔ)句覆蓋、電平翻轉(zhuǎn)覆蓋、有限狀態(tài)機(jī)覆蓋、觸發(fā)覆蓋、分支 覆蓋、表達(dá)式覆蓋、路徑覆蓋和信號(hào)覆蓋。 結(jié)構(gòu)覆蓋狀況分析提供了測(cè)試對(duì)設(shè)計(jì)的覆蓋分析能力，通過(guò)工具得到的覆 蓋率結(jié)果說(shuō)明了功能覆蓋狀況f 洛嘲。這些量化的分析既可以在各個(gè)功能模塊的級(jí) 別上進(jìn)行，也可以在整個(gè)系統(tǒng)級(jí)進(jìn)行。分析工具可以提供驗(yàn)證測(cè)試分析報(bào)告， 包括測(cè)試激勵(lì)已經(jīng)測(cè)試到的設(shè)計(jì)代碼、狀態(tài)機(jī)狀態(tài)以及信號(hào)的翻轉(zhuǎn)情況，為測(cè) 試提供了量化評(píng)價(jià)的手段和查明設(shè)計(jì)對(duì)象未被測(cè)試的地方。 5 軟硬件協(xié)同驗(yàn)證 軟硬件協(xié)同驗(yàn)證是一種在硬件流片封裝之前，驗(yàn)證s o c 系統(tǒng)硬件和軟件是 否能夠正確工作的技術(shù)。協(xié)同驗(yàn)證系統(tǒng)由一個(gè)硬件執(zhí)行環(huán)境和一個(gè)軟件執(zhí)行環(huán) 境組成，通過(guò)事件和命令，使這兩個(gè)環(huán)境間進(jìn)行相互控制l 鐲。敬件的執(zhí)行環(huán)境 用于產(chǎn)生總線周期的序列，協(xié)同驗(yàn)證工具將總線周期轉(zhuǎn)換成許多信號(hào)事件或者 命令集，并驅(qū)動(dòng)這些信號(hào)事件命令進(jìn)入硬件執(zhí)行環(huán)境，然后對(duì)總線周期響應(yīng)進(jìn) 行硬件環(huán)境取樣，這一響應(yīng)又被傳送回軟件環(huán)境。同時(shí)，保持硬件及軟件環(huán)境 間的同步以便發(fā)現(xiàn)硬件或軟件環(huán)境錯(cuò)失響應(yīng)而導(dǎo)致有誤的情形。 協(xié)同驗(yàn)證可以在硬件開(kāi)發(fā)的同時(shí)，讓軟件在硬件模擬平臺(tái)上運(yùn)行，從而硬 件和軟件可以同時(shí)調(diào)試，而不是串行進(jìn)行，大大縮短了集成電路的開(kāi)發(fā)時(shí)間。 協(xié)同驗(yàn)證能提前發(fā)現(xiàn)很多系統(tǒng)級(jí)的錯(cuò)誤。但是由于驗(yàn)證能力和模擬速度問(wèn)題， 已有的協(xié)同驗(yàn)證環(huán)境還無(wú)法提供足夠高的性能在目標(biāo)實(shí)時(shí)操作系統(tǒng)上運(yùn)行整個(gè) 應(yīng)用軟件。 6 ) 硬件仿真器 硬件仿真器以硬件的形式測(cè)試系統(tǒng)。把門級(jí)網(wǎng)表作為輸入，使用真實(shí)的硬 件環(huán)境進(jìn)行驗(yàn)證，通過(guò)軟件驅(qū)動(dòng)驗(yàn)證，與真實(shí)的硬件元件相連接。它首先把設(shè) 計(jì)映射到仿真器元件上，然后給定測(cè)試向量并檢測(cè)仿真器的輸出。這種方法對(duì) 于處理復(fù)雜設(shè)計(jì)可以得到更高的吞吐量，但是需要可綜合的測(cè)試平臺(tái)和昂貴的 仿真器。 整個(gè)仿真系統(tǒng)是專門設(shè)計(jì)出來(lái)的軟件和硬件系統(tǒng)，通常含有可重配置邏輯 或現(xiàn)場(chǎng)可重編程的邏輯門陣列。由于這些系統(tǒng)以硬件方式實(shí)現(xiàn)，所以其運(yùn)行速 度比軟件仿真器快好幾個(gè)數(shù)量級(jí)，并且在有些情況下，其運(yùn)行速度可以接近目 哈爾濱f ：程大學(xué)碩士學(xué)位論文 標(biāo)設(shè)計(jì)對(duì)象的速度。 7 ) 硬件加速器 為了加速邏輯模擬而把門級(jí)網(wǎng)表映射到專門的硬件中。硬件加速技術(shù)將軟 件模擬中全部或部分元件映射到特意為加快某些模擬操作速度而設(shè)計(jì)出來(lái)的硬 件平臺(tái)中圈。最普遍的做法是測(cè)試平臺(tái)仍然以軟件形式運(yùn)行，而幾個(gè)待驗(yàn)證的 設(shè)計(jì)對(duì)象在硬件加速器中運(yùn)行。 硬件仿真加速器可以提供非?？斓姆抡孢\(yùn)行速度，但是同時(shí)也需要很長(zhǎng)的 代碼編譯時(shí)間。而且，硬件仿真加速器也非常昂貴，比起軟件仿真來(lái)說(shuō)難以使 用。對(duì)于要進(jìn)行應(yīng)用程序測(cè)試的大型設(shè)計(jì)，硬件仿真加速器是適合的：但是對(duì) 于小模塊設(shè)計(jì)來(lái)說(shuō)，它不是非常適合的工具。 8 ) 原型驗(yàn)證 臣亟莖- 亟i - 習(xí) l使用示波器等具調(diào)試i - _ _ - - _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 一 圖2 1 0s o c 原型驗(yàn)證流程 原型驗(yàn)證是將硬件原型和軟件原型相結(jié)合進(jìn)行驗(yàn)證。它的本質(zhì)在于快速地 1 6 哈爾濱工程大學(xué)碩士學(xué)位論文 實(shí)現(xiàn)s o c 設(shè)計(jì)中的硬件模塊，讓軟件模塊在真正的硬件上高速運(yùn)行，實(shí)現(xiàn)s o c 設(shè)計(jì)的軟硬件協(xié)同驗(yàn)證p q 。驗(yàn)證流程如圖2 1 0 所示。 該技術(shù)較傳統(tǒng)的協(xié)同驗(yàn)證技術(shù)不同之處在于它實(shí)現(xiàn)的基礎(chǔ)是強(qiáng)大的f p g a 和有力的設(shè)計(jì)描述及編譯工具。原型驗(yàn)證系統(tǒng)由三個(gè)部分組成：系統(tǒng)硬件、軟 件編譯器和運(yùn)行程序。系統(tǒng)硬件設(shè)計(jì)的核心部分是定制的原型電路板，用來(lái)實(shí) 現(xiàn)s o c 設(shè)計(jì)中的關(guān)鍵模塊，系統(tǒng)硬件的常規(guī)模塊則可由商用芯片實(shí)現(xiàn)。軟件編 譯器把寄存器級(jí)或門級(jí)設(shè)計(jì)及其驗(yàn)證環(huán)境扁平化，映射到系統(tǒng)硬件。運(yùn)行程序 控制原型系統(tǒng)的運(yùn)行、設(shè)計(jì)調(diào)試，一般采用c 語(yǔ)言編程，并且有開(kāi)放的軟件結(jié) 構(gòu)，便于后期緊密集成。 9 ) 靜態(tài)檢查 靜態(tài)檢查是對(duì)設(shè)計(jì)對(duì)象的代碼在語(yǔ)法上正確性的檢查。語(yǔ)法上的類型包括 變量初始化、結(jié)構(gòu)語(yǔ)法支持和端口匹配等。靜態(tài)檢查可以在設(shè)計(jì)周期的早期進(jìn) 行，查出設(shè)計(jì)代碼中的簡(jiǎn)單錯(cuò)誤，避免在高層次驗(yàn)證中發(fā)現(xiàn)錯(cuò)誤而耗費(fèi)大量的 時(shí)間進(jìn)行錯(cuò)誤定位。 1 0 ) 靜態(tài)時(shí)序分析 時(shí)序驗(yàn)證用來(lái)確定設(shè)計(jì)是否己滿足時(shí)序要求。時(shí)序驗(yàn)證對(duì)設(shè)計(jì)對(duì)象中的每 一個(gè)存儲(chǔ)元素和鎖存器都有時(shí)序要求，如建立時(shí)間、保持時(shí)間和各種延遲時(shí)序。 靜態(tài)時(shí)序分析是檢測(cè)電路是否滿足時(shí)序要求限制的方法。通過(guò)分析電路的拓?fù)?路徑，檢測(cè)它們的時(shí)序特性和它們對(duì)電路延時(shí)的影響，靜態(tài)時(shí)序分析不需要模 擬，不需要輸入模式。檢查速度快、完整，可以達(dá)到1 0 0 的覆蓋率。但是時(shí) 序驗(yàn)證對(duì)大型設(shè)計(jì)對(duì)象是一種挑戰(zhàn)性難題，因?yàn)槊恳粋€(gè)輸入都可能有多個(gè)信號(hào) 來(lái)源，并且時(shí)序可能會(huì)根據(jù)電路運(yùn)行狀況而變化。 1 1 ) 形式化驗(yàn)證 形式化驗(yàn)證是數(shù)學(xué)的證明一個(gè)描述具有某些屬性或兩個(gè)不同抽象層次的 描述在功能上是等價(jià)的。形式化驗(yàn)證技術(shù)有：定理證明、模型檢驗(yàn)和等價(jià)性檢 測(cè)。形式化驗(yàn)證方法不需要用于驗(yàn)證的測(cè)試平臺(tái)和測(cè)試向量。理論上，形式化 驗(yàn)證技術(shù)將保證非常高的驗(yàn)證速度和1 0 0 的覆蓋率。 應(yīng)用于功能驗(yàn)證的形式驗(yàn)證有如下兩種：模型檢查，一模型檢查又稱特性檢 查，是驗(yàn)證設(shè)計(jì)的功能特點(diǎn)。檢驗(yàn)程序在所有可能的輸入條件下探測(cè)設(shè)計(jì)的全 部狀態(tài)空間，以發(fā)現(xiàn)動(dòng)態(tài)模擬難以找到的錯(cuò)誤。模型檢驗(yàn)對(duì)于以控制為主的設(shè) 1 7 哈爾濱工程大學(xué)碩士學(xué)位論文 計(jì)驗(yàn)證比以數(shù)據(jù)通路為主的設(shè)計(jì)驗(yàn)證更有效，這是由于后者一般有很大和很深 的狀態(tài)空間，驗(yàn)證要花費(fèi)很多的存儲(chǔ)器和處理時(shí)間。定理證明，典型的方法是 支持一種基于形式邏輯的說(shuō)明語(yǔ)言和一組命令形式的策略，用以機(jī)械地構(gòu)造邏 輯中的一個(gè)斷言的證明過(guò)程。定理證明系統(tǒng)的變化很大，定理證明不需要驗(yàn)證 測(cè)試，但需要特性的公式表達(dá)，并且不受輸入或狀態(tài)空間的限制。適合于數(shù)據(jù) 通路型的設(shè)計(jì)和高層應(yīng)用的驗(yàn)證。定理證明的主要缺點(diǎn)是自動(dòng)化不如模型檢驗(yàn) 好，因?yàn)橛脩舯仨氂枚ɡ碜C明器的命令來(lái)構(gòu)造證明過(guò)程；另一個(gè)缺點(diǎn)就是當(dāng)證 明結(jié)論為不成立時(shí)，只能用人工方法分析原因，不能自動(dòng)跟蹤定位錯(cuò)誤。 1 2 ) 基于斷言的驗(yàn)證 基于斷言的驗(yàn)證是把形式化方法集成到傳統(tǒng)模擬流程中的一種有效的方 法。設(shè)計(jì)人員在r t l 設(shè)計(jì)中插入設(shè)計(jì)意圖( 斷言) 并且進(jìn)行模擬，然后用形式 化技術(shù)檢查斷言，限制條件，也就是合法接口行為的斷言，和其他斷言同時(shí)一 同參加模擬。斷言檢查的結(jié)果改進(jìn)模擬的有效性。即使利用傳統(tǒng)的模擬驗(yàn)證， 斷言也可以大大提高模擬的效率?；跀嘌缘尿?yàn)證要由用戶寫出斷言，斷言表 示要驗(yàn)證的性質(zhì)，因此需要性質(zhì)描述語(yǔ)言。例如邏輯和時(shí)序方面的性質(zhì)。這些 也是驗(yàn)證語(yǔ)言要解決的問(wèn)題l - 5 , - z n l 。 基于斷言的驗(yàn)證能夠提高對(duì)設(shè)計(jì)的可控制性和可觀察性，實(shí)現(xiàn)很高的功能 覆蓋率驗(yàn)證，通過(guò)檢查斷言可以確定口是否正確地集中到設(shè)計(jì)中?；跀嘌缘?驗(yàn)證可以縮短驗(yàn)證時(shí)間。 在眾多的驗(yàn)證技術(shù)中，任何單獨(dú)一種驗(yàn)證技術(shù)都沒(méi)有使一次流片的成功率 超過(guò)5 0 。在工程實(shí)際中，常常采用多種技術(shù)相結(jié)合的方法來(lái)進(jìn)行驗(yàn)證，從而 保證更加嚴(yán)格的驗(yàn)證設(shè)計(jì)。但是需要驗(yàn)證人員進(jìn)行科學(xué)的設(shè)計(jì)，否則將會(huì)有重 復(fù)的工作量，增加驗(yàn)證時(shí)間，降低驗(yàn)證效率。 2 5 驗(yàn)證技術(shù)的發(fā)展趨勢(shì) 目前的設(shè)計(jì)驗(yàn)證方法迅速發(fā)展，設(shè)計(jì)和驗(yàn)證語(yǔ)言層出不窮。驗(yàn)證發(fā)展將呈 現(xiàn)以下幾方面發(fā)展趨勢(shì)。 一第一，形式化方法取得了長(zhǎng)遠(yuǎn)進(jìn)展，特別是等價(jià)性檢驗(yàn)已經(jīng)集成到標(biāo)準(zhǔn)驗(yàn) 證流程中。而模型檢驗(yàn)技術(shù)以及定理證明等還不能成為設(shè)計(jì)環(huán)境的主流驗(yàn)證方 法的主要原因有： 哈爾濱工程大學(xué)碩士學(xué)位論文 1 ) 缺乏主流的性質(zhì)描述語(yǔ)言。 2 ) 缺乏供設(shè)計(jì)公司使用的商業(yè)化工具。 3 ) 缺乏有效地使用形式化方法學(xué)的指導(dǎo)原則。 4 ) 在改變驗(yàn)證方法帶來(lái)的收益是否明顯的問(wèn)題上還有待迸一步證明。 第二，形式化方法還需要和傳統(tǒng)的方法相結(jié)合才能發(fā)揮作用。而設(shè)計(jì)和驗(yàn) 證方法的進(jìn)步應(yīng)當(dāng)是漸進(jìn)的，不可能是突然性的改變。因此根據(jù)目前驗(yàn)證方法 的現(xiàn)狀，數(shù)?；旌闲酒脑O(shè)計(jì)越來(lái)越多，混合驗(yàn)證方法應(yīng)當(dāng)成為主流的驗(yàn)證方 法。 第三，基于斷言的驗(yàn)證是結(jié)合形式化驗(yàn)證和傳統(tǒng)的模擬驗(yàn)證可行的途徑。 斷言對(duì)于表示接口限制、設(shè)計(jì)性質(zhì)和設(shè)計(jì)假