謝謝觀賞1功能驗(yàn)證

2019-6-9謝謝觀賞1功能驗(yàn)證謝謝觀賞2主要內(nèi)容

對(duì)VC開發(fā)與集成的功能驗(yàn)證分類VSI聯(lián)盟對(duì)虛擬元件的開發(fā)與集成的功能驗(yàn)證術(shù)語、驗(yàn)證技巧及語言風(fēng)格2019-6-9謝謝觀賞2主要內(nèi)容對(duì)VC開發(fā)與集成的功能驗(yàn)證分類2019-謝謝觀賞3功能驗(yàn)證分類

功能驗(yàn)證的技術(shù)主要分為以下四大塊：

從驗(yàn)證方法上分：l

目的性驗(yàn)證

目的是驗(yàn)證設(shè)計(jì)所試圖完成的功能在設(shè)計(jì)中已正確實(shí)現(xiàn)。最典型的情況是在抽象程度最高的層次完成，其最終結(jié)果是建立一套“黃金模型”，它可以在整個(gè)設(shè)計(jì)過程中作為設(shè)計(jì)細(xì)節(jié)的參考。l

等價(jià)性驗(yàn)證

目的是驗(yàn)證設(shè)計(jì)過程中產(chǎn)生的不同層次的設(shè)計(jì)結(jié)果功能是否符合“黃金模型”。

從驗(yàn)證對(duì)象上分：l

VC驗(yàn)證

對(duì)某個(gè)VC的功能（如：單元測試）進(jìn)行驗(yàn)證的過程。l

集成塊驗(yàn)證

對(duì)包含一個(gè)或多個(gè)VC的SOC進(jìn)行功能驗(yàn)證的過程。2019-6-9謝謝觀賞3功能驗(yàn)證分類

功能驗(yàn)證的技術(shù)主要分為以下四大塊：2謝謝觀賞4在以上每項(xiàng)任務(wù)所使用的技術(shù)和工具之間有很大的交迭。雖然ＶＣ驗(yàn)證和SOC驗(yàn)證的過程相同或者相似，但是，驗(yàn)證測試序列的模型和源代碼則可能迥然不同。對(duì)ＶＣ驗(yàn)證而言，關(guān)鍵的是對(duì)ＶＣ的內(nèi)部邏輯進(jìn)行詳細(xì)的功能驗(yàn)證以確保ＶＣ功能的正確性。而集成片驗(yàn)證卻只是把研究的重點(diǎn)放在VC的連接和相互作用上，其驗(yàn)證模型只需考慮對(duì)VC的接口進(jìn)行精確的描述，對(duì)VC的內(nèi)部功能則無太高要求。2019-6-9謝謝觀賞4在以上每項(xiàng)任務(wù)所使用的技術(shù)和工具之間有很大的交迭。謝謝觀賞5適合于目的驗(yàn)證的工具和技術(shù)動(dòng)態(tài)驗(yàn)證

動(dòng)態(tài)驗(yàn)證是在一系列激勵(lì)的作用下，對(duì)以下幾個(gè)方面的測試：一個(gè)設(shè)計(jì)方案的一個(gè)或幾個(gè)模塊、某設(shè)計(jì)的硬件實(shí)現(xiàn)等。靜態(tài)功能驗(yàn)證

靜態(tài)功能驗(yàn)證利用公式化的數(shù)學(xué)技巧來進(jìn)行驗(yàn)證而不使用驗(yàn)證測試序列。其測試方法還沒有統(tǒng)一的工業(yè)標(biāo)準(zhǔn)，說法比較含糊。

形式驗(yàn)證動(dòng)態(tài)－形式化混合驗(yàn)證為了更好的發(fā)揮形式化驗(yàn)證技術(shù)全面性的特點(diǎn)，在處理大型設(shè)計(jì)、更加廣泛的設(shè)計(jì)風(fēng)格的設(shè)計(jì)時(shí)使用。（符號(hào)仿真、半形式化仿真）硬、軟件聯(lián)合驗(yàn)證硬件仿真物理樣機(jī)虛擬樣機(jī)2019-6-9謝謝觀賞5適合于目的驗(yàn)證的工具和技術(shù)動(dòng)態(tài)驗(yàn)證謝謝觀賞6適用于目的驗(yàn)證的動(dòng)態(tài)驗(yàn)證工具和技術(shù)

確定性仿真概念：對(duì)一個(gè)模塊施加激勵(lì)信號(hào)并由這個(gè)模塊產(chǎn)生響應(yīng)信號(hào)的過程。在確定性仿真中，激勵(lì)信號(hào)被明確給出，而且模塊的響應(yīng)信號(hào)能夠預(yù)知并被檢測到。分類：基于事件的仿真基于事件的軟件仿真器通過事件的發(fā)生（一次一個(gè)事件）和在設(shè)計(jì)中進(jìn)行傳播而進(jìn)行操作直至獲得一個(gè)穩(wěn)定的狀態(tài)。該設(shè)計(jì)方案的模塊包含內(nèi)部周期時(shí)鐘的概念和功能性的概念。輸入的激勵(lì)信號(hào)的任何變化都將作為事件被檢測到，并將被傳遍設(shè)計(jì)的每個(gè)階段。由于輸入信號(hào)的到達(dá)不同時(shí)和底層被測元素的信號(hào)的反饋不同時(shí)，可以在每個(gè)時(shí)鐘周期對(duì)設(shè)計(jì)的某個(gè)元素評(píng)估多次。雖然這能提供高精度的仿真環(huán)境，但執(zhí)行速度有賴于設(shè)計(jì)的規(guī)模，在大型的設(shè)計(jì)中其驗(yàn)證速度會(huì)相應(yīng)降低。基于時(shí)間的仿真基于時(shí)間的仿真采用了不同的方法。這種仿真不再具有內(nèi)部周期時(shí)鐘的概念，它在單個(gè)周期中對(duì)狀態(tài)及/或各端口之間進(jìn)行邏輯評(píng)估。由于每個(gè)邏輯元素在每個(gè)周期中只賦值一次，因此這種方法極大地縮短了執(zhí)行時(shí)間?；跁r(shí)間仿真的簡單模型（沒有時(shí)序，邏輯狀態(tài)少等等）限制了仿真器能夠處理的電路類型。比如說，依賴于內(nèi)部周期時(shí)鐘的電路或在恰當(dāng)?shù)姆抡嬷袀鞑ゲ淮_定值的電路就不能使用這種基于時(shí)間的仿真方法。2019-6-9謝謝觀賞6適用于目的驗(yàn)證的動(dòng)態(tài)驗(yàn)證工具和技術(shù)

2019-6-謝謝觀賞7適用于目的驗(yàn)證的動(dòng)態(tài)驗(yàn)證工具和技術(shù)

隨機(jī)模式仿真分類：直接模式隨機(jī)地址和隨機(jī)控制信號(hào)被加入總線或信號(hào)流中，而且一個(gè)或多個(gè)總線監(jiān)測器對(duì)這些信號(hào)進(jìn)行監(jiān)控，以確?？偩€協(xié)議不會(huì)因?yàn)檫@些操作而產(chǎn)生誤操作。這種方法對(duì)總線驗(yàn)證尤其適用。驗(yàn)證測試序列是直接的，因?yàn)椴僮髦芷诘漠a(chǎn)生并非純粹的隨機(jī)產(chǎn)生，而是以某種特殊的方式來強(qiáng)調(diào)設(shè)計(jì)。這種向量發(fā)生器可用來以特定的分配產(chǎn)生特定的傳輸周期，如：在偽隨機(jī)序列中產(chǎn)生20％的讀，30％的寫和50％的變址讀寫。類似的，在數(shù)據(jù)和地址領(lǐng)域中也可產(chǎn)生隨機(jī)序列，但是得在有限的范圍內(nèi)使用有限的離散數(shù)值。這些類型的測試驗(yàn)證驗(yàn)證用確定性仿真很難驗(yàn)證的臨界狀態(tài)、臨界序列以及依賴于數(shù)據(jù)的狀態(tài)。用這種方法，任何算法錯(cuò)誤都能在設(shè)計(jì)周期的早期就能被發(fā)現(xiàn)和更正。間接模式在間接仿真中，設(shè)計(jì)的輸入直接由隨機(jī)向量發(fā)生器驅(qū)動(dòng)，之后檢查其輸出以檢測任何無效的操作。這種方法最常用于驗(yàn)證數(shù)據(jù)通道和算術(shù)元素，或者用來驗(yàn)證能夠接收任何隨機(jī)序列的小模塊。2019-6-9謝謝觀賞7適用于目的驗(yàn)證的動(dòng)態(tài)驗(yàn)證工具和技術(shù)

隨機(jī)模式仿真謝謝觀賞8適用于目的驗(yàn)證的動(dòng)態(tài)驗(yàn)證工具和技術(shù)

硬件加速

硬件加速是特指為加速某些仿真操作而設(shè)計(jì)的將軟件仿真中部分或全部的成分映射到硬件平臺(tái)中的操作。最典型情況就是測試平臺(tái)仍然保留在軟件中運(yùn)行，而被驗(yàn)證的設(shè)計(jì)卻是在硬件加速器中運(yùn)行。有些類型的加速器也能運(yùn)行行為級(jí)的代碼，這種情況下，具體的時(shí)鐘周期的行為表現(xiàn)并沒有給出詳細(xì)的說明，因此，有可能會(huì)全部在硬件加速器中運(yùn)行純確定性或隨機(jī)模式仿真。

硬件建模有些軟件仿真模型的設(shè)計(jì)元件難以實(shí)現(xiàn)，或者不夠精確。解決這個(gè)難題的方法就是運(yùn)行硬件模型中的一個(gè)半導(dǎo)體元件，將它連接到軟件仿真器上。這個(gè)硬件模型的輸入是接收來自仿真器的信號(hào)，然后將該信號(hào)送到半導(dǎo)體元件中運(yùn)行一個(gè)周期，最后獲得輸出信號(hào)并將它送回仿真器。2019-6-9謝謝觀賞8適用于目的驗(yàn)證的動(dòng)態(tài)驗(yàn)證工具和技術(shù)

硬件加速201謝謝觀賞9適用于目的驗(yàn)證的動(dòng)態(tài)驗(yàn)證工具和技術(shù)協(xié)議檢驗(yàn)協(xié)議檢驗(yàn)器指的是監(jiān)測接口的數(shù)據(jù)處理以及檢查任何無效操作的元件。如果在仿真器中有任何無效操作被檢驗(yàn)到，檢驗(yàn)器將會(huì)作標(biāo)記。這種元件可以裝備在測試平臺(tái)中而不作為設(shè)計(jì)的部分。在這種應(yīng)用中，檢驗(yàn)器僅僅在仿真時(shí)才起作用。當(dāng)然，協(xié)議檢驗(yàn)器也可以植入設(shè)計(jì)之中，這樣檢驗(yàn)器不僅可以在仿真的時(shí)候，而且可以在實(shí)際的物理設(shè)備進(jìn)行的普通操作中都能查錯(cuò)。不過，設(shè)計(jì)中植入的這種設(shè)備要能夠在門級(jí)進(jìn)行綜合。

預(yù)期結(jié)果檢驗(yàn)是系統(tǒng)測試平臺(tái)的一部分。它對(duì)仿真結(jié)果與事先的規(guī)定——期望響應(yīng)文件進(jìn)行比較。如果結(jié)果不符，將會(huì)報(bào)錯(cuò)。2019-6-9謝謝觀賞9適用于目的驗(yàn)證的動(dòng)態(tài)驗(yàn)證工具和技術(shù)協(xié)議檢驗(yàn)2019謝謝觀賞10形式驗(yàn)證形式驗(yàn)證利用數(shù)學(xué)方法對(duì)設(shè)計(jì)結(jié)果的功能進(jìn)行驗(yàn)證。由于它依賴于對(duì)設(shè)計(jì)的數(shù)學(xué)分析，因此無需使用驗(yàn)證測試序列。適用于等價(jià)性檢驗(yàn)和目的性驗(yàn)證。適用于目的性驗(yàn)證的形式驗(yàn)證工具和技巧：性能/模型驗(yàn)證

性能/模型驗(yàn)證是運(yùn)用公式化的數(shù)學(xué)技巧來校驗(yàn)設(shè)計(jì)的功能特性。模型驗(yàn)證器搜索一個(gè)設(shè)計(jì)在所有可能條件下的狀態(tài)空間，去尋找通過仿真很難發(fā)現(xiàn)的缺陷。當(dāng)模型驗(yàn)證員的報(bào)告說某種性質(zhì)是正確的，那么設(shè)計(jì)者就可以放心：他的報(bào)告是100％的精確。模型驗(yàn)證不需要建立任何測試平臺(tái)，其要驗(yàn)證的性質(zhì)是用以特殊的規(guī)范語言描述的查詢表形式。當(dāng)模型驗(yàn)證工具發(fā)現(xiàn)錯(cuò)誤的時(shí)候，它會(huì)產(chǎn)生自初始狀態(tài)開始，到行為或特性出錯(cuò)的地方為止的完全搜索路徑。因?yàn)榘瑪?shù)據(jù)通道的系統(tǒng)經(jīng)常包含很大很廣的狀態(tài)空間，對(duì)這樣的系統(tǒng)進(jìn)行驗(yàn)證就花費(fèi)昂貴的存儲(chǔ)空間和大量的處理時(shí)間。所以模型驗(yàn)證通常在控制密集設(shè)計(jì)的驗(yàn)證中比數(shù)據(jù)通道密集設(shè)計(jì)驗(yàn)證更加有效。模型驗(yàn)證者通常能夠在各種合法輸入序列和合法的輸入狀態(tài)下，如模型驗(yàn)證和性能一樣可以直接從仿真驗(yàn)證出某種特定的條件總是真，最終為真還是永遠(yuǎn)不會(huì)是真。這種性質(zhì)就是對(duì)設(shè)計(jì)的斷言，對(duì)仿真和模型驗(yàn)證都十分有用。通常，斷言表明了某些特定條件必須總是正確，就將該條件列入checker的職能范圍之內(nèi)，一旦在仿真中這種條件有絲毫偏離，checker就會(huì)“罷工”，從而使用戶得到通知。2019-6-9謝謝觀賞10形式驗(yàn)證形式驗(yàn)證利用數(shù)學(xué)方法對(duì)設(shè)計(jì)結(jié)果的功能進(jìn)行謝謝觀賞11形式驗(yàn)證理論證明

基于理論證明技術(shù)的驗(yàn)證系統(tǒng)通常支持某種基于選定形式的邏輯的規(guī)范語言，并支持一組以該語言命令的形式機(jī)械地構(gòu)造邏輯斷言的證明。一個(gè)使用基于理論證明技術(shù)的驗(yàn)證系統(tǒng)的硬件設(shè)計(jì)的形式化驗(yàn)證，通常包含：對(duì)設(shè)計(jì)模型(M)的初步描述，將由驗(yàn)證系統(tǒng)支持的邏輯/規(guī)范語言的性能（P）的初步描述。在所有可能的輸入條件下M能夠正確地推出P的斷言，從而驗(yàn)證性能P。證明標(biāo)準(zhǔn)的完備性保證了在所有可能的輸入狀態(tài)下，該設(shè)計(jì)的性能都是正確的。已經(jīng)有很多的理論證明系統(tǒng)在大型的設(shè)計(jì)中得以成功地運(yùn)用，如在浮點(diǎn)指針單元和在復(fù)雜流水控制中。

同模型校驗(yàn)一樣，理論證明驗(yàn)證也不需要?jiǎng)?chuàng)建任何驗(yàn)證測試平臺(tái)，但是需要有待證明的性能公式。與模型校驗(yàn)不一樣的是，理論證明驗(yàn)證不受輸入規(guī)模和狀態(tài)空間的限制。因此，理論證明驗(yàn)證更加適于基于數(shù)據(jù)通道的設(shè)計(jì)和高層應(yīng)用的功能驗(yàn)證，如浮點(diǎn)指針單元和復(fù)雜流水控制中冒險(xiǎn)的驗(yàn)證等。同時(shí)，理論證明驗(yàn)證還能用于性能檢查中，就如同在一個(gè)設(shè)計(jì)的兩個(gè)模型之間的等價(jià)性校驗(yàn)一樣。但是對(duì)兩個(gè)模型的等價(jià)性檢驗(yàn)而言，在運(yùn)用系統(tǒng)驗(yàn)證語言對(duì)兩個(gè)模型進(jìn)行描述之后，還得給兩個(gè)模型寫一個(gè)合適的斷言并對(duì)之加以證明。

通過理論證明的驗(yàn)證的主要缺點(diǎn)就是它不如模型校驗(yàn)?zāi)菢幼詣?dòng)化程度較高。因?yàn)樵谕ㄟ^理論證明的驗(yàn)證中，用戶必須使用理論證明的命令進(jìn)行交互式的證明。同時(shí)，另一個(gè)缺點(diǎn)就是在對(duì)某事件的證明失敗時(shí)，驗(yàn)證系統(tǒng)無法自動(dòng)構(gòu)造搜索指針。用戶必須通過人為的分析來尋找錯(cuò)誤發(fā)生的原因。2019-6-9謝謝觀賞11形式驗(yàn)證理論證明2019-6-9謝謝觀賞12

硬、軟件聯(lián)合驗(yàn)證

在傳統(tǒng)的系統(tǒng)設(shè)計(jì)的串行流程中，首先構(gòu)造硬件，然后在硬件的基礎(chǔ)上編寫和調(diào)試系統(tǒng)軟件。但是在硬、軟件聯(lián)合驗(yàn)證技術(shù)中，對(duì)系統(tǒng)硬件和軟件的驗(yàn)證是同時(shí)進(jìn)行的。在硬件被開發(fā)的同時(shí)，相應(yīng)的軟件也在硬件仿真平臺(tái)中執(zhí)行，這樣就實(shí)現(xiàn)了硬件和軟件的并行調(diào)試。雖然聯(lián)合驗(yàn)證環(huán)境的建立需要大量的時(shí)間和豐富的經(jīng)驗(yàn)，但是使用硬、軟件聯(lián)合驗(yàn)證技術(shù)的回報(bào)也是十分豐厚的。首先，使用硬、軟件聯(lián)合驗(yàn)證技術(shù)能夠在SOC芯片制造之前就能發(fā)現(xiàn)并糾正許多系統(tǒng)級(jí)漏洞和問題。在實(shí)際的處理器和固件模型中進(jìn)行的仿真，結(jié)果會(huì)更加精確，而且同舊的使用總線傳輸模型的設(shè)計(jì)流程比較起來，可以進(jìn)行更廣泛的驗(yàn)證。而且，在仿真過程中，軟件也得到了調(diào)試和驗(yàn)證。相應(yīng)的允許在芯片實(shí)際生成的同時(shí)，給系統(tǒng)的發(fā)展提供較高的發(fā)展速度。最終結(jié)果是，硬、軟件聯(lián)合驗(yàn)證技術(shù)通過在設(shè)計(jì)的早期就很快的解決了問題而提高了整個(gè)產(chǎn)品開發(fā)周期的質(zhì)量，節(jié)省了時(shí)間和金錢。

2019-6-9謝謝觀賞12硬、軟件聯(lián)合驗(yàn)證在傳統(tǒng)的系統(tǒng)設(shè)計(jì)的串行流程中謝謝觀賞13硬件仿真硬件仿真器是通常由某些可重構(gòu)邏輯（通常為現(xiàn)場可編程門陣列，如FPGA）組成的專門設(shè)計(jì)的硬件和軟件系統(tǒng)。編程這些系統(tǒng)以模仿設(shè)計(jì)目標(biāo)的行為和功能，甚至達(dá)到將仿真過的設(shè)計(jì)同設(shè)計(jì)即將在其中操作的系統(tǒng)的剩余部分直接連接的程度。由于這些系統(tǒng)是以硬件為基礎(chǔ)的，因此，它們能夠提供與最終設(shè)計(jì)目標(biāo)接近的電路仿真速度。這些幾千Hz的速度同以軟件為基礎(chǔ)的仿真所提供的幾十Hz的速度形成鮮明的對(duì)比。這種幾個(gè)量級(jí)的行為差異使得模擬技術(shù)能夠執(zhí)行在軟件硬件仿真時(shí)要用幾個(gè)月甚至幾年才能完成的大型驗(yàn)證任務(wù)。這種驗(yàn)證任務(wù)的例子包括數(shù)據(jù)集的處理如視頻數(shù)據(jù)流等，或者是有成千上萬行的軟件如操作系統(tǒng)的引導(dǎo)程序等。在帶有嵌入式處理器的SOC在轉(zhuǎn)化至硅片之前，在軟件在與周圍邏輯協(xié)同工作時(shí)，需要硬件仿真技術(shù)或樣機(jī)技術(shù)對(duì)軟件在嵌入的處理器上運(yùn)行時(shí)的復(fù)雜功能進(jìn)行驗(yàn)證。正因?yàn)檫@樣，通常認(rèn)為這種硬件仿真系統(tǒng)在并行設(shè)計(jì)流程中是介于硬件和軟件之間的。2019-6-9謝謝觀賞13硬件仿真硬件仿真器是通常由某些可重構(gòu)邏輯（通常為謝謝觀賞14硬件仿真有很多不同的體系結(jié)構(gòu)都借用這種硬件仿真系統(tǒng)來提供靈活性、可控性、可視性和性能。這些體系結(jié)構(gòu)包括FPGA的互聯(lián)陣列，自定義處理器陣列，帶有可編程縱橫切換器的磁頭系統(tǒng)和可編程總線接口的系統(tǒng)等。這些不同的體系結(jié)構(gòu)能夠在設(shè)計(jì)容量、行為特性和最優(yōu)布局結(jié)構(gòu)方面能提供一定程度的折衷方案，并且力圖能夠兼容并輔助包括其他驗(yàn)證技術(shù)如軟件模擬、時(shí)序驗(yàn)證、形式化驗(yàn)證和邏輯分析的驗(yàn)證方法。雖然硬件仿真的設(shè)計(jì)方案是從建立在一般的硬件平臺(tái)上的，但是在某種程度上可以看作有限精度的樣機(jī)。通常硬件仿真器支持對(duì)設(shè)計(jì)的內(nèi)部節(jié)點(diǎn)保持高度的可觀察性，使設(shè)計(jì)在更類似于模擬而非真實(shí)物理樣機(jī)的方式除錯(cuò)。事實(shí)上，因?yàn)檐浖M器與仿真器交互工作的方式在本質(zhì)上與硬件模擬加速器相同，有時(shí)仿真器也用作模擬目的。雖然硬件仿真器有時(shí)候能夠接近最終設(shè)計(jì)的速度，但是，除非它們能夠同與最終設(shè)計(jì)一樣的系統(tǒng)相聯(lián)，否則，它們的速度仍將受到限制。另外，硬件仿真系統(tǒng)的成本往往限制了一個(gè)項(xiàng)目中允許的系統(tǒng)數(shù)目，反過來，這又限制了能夠同時(shí)運(yùn)行硬件仿真的工程師的數(shù)目。2019-6-9謝謝觀賞14硬件仿真有很多不同的體系結(jié)構(gòu)都借用這種硬件仿真系謝謝觀賞15物理樣機(jī)一種目標(biāo)設(shè)計(jì)的硬件代替品，它的運(yùn)行能夠“接近”目標(biāo)設(shè)計(jì)平臺(tái)的性能。執(zhí)行速度能夠比軟件仿真系統(tǒng)的速度快出許多。物理樣機(jī)能夠支持以下功能：

在SOC器件可用之前，應(yīng)用軟件和系統(tǒng)軟件的開發(fā)和調(diào)試

系統(tǒng)的系統(tǒng)級(jí)性能測試

目標(biāo)設(shè)計(jì)的高性能仿真平臺(tái)，該設(shè)計(jì)能支持復(fù)雜測試周期

具有支持硬、軟件聯(lián)合仿真的硬件平臺(tái)和軟件環(huán)境

用于測試的邏輯分析接口

目標(biāo)設(shè)計(jì)的市場演示典型情況下，物理樣機(jī)在與目標(biāo)系統(tǒng)速度相同的數(shù)量級(jí)范圍內(nèi)運(yùn)行，因此，它的執(zhí)行速度能夠比軟件仿真系統(tǒng)的速度快出許多。這意味著全部的測試序列都能夠裝載到物理樣機(jī)中去，并同系統(tǒng)級(jí)驗(yàn)證測試向量一起運(yùn)行。在考慮到可以樣機(jī)化的設(shè)計(jì)的數(shù)目、執(zhí)行速度以及性能變化時(shí)間時(shí)，通過不同的方法得到的樣機(jī)就會(huì)有不同的性能。在以下系統(tǒng)中都可以在SOC設(shè)計(jì)上建立可重用的樣機(jī)：硬件仿真系統(tǒng)的樣機(jī)可重構(gòu)樣機(jī)系統(tǒng)專用樣機(jī)系統(tǒng)2019-6-9謝謝觀賞15物理樣機(jī)一種目標(biāo)設(shè)計(jì)的硬件代替品，它的運(yùn)行能夠“謝謝觀賞16虛擬樣機(jī)

一個(gè)虛擬樣機(jī)就是一個(gè)產(chǎn)品、一個(gè)元件或一個(gè)系統(tǒng)的計(jì)算機(jī)模擬模型。同其它基于其自身特性的“模型”術(shù)語不一樣的是，“虛擬樣機(jī)”這個(gè)術(shù)語并不是指任何特殊的模型特性，而指在設(shè)計(jì)流程中做模型的角色。一般來說，一個(gè)虛擬模型應(yīng)該支持下列任務(wù)：l

試探開發(fā)設(shè)計(jì)的替代品l

證明設(shè)計(jì)的概念l

測試需求的滿意度和正確度虛擬樣機(jī)可以在各個(gè)抽象的層次上構(gòu)建也可以包含一個(gè)多層次的混合體。在一個(gè)設(shè)計(jì)系統(tǒng)中可以有一個(gè)和幾個(gè)虛擬樣機(jī)同時(shí)存在，每個(gè)虛擬樣機(jī)都能完成上述所說的任務(wù)。為了能在更大的設(shè)計(jì)系統(tǒng)中發(fā)揮作用，一個(gè)虛擬樣機(jī)應(yīng)該對(duì)設(shè)計(jì)的元件或系統(tǒng)的接口進(jìn)行定義。與物理樣機(jī)相比，物理樣機(jī)需要有詳細(xì)的硬件和軟件設(shè)計(jì)描述，而虛擬樣機(jī)能夠更快、更有效、更加抽象而且在設(shè)計(jì)流程中能夠更早的加以構(gòu)建。因此，其中的一個(gè)區(qū)別就是，虛擬樣機(jī)作為一個(gè)計(jì)算機(jī)仿真器，比起物理樣機(jī)的常規(guī)操作來，能提供有關(guān)內(nèi)部狀態(tài)的更多的，無害的可視化信息。此外，與物理樣機(jī)相比較而言，虛擬樣機(jī)的一個(gè)主要缺點(diǎn)就是，它的操作速度同軟件仿真器的速度十分接近，因此就限制了在一定的時(shí)間內(nèi)所能完成的驗(yàn)證數(shù)目。2019-6-9謝謝觀賞16虛擬樣機(jī)一個(gè)虛擬樣機(jī)就是一個(gè)產(chǎn)品、一個(gè)元件或一謝謝觀賞17適合于等價(jià)性驗(yàn)證的工具和技術(shù)動(dòng)態(tài)驗(yàn)證形式化等價(jià)性檢驗(yàn)

物理驗(yàn)證

2019-6-9謝謝觀賞17適合于等價(jià)性驗(yàn)證的工具和技術(shù)動(dòng)態(tài)驗(yàn)證2019-6謝謝觀賞18等價(jià)性驗(yàn)證中的動(dòng)態(tài)驗(yàn)證工具和技術(shù)確定性仿真：給模型施加明確定義的信號(hào)，產(chǎn)生相應(yīng)的響應(yīng)，在將仿真結(jié)果與預(yù)期值比較。一旦在RTL級(jí)模型上的驗(yàn)證平臺(tái)和驗(yàn)證測試向量被開發(fā)出來，那么同樣地驗(yàn)證向量集合也能在門級(jí)網(wǎng)表上對(duì)原設(shè)計(jì)進(jìn)行仿真，以檢查結(jié)果是否相同。在有些情形下，也有可能在對(duì)同樣的設(shè)計(jì)的高層或者低層仿真過程中進(jìn)行同樣的驗(yàn)證測試。預(yù)期結(jié)果檢查：對(duì)仿真結(jié)果同先前指定了的預(yù)期響應(yīng)文件進(jìn)行比較。出現(xiàn)任何錯(cuò)誤的時(shí)候，檢查者就會(huì)報(bào)錯(cuò)。黃金模型檢查：監(jiān)視一個(gè)設(shè)計(jì)中兩個(gè)模型的響應(yīng)，將響應(yīng)信號(hào)與輸入激勵(lì)相比較，并且對(duì)任何偏差作出標(biāo)記。其中一個(gè)為“黃金模型”或可信任模型，而另外一個(gè)則是待證明的模型。一般情況下，這種比較不包括任何形式化驗(yàn)證技術(shù)，兩個(gè)模型之間的響應(yīng)信號(hào)比較僅基于信號(hào)的變化。驗(yàn)證測試序列的遷移：把系統(tǒng)級(jí)驗(yàn)證測試序列應(yīng)用到設(shè)計(jì)的其它層次需要有可以將其遷移或轉(zhuǎn)換為設(shè)計(jì)的RTL級(jí)或網(wǎng)表級(jí)應(yīng)用序列格式的能力。包括：功能級(jí)向RTL級(jí)的遷移和RTL級(jí)向網(wǎng)表級(jí)遷移。2019-6-9謝謝觀賞18等價(jià)性驗(yàn)證中的動(dòng)態(tài)驗(yàn)證工具和技術(shù)確定性仿真：給模謝謝觀賞19等價(jià)性驗(yàn)證中的動(dòng)態(tài)驗(yàn)證工具和技術(shù)回歸測試：最通常用來驗(yàn)證一個(gè)設(shè)計(jì)的更改沒有使現(xiàn)有的驗(yàn)證測試產(chǎn)生失敗。在一個(gè)設(shè)計(jì)上運(yùn)行一個(gè)回歸測試通常意味著兩種驗(yàn)證環(huán)境屬性：第一種是在自動(dòng)化驗(yàn)證環(huán)境下，其中所有的EDA工具、驗(yàn)證測試過程及結(jié)果分析都能成批的進(jìn)行；第二種真正回歸測試方法的特點(diǎn)是測試的成功或失敗都在批處理模式中實(shí)現(xiàn)。在每次運(yùn)行的隨機(jī)行為都等價(jià)時(shí)，回歸測試最經(jīng)常被用來與目的性模擬和隨機(jī)向量模擬一起使用。Regressionenvironment:用以收集，編譯，并運(yùn)行testbench和激勵(lì)文件的機(jī)制。驗(yàn)證有一個(gè)很典型的問題，即在解決bug的的過程中，可能會(huì)無意識(shí)地引入另一個(gè)bug，在此時(shí)我們應(yīng)該在其中加入regression測試組，幫助驗(yàn)證：在新特性加入、舊bug解除時(shí)，現(xiàn)存的功能基本點(diǎn)得以保留。在整個(gè)項(xiàng)目的驗(yàn)證階段，在驗(yàn)證的過程之中，一旦檢測到bug，在regression測試組就應(yīng)加入對(duì)bug的測試，這一點(diǎn)非常重要。regression測試組可以基于一個(gè)規(guī)則一定的基礎(chǔ)。在同一個(gè)模型上的不同的環(huán)境context（如不同的激勵(lì)向量序列，或反標(biāo)時(shí)序）中運(yùn)行驗(yàn)證工具（如模擬）。對(duì)于每次運(yùn)行都同時(shí)備有建立pass/fail狀態(tài)的機(jī)制。2019-6-9謝謝觀賞19等價(jià)性驗(yàn)證中的動(dòng)態(tài)驗(yàn)證工具和技術(shù)回歸測試：最通常謝謝觀賞20形式化等價(jià)性檢驗(yàn)

形式化等價(jià)性檢驗(yàn)工具要證明的是：兩個(gè)設(shè)計(jì)從I/O接口和基于一個(gè)接一個(gè)的周期的角度來看功能上是等價(jià)的。形式化等價(jià)性檢驗(yàn)通常用在設(shè)計(jì)的RTL級(jí)和門級(jí)網(wǎng)表級(jí)。在有些情形下，也能用于更高或者更低的模型。同軟件仿真相比，形式化等價(jià)性檢驗(yàn)具有幾個(gè)優(yōu)點(diǎn)。首先，與仿真不同，形式化等價(jià)性檢驗(yàn)?zāi)軌蛱峁┩暾牡葍r(jià)性檢驗(yàn)，而仿真只驗(yàn)證到一個(gè)驗(yàn)證測試組是否在設(shè)計(jì)中運(yùn)行的程度。另外，形式化等價(jià)性檢驗(yàn)?zāi)軌蛟诤芏痰臅r(shí)間內(nèi)執(zhí)行完需要復(fù)雜仿真才能完成的任務(wù)，這就有利于將驗(yàn)證和錯(cuò)誤調(diào)試自動(dòng)化。等價(jià)性檢驗(yàn)工具通常會(huì)提供與小的獨(dú)立邏輯塊不匹配的詳細(xì)“反例”。包括布爾等價(jià)性檢驗(yàn)和時(shí)序等價(jià)性檢驗(yàn)。2019-6-9謝謝觀賞20形式化等價(jià)性檢驗(yàn)形式化等價(jià)性檢驗(yàn)工具要證明的是謝謝觀賞21形式化等價(jià)性檢驗(yàn)布爾等價(jià)性檢驗(yàn)許多等價(jià)性檢驗(yàn)工具是布爾等價(jià)性檢驗(yàn)器，這意味著它們檢驗(yàn)的是組合邏輯。運(yùn)用這些工具，通常自動(dòng)進(jìn)行兩個(gè)設(shè)計(jì)的存儲(chǔ)元件（如觸發(fā)器、鎖存器等）間格式的比較，從而完成對(duì)名詞的映射。當(dāng)映射確定以后，相應(yīng)的工具就開始對(duì)存儲(chǔ)器的每對(duì)映射名詞的輸入的組合邏輯開始檢查是否等價(jià)。這意味著對(duì)每一種可能的輸入組合，組合邏輯輸出（也即存儲(chǔ)器元件的輸入）是相同的。時(shí)序等價(jià)性檢驗(yàn)有這樣一種情況：兩個(gè)設(shè)計(jì)的存儲(chǔ)元件的數(shù)目不同或排列不同，但是就輸入－輸出數(shù)據(jù)流的生成以及在兩個(gè)狀態(tài)機(jī)之間給定的某些初始狀態(tài)方面兩者是等價(jià)的。這就是時(shí)序等價(jià)。這樣的例子如有限狀態(tài)機(jī)的兩種實(shí)現(xiàn)方式：一個(gè)采用全譯碼方式，即用3個(gè)鎖存器編碼8個(gè)狀態(tài)；另一種采用one-hot編碼，用8個(gè)鎖存器為8個(gè)狀態(tài)編碼。然而這兩個(gè)狀態(tài)機(jī)都有同樣的輸出/入數(shù)據(jù)信號(hào)，都開始于相同的初始狀態(tài)，有相同的輸入數(shù)據(jù)流。時(shí)序等價(jià)性檢驗(yàn)比布爾等價(jià)性檢驗(yàn)存在更大的困難。因此能夠執(zhí)行這種任務(wù)的工具更加稀少。有很多的布爾等價(jià)性檢驗(yàn)確實(shí)支持時(shí)序等價(jià)性檢驗(yàn)，允許檢驗(yàn)很小的有限狀態(tài)機(jī)（通常用戶必須手動(dòng)地支持一些等價(jià)狀態(tài)賦值的映射，因而限制了這種檢驗(yàn)只能適合于小規(guī)模的狀態(tài)機(jī)），或者允許檢驗(yàn)?zāi)承┙M合邏輯器件跨越存儲(chǔ)器元件邊界的簡單操作。但是，從實(shí)際的觀點(diǎn)來看，總的說來大規(guī)模設(shè)計(jì)的時(shí)序等價(jià)性檢驗(yàn)中有很多有待解決的問題。2019-6-9謝謝觀賞21形式化等價(jià)性檢驗(yàn)布爾等價(jià)性檢驗(yàn)2019-6-9謝謝觀賞22物理驗(yàn)證

物理驗(yàn)證就是通過檢驗(yàn)圖形設(shè)計(jì)的數(shù)據(jù)庫以確信物理實(shí)現(xiàn)確實(shí)是原始邏輯設(shè)計(jì)的正確表述。物理驗(yàn)證包括以下三個(gè)部分：電學(xué)規(guī)則檢驗(yàn)（以下簡稱ERC）、設(shè)計(jì)規(guī)則檢驗(yàn)（以下簡稱DRC）及布線和電路圖檢驗(yàn)（以下簡稱LVS）。標(biāo)準(zhǔn)的圖形數(shù)據(jù)庫形式是GDSII－數(shù)據(jù)流。一個(gè)設(shè)計(jì)的GDSII－數(shù)據(jù)流數(shù)據(jù)庫包括電路的多邊形表述，并對(duì)目標(biāo)設(shè)計(jì)劃分成不同的設(shè)計(jì)層次。ERC指的是檢驗(yàn)圖形數(shù)據(jù)庫是否有與電學(xué)設(shè)計(jì)規(guī)則相違背之處。這些電學(xué)規(guī)則就是流程說明，并包含檢驗(yàn)是否有無用輸入，浮點(diǎn)輸入和裝載沖突等。還檢驗(yàn)連接是否合法，如短路和短接。DRC指的是檢驗(yàn)圖形數(shù)據(jù)庫是否有與設(shè)計(jì)流程規(guī)則相違背之處。這些規(guī)則收集在DRC規(guī)則文件中，并包含層與層之間的空間檢驗(yàn)、布線寬度、層與層的相互重疊等。LVS就是檢驗(yàn)提取的圖形數(shù)據(jù)庫是否有與“黃金”網(wǎng)表相違背之處。LVS工具從多邊形數(shù)據(jù)中構(gòu)建網(wǎng)表以及從物理布局中提取器件模型。提取出的網(wǎng)表需和“黃金”模型保持一致。所有的器件和互連都必須嚴(yán)格地相匹配。其他的影響時(shí)序的物理驗(yàn)證如信號(hào)的完整性、串?dāng)_、金屬遷移、噪音等不在功能驗(yàn)證論述的范圍內(nèi)。2019-6-9謝謝觀賞22物理驗(yàn)證物理驗(yàn)證就是通過檢驗(yàn)圖形設(shè)計(jì)的數(shù)據(jù)庫以謝謝觀賞23VC驗(yàn)證

VC驗(yàn)證包含目的性驗(yàn)證和等價(jià)性驗(yàn)證。目的性驗(yàn)證可以在任何層次完成。但是，應(yīng)該指出的是，所應(yīng)用的抽象層次越高，驗(yàn)證的效率就越高?，F(xiàn)在，因?yàn)镽TL級(jí)是在設(shè)計(jì)和驗(yàn)證過程中許多工具所能提供的最高抽象層次，所以通過在設(shè)計(jì)過程中使用許多工具（如比如模型驗(yàn)證、等價(jià)性檢查、代碼覆蓋率等），目的驗(yàn)證的典型情況在RTL級(jí)完成。等價(jià)性驗(yàn)證必須至少在設(shè)計(jì)分解的最底層（如GDSII流，網(wǎng)表等）同黃金模型（在先前目的驗(yàn)證中已驗(yàn)證的模型）進(jìn)行驗(yàn)證時(shí)也能通過驗(yàn)證。一般很多（當(dāng)然不一定是所有的）中間設(shè)計(jì)抽象也都需要進(jìn)行驗(yàn)證。2019-6-9謝謝觀賞23VC驗(yàn)證

VC驗(yàn)證包含目的性驗(yàn)證和等價(jià)性驗(yàn)證。2謝謝觀賞24集成塊驗(yàn)證集成塊驗(yàn)證包含目的性驗(yàn)證和等價(jià)性檢驗(yàn)，它致力于驗(yàn)證含有一個(gè)或多個(gè)VC的SOC。因?yàn)槠淠康氖球?yàn)證一塊集成的SOC而不是單個(gè)的元件，在驗(yàn)證中可以使用“灰箱”模型。它們精確地模擬VC的接口而非VC的內(nèi)部功能。雖然集成塊測試無需重復(fù)VC提供者執(zhí)行的VC驗(yàn)證，但集成者還是想知道VC驗(yàn)證計(jì)劃來評(píng)定/證明VC。第六部分就提供了有可能被驗(yàn)證的模型層次的小結(jié)。由于集成塊驗(yàn)證以VC提供者難以預(yù)期的方式激勵(lì)VC，因此，于VC自身而言，對(duì)含有全部內(nèi)部功能的“白箱”模型的驗(yàn)證在錯(cuò)誤探測方面具有大的發(fā)展?jié)摿Α?019-6-9謝謝觀賞24集成塊驗(yàn)證集成塊驗(yàn)證包含目的性驗(yàn)證和等價(jià)性檢驗(yàn)，謝謝觀賞25功能驗(yàn)證映射驗(yàn)證步驟驗(yàn)證技術(shù)模型硬件目的性仿真功能級(jí)

行為級(jí)

RTL級(jí)

硬件仿真RTL級(jí)

模型檢驗(yàn)RTL級(jí)

理論證明RTL級(jí)

物理樣機(jī)行為級(jí)

RTL級(jí)

邏輯

虛擬樣機(jī)功能級(jí)

代碼覆蓋率RTL級(jí)軟件目的性硬、軟件聯(lián)合驗(yàn)證行為級(jí)

RTL級(jí)

硬件仿真RTL級(jí)

物理樣機(jī)行為級(jí)

RTL級(jí)

邏輯硬件等價(jià)性仿真行為級(jí)

RTL級(jí)

邏輯

門級(jí)

開關(guān)級(jí)

電路

硬件仿真RTL級(jí)

等價(jià)性檢驗(yàn)RTL級(jí)

門級(jí)

故障覆蓋率門級(jí)

物理驗(yàn)證圖形數(shù)據(jù)庫

電路

開關(guān)級(jí)

門級(jí)軟件等價(jià)性硬、軟件聯(lián)合驗(yàn)證行為級(jí)

硬件仿真RTL級(jí)

物理樣機(jī)行為級(jí)

RTL級(jí)

邏輯左表給出了不同的功能驗(yàn)證模型和技術(shù)與不同的驗(yàn)證步驟之間的對(duì)應(yīng)關(guān)系。2019-6-9謝謝觀賞25功能驗(yàn)證映射驗(yàn)證步驟驗(yàn)證技術(shù)模型硬件目的性仿真功謝謝觀賞26驗(yàn)證衡量方法

以下部分所描述的技術(shù)和工具，可以用來衡量對(duì)某設(shè)計(jì)驗(yàn)證的完備性：

一、硬件代碼覆蓋率：可以在仿真過程中通過硬件代碼覆蓋率分析工具來評(píng)定驗(yàn)證測試序列的覆蓋率指標(biāo)。把特定的測試驗(yàn)證序列輸入到特定設(shè)計(jì)中，通過代碼覆蓋率分析就有可能得出功能覆蓋率的某些方面的信息。分析工具可以提供以下信息：·每個(gè)被評(píng)估屬性的百分比的覆蓋率值·設(shè)計(jì)中沒有執(zhí)行或者只是部分執(zhí)行的區(qū)域的列表代碼覆蓋率分析通常是在設(shè)計(jì)流程的RTL級(jí)上進(jìn)行的，評(píng)估的是以下類型的覆蓋率：

·語句覆蓋率：表明每條語句被執(zhí)行的次數(shù)；·信號(hào)觸發(fā)覆蓋率：表明設(shè)計(jì)信號(hào)中的哪一位被觸發(fā)；·有限狀態(tài)機(jī)覆蓋率：表明進(jìn)行了多少個(gè)有限狀態(tài)機(jī)的轉(zhuǎn)變過程，可以視為路徑覆蓋率的一部分；·被訪問狀態(tài)覆蓋率：表明有限狀態(tài)機(jī)有多少個(gè)的狀態(tài)參與了仿真；·觸發(fā)覆蓋率：表明每個(gè)進(jìn)程是否被敏感度列表中的每個(gè)信號(hào)唯一觸發(fā)到；·分支覆蓋率：表明哪一條“case”或者“if…else”語句被執(zhí)行；·表達(dá)式覆蓋率：表明“if”條件布爾表達(dá)式或賦值布爾表達(dá)式的執(zhí)行的好壞程度；·路徑覆蓋率：表明通過“if…else”和“case”順序結(jié)構(gòu)的哪條路徑被執(zhí)行；·信號(hào)覆蓋率：表明狀態(tài)信號(hào)或ROM尋址的執(zhí)行的好壞程度。2019-6-9謝謝觀賞26驗(yàn)證衡量方法

以下部分所描述的技術(shù)和工具，可以謝謝觀賞27驗(yàn)證衡量方法二、功能覆蓋率功能覆蓋率是一種由用戶定義的、反映在驗(yàn)證過程中被運(yùn)行到的功能點(diǎn)的范圍的衡量方法。功能點(diǎn)可以是對(duì)VC用戶而言可視的體系結(jié)構(gòu)特點(diǎn)，也可以是主要的微結(jié)構(gòu)特征。通常情況下，這些特征不能從實(shí)現(xiàn)中自動(dòng)生成，因此需要在驗(yàn)證testbench中的一些規(guī)范。功能覆蓋率數(shù)據(jù)一般是一些時(shí)序行為（如總線的交易）和一些數(shù)據(jù)（如交易源、目的和優(yōu)先級(jí)等）的交叉組合。附加覆蓋率信息可以從功能覆蓋率點(diǎn)的交叉引用中得到。比如，在一個(gè)器件的兩個(gè)引腳之間進(jìn)行的數(shù)據(jù)處理的相互關(guān)系，或者在一個(gè)處理器中指令和中斷的關(guān)系等。與代碼覆蓋率不一樣的是功能覆蓋率的指標(biāo)需要開發(fā)者自行定義。一個(gè)好的定義不僅與驗(yàn)證平臺(tái)緊密相關(guān)，而且應(yīng)覆蓋VC中的所有主要特征。因此，功能覆蓋率比代碼覆蓋率的要求更加嚴(yán)格。經(jīng)驗(yàn)表明，功能覆蓋率與bugs/每周衡量法之間有緊密聯(lián)系。雖然有些方面可以在更低或者更高的層次上評(píng)估，功能覆蓋率分析通常還是在設(shè)計(jì)的RTL級(jí)上進(jìn)行。2019-6-9謝謝觀賞27驗(yàn)證衡量方法二、功能覆蓋率2019-6-9謝謝觀賞28Terminology(1)

Branchcoverage:確定在模擬中運(yùn)行到了哪些RTL源代碼的分支的代碼覆蓋率類型。Codecoverage:一種通過報(bào)告被模擬過的RTL源代碼以測量覆蓋率的測量方法。代碼覆蓋率的類型包括語句，分支，條件和觸發(fā)器覆蓋率。Conditioncoverage:檢查條件語句中的子表達(dá)式以確定那些子表達(dá)式的哪些值導(dǎo)致了在模擬中高一層表達(dá)式為真/假的代碼覆蓋率類型。Finitestatemachine(FSM)coverage:Metricthatmeasurescoveragebyreportingwhichstates,transitions,and/orinputpatternsofanFSMhavebeensimulated.Compiledstimulus:C,assembly,orotherlanguagehigherthanabinaryrepresentationthatiscompiledintobinary.Configuration:Collectionofsetupvaluesappliedtotheconfigurablemodules.2019-6-9謝謝觀賞28Terminology(1)

Branchco謝謝觀賞29Terminology(2)Logicchecking(alsoequivalencechecking):Useofformalmathematicalmethodstodetermineifthebooleanfunctionsoftwodesignsarethesame;typicallyperformedautomaticallyusingasoftwareprogram.Mastermode:Modeinwhichtheprocessorexecutescodefromeitherinternalorexternalmemory.Muxchecking(alsoone-hotchecking):Useofformalmathematicalmethodstodetermineifthehigh-impedancemultiplexorsinadesignallexhibitthepropertythatoneandonlyoneenableisactiveatatime;typicallyperformedautomaticallyusingasoftwareprogram.Pin:Externalphysicalconnection.Regression:一種在同一個(gè)模型上的不同的環(huán)境context（如不同的激勵(lì)向量序列，或反標(biāo)時(shí)序）中運(yùn)行驗(yàn)證工具（如模擬）的做法。對(duì)于每次運(yùn)行都同時(shí)備有建立pass/fail

狀態(tài)的機(jī)制。Regressionenvironment:用以收集，編譯，并運(yùn)行testbench和激勵(lì)文件的機(jī)制。2019-6-9謝謝觀賞29Terminology(2)Logicchec謝謝觀賞30Terminology(3)Simulation:Processofapplyingastimuluspatterntoasoftwaremodelthatpropagatestheeffectofinputstimuluschangesasifthemodelwastheactualdevice.Thesoftwaremodelallowsforvariouskindsofmonitoring,probinganddebuggingtoolstoberuninconjunctionwiththesimulation.Mastermode:Modeinwhichtheprocessorexecutescodefromeitherinternalorexternalmemory.Slavemode:Modeinwhichprocessorbusisdirectlycontrolledbyabusdriver.AttheSoClevel,thisrequirestheSoCtosupportanexternalbusinterface(EBI)orothermeanstoaccessthebusfromtheoutside.Specificationcoverage:Metricthatmeasurescoveragebyreportinghowmanyfactualattributesinthespecificationhavebeendemonstratedtobetrueduringsimulation.Statementcoverage:TypeofcodecoveragethatdetermineswhichexecutablestatementsintheRTLsourcecodehavebeenexecutedduringsimulation.Testmode:Modeinwhichspecialfactorytestfeaturesareenabled.2019-6-9謝謝觀賞30Terminology(3)Simulation謝謝觀賞31Terminology(4)Stimulus:Definitionforaspecificsetofstatechanges(e.g.,transactions)tobeappliedtotheDUTthroughasuitabletestbenchanddrivers/monitors.MayormaynotalsospecifyconstructstoanalyzeresponsevaluesgeneratedbytheDUT.Testbench:Verification-specificconstructsthatprovidethegluebetweentheDUT,driver,monitors,andstimulus.Togglecoverage:Typeofcodecoveragethatchecksthateachnodeinagatelevelrepresentationchangespolarity(toggles)duringsimulationandsoisnotstuckatonelevel.Vector:Singleunitofstimulusandresponse.Itspecifiesstimulusbyassigningazero,one,orZtoeachinputandbidirectionalpin,anditspecifiesresponsebyassigningazero,one,Z,orXtoeachoutputandbidirectionalpin.Contentionmustbeavoidedonbi-directionalpinsbyconformingtothefollowingconstraints:Ifthepinisstimulatedwithzeroorone,itsexpectedresponsemustbespecifiedasX.Iftheexpectedresponseofthepiniszeroorone,itmustbestimulatedwithZ.2019-6-9謝謝觀賞31Terminology(4)Stimulus:謝謝觀賞32驗(yàn)證技巧及語言風(fēng)格1.CodingforVerification2.Testbench3.DriversandMonitors4.DetailedBehavioralModelforVC5.DetailedBehavioralModelforMemory6.DetailedBehavioralModelforI/OPads7.StubModel8.Stimulus9.SimulationScripts10.Coverage11.FormalLogicEquivalenceChecking12.FunctionalCoverage13.FormalModelChecking14.Emulation2019-6-9謝謝觀賞32驗(yàn)證技巧及語言風(fēng)格1.CodingforVe謝謝觀賞331.CodingforVerification

標(biāo)準(zhǔn)編碼指南幫助VC設(shè)計(jì)者和集成者共享設(shè)計(jì)數(shù)據(jù)并開發(fā)SoC解決辦法。以下規(guī)則和指南主要適用于VerilogHDL.1.GeneralRulesandGuidelines2.SymbolicConstants3.Routines4.SignalStateandTime2019-6-9謝謝觀賞331.CodingforVerificatio謝謝觀賞342.Testbench

下面講述VCtestbench和系統(tǒng)級(jí)testbench的標(biāo)準(zhǔn).這些規(guī)則和指南要求一個(gè)由激勵(lì)、序列控制、時(shí)鐘、driver和monitors之間的接口組成的testbench的體系結(jié)構(gòu).見Figure9-1.2019-6-9謝謝觀賞342.Testbench

下面講述VCtestb謝謝觀賞352.Testbench1.Clocking2.I/OandPads3.Messages4.Termination5.Synchronization6.ExternalInterfaceFunctions7.ConfigurationControl8.VCReset2019-6-9謝謝觀賞352.Testbench1.Clocking20謝謝觀賞363.DriversandMonitors

9.4.1TestbenchInterface9.4.2Drivers9.4.3Monitors9.4.4CommonCommandSet2019-6-9謝謝觀賞363.DriversandMonitors

9謝謝觀賞374.DetailedBehavioralModelforVC

ThedetailedbehavioralmodelforVC(blockbehaviorchecker)watchesrequeststhatcomeintoaunit,andverifiestheproperresponseonsomeotherinterface.Blockbehaviorcheckerverifiesthatoperationsarehappeningandthattheresultsarecorrect.DetailedbehavioralmodelsforVCshouldonlydescribedetailsthatarefunctionallyrelevantandnotconveyintellectualproperty.R9.5.1ConfigurethedetailedbehavioralmodelindependentoftheVCBlockbehaviorcheckersmustbeconfiguredviathetestbench,stimulus,and/ormonitors.ConfigurationofthebehavioralmustnotoccurbasedontheinternalVCstate.BehavioralsmaybeusedtopreloadstatesintotheVC.Reason:ProblemswiththeVCconfigurationmaybemasked.ThisprovidesindependentverificationoftheVCoperationandconfigurationmechanism.2019-6-9謝謝觀賞374.DetailedBehavioralMo謝謝觀賞385.DetailedBehavioralModelforMemory

Memoryarraymodelsareverificationcomponentsthatrepresentthefunctionalityofinternalandexternalmemorycircuits.Behavioralmodelsareusedinsteadofimplementation-orientedmodelstospeedupsimulation.ThemodelsarereusableVC.Reusabilityisenhancedbyfollowingtherulesandguidelinesinthissection.R9.6.1ArraysdimensionsmustbeparameterizedR9.6.2ROMsmusthavehighandlowlevelmodelsR9.6.3RAMsmusthavehighandlowlevelmodelsR9.6.4RAMmustnotbepre-loadedunlessitisloadableviaahardwareinterfaceR9.6.5ExternalSoCmemoryarraysmustberepresentedviaPLIcallsR9.6.6StimulusbinariesmustbeparsedandloadedintomemoryviaPLIfunctionsR9.6.7MemorymodelsmustseparatecontrolandstoragefunctionsG9.6.8Limitmemorysizestothesizerequiredbythestimulus2019-6-9謝謝觀賞385.DetailedBehavioralMo謝謝觀賞396.DetailedBehavioralModelforI/OPads

ThedriversandmonitorsmayinteractwiththeVCviapads.IftheSoCusesnon-standardpadcells,detailedbehavioralmodelsmustbeprovidedwiththeSoC.R9.7.1Thepadmodelmustbenamed<module>_pad.<extension>Reason:Easyidentificationinthedeliverablesdirectorystructure.2019-6-9謝謝觀賞396.DetailedBehavioralM謝謝觀賞407.StubModel

Stubmodel:Modelforadesignorverificationblockthathasthesamemodulenameandportlist,andbehaveslikearealblockinit’sinactivestate(i.e.,internalsignalscouldbetiedorfedthrough).Usedasaplaceholderwhentheblock’sfunctionalityisnotrequiredbutthetop-levelnetlistisnottobechangedThestubmodelisaverysimplemodelthatincludesthemoduledefinitionwithaportlistandmodelstheVCinitsinactivestate.Themodelmaybeusedasaplaceholderfortherealdesigntoassistindesigncompilationand/orsimplemodeling.2019-6-9謝謝觀賞407.StubModel

Stubmodel謝謝觀賞418.Stimulus

RandomsimulationisusedforexercisingboundarycasesoftheVC.Itisachievedbygeneratingpseudo-randomtransactionsforstimulus.Therandomnesscanbeeitherincontent(e.g.,randomdatainawritetransaction)orinappearance(e.g.,randomlychoosebetweenareadandawritetransaction).Constraintsarewrittentospecifytherangeofallowedrandomtransactions.Toolsareusedtorandomlygeneratetransactionwithintheallowedrange.Probabilityandweightingschemesareusedtobiastherandomselectionoftransactions.Thissectioncoversthepseudo-randomtestbenchstandards.Itincludesrulesandguidelinesforrandomgeneration.However,thepseudo-randomtestbenchstandardsarenotmandatoryandthefollowingrulesandguidelinesareapplicableonlyifrandomsimulationisdone.R9.9.1RandomstimulusmustincludeacheckingmechanismAreferencemodelorapredictionfunctionmustbeprovidedtoverifytherandombehavioroftheVC.Reason:Asopposedtonon-randomtestbencheswhereexpectedresultscanbeembeddedwithinthestimulus,randombehaviorsneedamoregeneralwaytodescribetheexpectedresults.R9.9.2Allrandomstimulusmustbeabletobecapturedanddeliveredasstand-alonetestsReason:TheVCintegratormustbeabletorunstaticallysavedrandomtestswithouttherandomgenerationfunction.9.9.1Random2019-6-9謝謝觀賞418.Stimulus

Randomsimul謝謝觀賞428.StimulusStimulusmustprovideanautomatedmechanismtodeterminepassorfail.Theverificationstimulusmustbeself-containedsothattheresultsarenotsubjecttointerpretation.R9.9.3ThecheckingmechanismusedmustbeautomatedReason:Thiseliminatespotentialforerrors.R9.9.4Allstimulusmustbeself-checkingStimulusmustprovideameansforautomatedself-checking.Whenstimulusfails,anerrormustbeindicated,failingthestimulusorregression.AllstimulusmustrelyonandetailedbehavioralmodelforVCtocheckresultsduringruntimeorthestimulusmustincludecheckingforexpectedresults.Reason:Thisprovidesawayforautomaticcheckingofverificationstimulusresultsandeliminatespotentialforerrors.R9.9.5ErrorsmustbedetectedatthepointoffailureIdentificationofthefailuresmustbeatthepointoffailureandnotpostprocessedasoftenaspossible.Reason:Reducesthetimespentdebuggingfailures.R9.9.6SimulatorerrorsandwarningsmustbedetectedPost-processingscriptsmusttakeintoaccountsimulatormessages(i.e.,compilation,invocationerrors,etc.).Reason:Ensuresthatstimuluswasproperlyexecuted.9.9.2Checking2019-6-9謝謝觀賞428.StimulusStimulusmust謝謝觀賞438.StimulusPartitioningcanimpacttheeasewithwhichamodelcanbeadaptedtoanapplication.Patternsmustbepartitionedtofacilitateportabilitytodifferentchips.Properpartitioningallowstheeasyomissionofpatternswhosefunctionsand/orpinsarenotbeingutilizedonaparticularchip.Patternsareabletobeused“asis”withoutmodifications.Thisdirectlyreducesstimulusdebugtime.R9.9.7AnystimulusthatdependsonanotherVCmustbepartitionedAnystimulusthatdependsonanotherVCmustbepartitioned.AnyaccessestofunctionsoutsideofaVCmustbedonewithamacroortask.Reason:Onfutureproducts,thedependentVCmaynotexist.Aproperlypartitionedstimulussuiteallowsfortheeasyidentificationandportingofpatternsthatspecificallydependonthatmodule.R9.9.8ModulepatternsmustbepartitionedbasedonthemodeofoperationandfunctionalityThepatternsmustbeinindividualfilesfortheregressionruns.Thestimulusfilenamingmustfollowtheconventionsoutlinedin9.9.4Naming.Reason:Havingmodularandindependentstimulusallowsfasteridentificationofproblemsinthefailingtests.R9.9.9TimingCriticalpatternsmustbepartitioned.Anypatternsthatareverifyingatimingcriticalpathmustbepartitionedintoaseparatestimulus.9.9.3Partitioning2019-6-9謝謝觀賞438.StimulusPartitioning謝謝觀賞448.StimulusReason:Infutureproducts,thetimingpathmaynotexistduetore-synthesis.Inaddition,timingcriticalpatternsaretypicallypartdependentandcarefulconsiderationmustbetakenwhenportingthemtoanotherproduct.R9.9.10TestModepatternsmustbepartitionedAnystimulusthatrequiresatestmodemustbepartitionedintoaseparatestimulus.Testmodeisanoperatingconfigurationthatallowshardwaretobetestedmoreeasilythanitwouldbeinnormaloperatingconditions.Thesetestsmayberuninmastermode,slavemode,etc.andshouldfollowthenamingconventionoutlinedinR9.9.14.Thetestsshouldbepartitionedseparatelyfromtherestoftheteststimulussinceaspecialmodeofoperationisrequired.Reason:Typically,atestmodeisdifferentondifferentproducts,thereforecarefulconsiderationmustbetakenwhenportingtestmodepatternstoanotherpart.R9.9.11Stimulusmustbepartitionedintostart-up,body,andshutdownsectionsReason:Reuseofbodycode.Start-upandshutdowncodemaybedifferentwhenrunningatthesystem,SoC,ormodulelevel.Ifthestimulusispartitioned,reusabilityisenhanced.G9.9.12ModulepatternsshouldbepartitionedbaseduponfunctionalityIndividualpatternsshouldbepartitionedintoseparatefilesbaseduponfunctionaltestcases.Partitioningshouldbedonetoavoidredundancyandensureproperorderingoftests.Reason:Atestpatternthatchecksasmallnumberoftestcasesallowsfasteridentificationofproblemsinthefailingstimulusandallowseasiergenerationoftestvectors.Example:Thetestordershouldexercisethereadandwritecapabilityofaregisterpriortotestingthefunctionofaregister.9.9.3Partitioning2019-6-9謝謝觀賞448.StimulusReason:Infu謝謝觀賞458.StimulusThefollowingsectioncontainsrulesandguidelinestospecifynamingandconventionsforverificationstimulusfilesanddirectories.R9.9.13StimulusmustindicatethestimulusversionatruntimeStimulusbinariesmustdisplaytheirrevisioncontrolnumberatruntimethatidentifiestheversionofthesourcecode.Reason:Failcorrelationtostimulusversion.R9.9.14Stimulussourcefilesmustbenamed<module_name>_<mode>_<description>Themodemustbeasinglewordusedtoindicatetheoperatingenvironmentofthetest.Usersmaydefineadditionalmodenamestothosefoundinthetablebelow.Reason:Thisimprovesreadabilityandmakesiteasytoidentifythemoduleandmodeofoperationtowhichthestimulusisassigned.Example:<module_name>_slave_register_tests.ForexampleseeTable9-3.Forslavemode,“slave”mustbeusedinthemodefieldand“intmemandextmem”mustbeusedformastermodepatterns.“Emul”mustbeusedforemulationmode.Newmodesmaybecreatedbutmustbedocumentedintheverificationguide.Morethanonefieldisallowedforthedescription,however,itmustresideafterthemodefield.R9.9.15StimulusfilenamesmustbelowercaseStimulusnamesmustbeinlowe