哈工大功能驗證技術(shù)

功能驗證技術(shù)概述驗證的基本概念驗證：保證某種形式的轉(zhuǎn)換是符合我們所期望的。它是一個復(fù)雜的過程。功能驗證：保證設(shè)計正確的實現(xiàn)了規(guī)范所定義的功能。形式驗證：形式驗證采用數(shù)學(xué)的方法來驗證一個設(shè)計的不同描述是等價的。平等性檢測、模型檢測。驗證平臺（Testbench)：一段代碼用來對一個設(shè)計產(chǎn)生預(yù)先決定了的輸入序列，然后選擇性的觀察響應(yīng)，是一個封閉式的系統(tǒng)。概述驗證面臨的挑戰(zhàn)驗證的主導(dǎo)地位SOC設(shè)計的關(guān)鍵是IP復(fù)用，IP復(fù)用的關(guān)鍵是信任，信任的關(guān)鍵是完整正確的驗證。在當(dāng)今百萬門級的ASIC，IP，SoC設(shè)計中，驗證消耗了大約70%的設(shè)計努力。

用于驗證的工程師的人數(shù)是RTL設(shè)計工程師的兩倍。

當(dāng)一個設(shè)計完成的時候驗證代碼的長度占總代碼長度的80%。

驗證要解決的問題如何保證驗證是充分的？如何實現(xiàn)驗證的自動化？概述驗證要解決的問題這個設(shè)計的功能是否正確？測試要解決的問題一個正確的設(shè)計，在物理實現(xiàn)過程中是否有制造缺陷？二者的相同點施加激勵---〉觀看響應(yīng)二者的不同點驗證施加的激勵要人來編寫測試施加的激勵是工具自動產(chǎn)生的，響應(yīng)也是自動計算出來的。整個過程完全的自動化。功能驗證與芯片測試的差別5功能驗證分類從驗證方法上分：目的性驗證

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

目的是驗證設(shè)計過程中產(chǎn)生的不同層次的設(shè)計結(jié)果功能是否符合“黃金模型”。從驗證對象上分：IP驗證

對某個IP的功能（如：單元測試）進行驗證的過程。系統(tǒng)驗證

對包含一個或多個IP的SoC進行功能驗證的過程。概述6適合目的性驗證技術(shù)動態(tài)驗證

動態(tài)驗證是在一系列激勵的作用下，對以下幾個方面的測試：一個設(shè)計方案的一個或幾個模塊、某設(shè)計的硬件實現(xiàn)等。靜態(tài)功能驗證靜態(tài)功能驗證利用公式化的數(shù)學(xué)技巧來進行驗證而不使用驗證測試序列。其測試方法還沒有統(tǒng)一的工業(yè)標準，說法比較含糊。

形式驗證動態(tài)－形式化混合驗證為了更好的發(fā)揮形式化驗證技術(shù)全面性的特點，在處理大型設(shè)計、更加廣泛的設(shè)計風(fēng)格的設(shè)計時使用。（符號仿真、半形式化仿真）軟、硬件協(xié)同驗證硬件仿真物理樣機虛擬樣機概述7目的性驗證——動態(tài)驗證技術(shù)概念：對一個模塊施加激勵信號并由這個模塊產(chǎn)生響應(yīng)信號的過程。在確定性仿真中，激勵信號被明確給出，而且模塊的響應(yīng)信號能夠預(yù)知并被檢測到?；谑录姆抡妫夯谑录能浖抡嫫魍ㄟ^事件的發(fā)生（一次一個事件）和在設(shè)計中進行傳播而進行操作直至獲得一個穩(wěn)定的狀態(tài)。該設(shè)計方案的模塊包含內(nèi)部周期時鐘的概念和功能性的概念。輸入的激勵信號的任何變化都將作為事件被檢測到，并將被傳遍設(shè)計的每個階段。由于輸入信號的到達不同時和底層被測元素的信號的反饋不同時，可以在每個時鐘周期對設(shè)計的某個元素評估多次。雖然這能提供高精度的仿真環(huán)境，但執(zhí)行速度有賴于設(shè)計的規(guī)模，在大型的設(shè)計中其驗證速度會相應(yīng)降低?；谥芷诘姆抡妫夯谥芷诘姆抡娌捎昧瞬煌姆椒ā＿@種仿真不再具有內(nèi)部周期時鐘的概念，它在單個周期中對狀態(tài)及/或各端口之間進行邏輯評估。由于每個邏輯元素在每個周期中只賦值一次，因此這種方法極大地縮短了執(zhí)行時間。8目的性驗證——動態(tài)驗證技術(shù)隨機模式仿真隨機地址和隨機控制信號被加入總線或信號流中，而且有一個或多個總線監(jiān)測器對這些信號進行監(jiān)控，以確?？偩€協(xié)議不會因為這些操作而產(chǎn)生誤操作。這種方法對總線驗證尤其適用。驗證測試序列是直接的，因為操作周期的產(chǎn)生并非純粹的隨機產(chǎn)生，而是以某種特殊的方式來強調(diào)設(shè)計。這種向量發(fā)生器可用來以特定的分配產(chǎn)生特定的傳輸周期，如：在偽隨機序列中產(chǎn)生20％的讀，30％的寫和50％的變址讀寫。類似的，在數(shù)據(jù)和地址領(lǐng)域中也可產(chǎn)生隨機序列，但是得在有限的范圍內(nèi)使用有限的離散數(shù)值。這些類型的仿真驗證用確定性仿真很難驗證的臨界狀態(tài)、臨界序列以及依賴于數(shù)據(jù)的狀態(tài)。用這種方法，任何算法錯誤都能在設(shè)計周期的早期就能被發(fā)現(xiàn)和更正。9目的性驗證——動態(tài)驗證技術(shù)硬件加速硬件加速是特指為加速某些仿真操作而將設(shè)計中部分或全部的模塊映射到硬件平臺上。最典型情況就是測試平臺仍然保留在軟件中運行，而被驗證的設(shè)計卻是在硬件加速器中運行。有些類型的加速器也能運行行為級的代碼，這種情況下，具體的時鐘周期的行為表現(xiàn)并沒有給出詳細的說明，因此，有可能會全部在硬件加速器中運行純確定性或隨機模式仿真。

硬件建模有些軟件仿真模型的設(shè)計元件難以實現(xiàn)，或者不夠精確。解決這個難題的方法就是運行硬件模型中的一個半導(dǎo)體元件，將它連接到軟件仿真器上。這個硬件模型的輸入是接收來自仿真器的信號，然后將該信號送到半導(dǎo)體元件中運行一個周期，最后獲得輸出信號并將它送回仿真器。10目的性驗證——動態(tài)驗證技術(shù)協(xié)議檢驗協(xié)議檢驗器指的是監(jiān)測接口的數(shù)據(jù)處理以及檢查任何無效操作的元件。如果在仿真器中有任何無效操作被檢驗到，檢驗器將會作標記。這種元件可以裝備在測試平臺中而不作為設(shè)計的部分。在這種應(yīng)用中，檢驗器僅僅在仿真時才起作用。當(dāng)然，協(xié)議檢驗器也可以植入設(shè)計之中，這樣檢驗器不僅可以在仿真的時候，而且可以在實際的物理設(shè)備進行的普通操作中都能查錯。不過，設(shè)計中植入的這種設(shè)備要能夠在門級進行綜合。預(yù)期結(jié)果檢驗是系統(tǒng)測試平臺的一部分。它對仿真結(jié)果與事先的規(guī)定——期望響應(yīng)文件進行比較。如果結(jié)果不符，將會報錯。11目的性驗證——形式驗證形式驗證利用數(shù)學(xué)方法對設(shè)計結(jié)果的功能進行驗證。它依賴于對設(shè)計的數(shù)學(xué)分析，無需使用驗證測試序列。適用于目的性驗證和等價性檢驗。性能/模型驗證

性能/模型驗證是運用公式化的數(shù)學(xué)技巧來校驗設(shè)計的功能特性。模型驗證器搜索一個設(shè)計在所有可能條件下的狀態(tài)空間，去尋找通過仿真很難發(fā)現(xiàn)的缺陷。模型驗證不需要建立任何測試平臺，其要驗證的性質(zhì)是用以特殊的規(guī)范語言描述的查詢表形式。當(dāng)模型驗證工具發(fā)現(xiàn)錯誤的時候，它會產(chǎn)生自初始狀態(tài)開始，到行為或特性出錯的地方為止的完全搜索路徑。包含數(shù)據(jù)通道的系統(tǒng)經(jīng)常包含很大很廣的狀態(tài)空間，對這樣的系統(tǒng)進行驗證就花費昂貴的存儲空間和大量的處理時間。所以模型驗證通常在控制密集設(shè)計的驗證中比數(shù)據(jù)通道密集設(shè)計驗證更加有效。模型驗證者通常能夠在各種合法輸入序列和合法的輸入狀態(tài)下，如模型驗證和性能一樣可以直接從仿真驗證出某種特定的條件總是真，最終為真還是永遠不會是真。這種性質(zhì)就是對設(shè)計的斷言，對仿真和模型驗證都十分有用。斷言表明了某些特定條件必須總是正確，就將該條件列入checker的職能范圍之內(nèi)，一旦在仿真中這種條件有偏離，checker就會報告錯誤。12目的性驗證——形式驗證理論證明基于理論證明技術(shù)的驗證系統(tǒng)通常支持某種基于選定形式的邏輯的規(guī)范語言，并支持一組以該語言命令的形式機械地構(gòu)造邏輯斷言的證明。一個使用基于理論證明技術(shù)的驗證系統(tǒng)的硬件設(shè)計的形式化驗證，通常包含：對設(shè)計模型(M)的初步描述，將由驗證系統(tǒng)支持的邏輯/規(guī)范語言的性能（P）的初步描述。在所有可能的輸入條件下M能夠正確地推出P的斷言，從而驗證性能P。證明標準的完備性保證了在所有可能的輸入狀態(tài)下，該設(shè)計的性能都是正確的。已經(jīng)有很多的理論證明系統(tǒng)在大型的設(shè)計中得以成功地運用，如在浮點指針單元和在復(fù)雜流水控制中。同模型校驗一樣，理論證明驗證也不需要創(chuàng)建任何驗證測試平臺，但是需要有待證明的性能公式。與模型校驗不一樣的是，理論證明驗證不受輸入規(guī)模和狀態(tài)空間的限制。因此，理論證明驗證更加適于基于數(shù)據(jù)通道的設(shè)計和高層應(yīng)用的功能驗證，如浮點指針單元和復(fù)雜流水控制中冒險的驗證等。同時，理論證明驗證還能用于性能檢查中，就如同在一個設(shè)計的兩個模型之間的等價性校驗一樣。但是對兩個模型的等價性檢驗而言，在運用系統(tǒng)驗證語言對兩個模型進行描述之后，還得給兩個模型寫一個合適的斷言并對之加以證明。通過理論證明的驗證的主要缺點就是它不如模型校驗?zāi)菢幼詣踊潭容^高。因為在通過理論證明的驗證中，用戶必須使用理論證明的命令進行交互式的證明。同時，另一個缺點就是在對某事件的證明失敗時，驗證系統(tǒng)無法自動構(gòu)造搜索指針。用戶必須通過人為的分析來尋找錯誤發(fā)生的原因。13目的性驗證——軟、硬件協(xié)同驗證在傳統(tǒng)的系統(tǒng)設(shè)計的串行流程中，首先構(gòu)造硬件，然后在硬件的基礎(chǔ)上編寫和調(diào)試系統(tǒng)軟件。但是在軟、硬件聯(lián)合驗證技術(shù)中，對系統(tǒng)硬件和軟件的驗證是同時進行的。在硬件被開發(fā)的同時，相應(yīng)的軟件也在硬件仿真平臺中執(zhí)行，這樣就實現(xiàn)了硬件和軟件的并行調(diào)試。雖然協(xié)同驗證環(huán)境的建立需要大量的時間和豐富的經(jīng)驗，但是使用軟、硬件聯(lián)合驗證技術(shù)的回報也是十分豐厚的。首先，使用軟、硬件協(xié)同驗證技術(shù)能夠在SOC芯片制造之前就能發(fā)現(xiàn)并糾正許多系統(tǒng)級漏洞和問題。在實際的處理器和固件模型中進行的仿真，結(jié)果會更加精確，而且同舊的使用總線傳輸模型的設(shè)計流程比較起來，可以進行更廣泛的驗證。而且，在仿真過程中，軟件也得到了調(diào)試和驗證。相應(yīng)的允許在芯片實際生成的同時，給系統(tǒng)的發(fā)展提供較高的發(fā)展速度。最終結(jié)果是，軟、硬件協(xié)同驗證技術(shù)通過在設(shè)計的早期就很快的解決了問題而提高了整個產(chǎn)品開發(fā)周期的質(zhì)量，節(jié)省了時間和金錢。

14目的性驗證——硬件仿真硬件仿真器是通常由某些可重構(gòu)邏輯（通常為現(xiàn)場可編程門陣列，如FPGA）組成的專門設(shè)計的硬件和軟件系統(tǒng)。編程這些系統(tǒng)以模仿設(shè)計目標的行為和功能，甚至達到將仿真過的設(shè)計同設(shè)計即將在其中操作的系統(tǒng)的剩余部分直接連接的程度。由于這些系統(tǒng)是以硬件為基礎(chǔ)的，因此，它們能夠提供與最終設(shè)計目標接近的電路仿真速度。這些幾千Hz的速度同以軟件為基礎(chǔ)的仿真所提供的幾十Hz的速度形成鮮明的對比。這種幾個量級的行為差異使得模擬技術(shù)能夠執(zhí)行在軟件硬件仿真時要用幾個月甚至幾年才能完成的大型驗證任務(wù)。這種驗證任務(wù)的例子包括數(shù)據(jù)集的處理如視頻數(shù)據(jù)流等，或者是有成千上萬行的軟件如操作系統(tǒng)的引導(dǎo)程序等。在帶有嵌入式處理器的SoC在轉(zhuǎn)化至硅片之前，在軟件在與周圍邏輯協(xié)同工作時，需要硬件仿真技術(shù)或樣機技術(shù)對軟件在嵌入的處理器上運行時的復(fù)雜功能進行驗證。正因為這樣，通常認為這種硬件仿真系統(tǒng)在并行設(shè)計流程中是介于硬件和軟件之間的。15目的性驗證——硬件仿真有很多不同的體系結(jié)構(gòu)都借用這種硬件仿真系統(tǒng)來提供靈活性、可控性、可視性和性能。這些體系結(jié)構(gòu)包括FPGA的互聯(lián)陣列，自定義處理器陣列，帶有可編程縱橫切換器的磁頭系統(tǒng)和可編程總線接口的系統(tǒng)等。這些不同的體系結(jié)構(gòu)能夠在設(shè)計容量、行為特性和最優(yōu)布局結(jié)構(gòu)方面能提供一定程度的折衷方案，并且力圖能夠兼容并輔助包括其他驗證技術(shù)如軟件模擬、時序驗證、形式化驗證和邏輯分析的驗證方法。硬件仿真器在某種程度上可以看作有限精度的樣機。通常硬件仿真器支持對設(shè)計的內(nèi)部節(jié)點保持高度的可觀察性，使設(shè)計在更類似于模擬而非真實物理樣機的方式除錯。事實上，因為軟件模擬器與仿真器交互工作的方式在本質(zhì)上與硬件模擬加速器相同，有時仿真器也用作模擬目的。雖然硬件仿真器有時候能夠接近最終設(shè)計的速度，但是，除非它們能夠同與最終設(shè)計一樣的系統(tǒng)相聯(lián)，否則，它們的速度仍將受到限制。另外，硬件仿真系統(tǒng)的成本往往限制了一個項目中允許的系統(tǒng)數(shù)目，反過來，這又限制了能夠同時運行硬件仿真的工程師的數(shù)目。16目的性驗證——物理樣機一種目標設(shè)計的硬件代替品，它的運行能夠“接近”目標設(shè)計平臺的性能。執(zhí)行速度能夠比軟件仿真系統(tǒng)的速度快出許多。物理樣機能夠支持以下功能：在SOC器件可用之前，應(yīng)用軟件和系統(tǒng)軟件的開發(fā)和調(diào)試系統(tǒng)的系統(tǒng)級性能測試目標設(shè)計的高性能仿真平臺，該設(shè)計能支持復(fù)雜測試周期具有支持硬、軟件聯(lián)合仿真的硬件平臺和軟件環(huán)境用于測試的邏輯分析接口目標設(shè)計的市場演示典型情況下，物理樣機可與目標系統(tǒng)速度相同的數(shù)量級范圍內(nèi)運行，因此，它的執(zhí)行速度能夠比軟件仿真系統(tǒng)的速度快出許多。這意味著全部的測試序列都能夠裝載到物理樣機中去，并同系統(tǒng)級驗證測試向量一起運行。在考慮到可以樣機化的設(shè)計的數(shù)目、執(zhí)行速度以及性能變化時間時，通過不同的方法得到的樣機就會有不同的性能。17目的性驗證——虛擬樣機一個虛擬樣機就是一個產(chǎn)品、一個元件或一個系統(tǒng)的計算機模擬模型。同其它基于其自身特性的“模型”術(shù)語不一樣的是，“虛擬樣機”這個術(shù)語并不是指任何特殊的模型特性，而指在設(shè)計流程中做模型的角色。一般來說，一個虛擬模型應(yīng)該支持下列任務(wù)：試探開發(fā)設(shè)計的替代品證明設(shè)計的概念測試需求的滿意度和正確度虛擬樣機可以在各個抽象的層次上構(gòu)建也可以包含一個多層次的混合體。在一個設(shè)計系統(tǒng)中可以有一個和幾個虛擬樣機同時存在，每個虛擬樣機都能完成上述所說的任務(wù)。為了能在更大的設(shè)計系統(tǒng)中發(fā)揮作用，一個虛擬樣機應(yīng)該對設(shè)計的元件或系統(tǒng)的接口進行定義。物理樣機需要有詳細的硬件和軟件設(shè)計描述，而虛擬樣機能夠更快、更有效、更加抽象而且在設(shè)計流程中能夠更早的加以構(gòu)建。因此，其中的一個區(qū)別就是，虛擬樣機作為一個計算機仿真器，比起物理樣機的常規(guī)操作來，能提供有關(guān)內(nèi)部狀態(tài)的更多的，無害的可視化信息。此外，與物理樣機相比較而言，虛擬樣機的一個主要缺點就是，它的操作速度同軟件仿真器的速度十分接近，因此就限制了在一定的時間內(nèi)所能完成的驗證數(shù)目。

18等價性驗證確定性仿真：給模型施加明確定義的信號，產(chǎn)生相應(yīng)的響應(yīng)，在將仿真結(jié)果與預(yù)期值比較。一旦在RTL級模型上的驗證平臺和驗證測試向量被開發(fā)出來，那么同樣地驗證向量集合也能在門級網(wǎng)表上對原設(shè)計進行仿真，以檢查結(jié)果是否相同。在有些情形下，也有可能在對同樣的設(shè)計的高層或者低層仿真過程中進行同樣的驗證測試。預(yù)期結(jié)果檢查：對仿真結(jié)果同先前指定了的預(yù)期響應(yīng)文件進行比較。出現(xiàn)任何錯誤的時候，檢查者就會報錯。黃金模型檢查：監(jiān)視一個設(shè)計中兩個模型的響應(yīng)，將響應(yīng)信號與輸入激勵相比較，并且對任何偏差作出標記。其中一個為“黃金模型”或可信任模型，而另外一個則是待證明的模型。一般情況下，這種比較不包括任何形式化驗證技術(shù)，兩個模型之間的響應(yīng)信號比較僅基于信號的變化。驗證測試序列的遷移：把系統(tǒng)級驗證測試序列應(yīng)用到設(shè)計的其它層次需要有可以將其遷移或轉(zhuǎn)換為設(shè)計的RTL級或網(wǎng)表級應(yīng)用序列格式的能力。包括：功能級向RTL級的遷移和RTL級向網(wǎng)表級遷移。119等價性驗證——形式化等性檢驗形式化等價性檢驗工具要證明的是：兩個設(shè)計從I/O接口和基于一個接一個的周期的角度來看功能上是等價的。形式化等價性檢驗通常用在設(shè)計的RTL級和門級網(wǎng)表級。在有些情形下，也能用于更高或者更低的模型。同軟件仿真相比，形式化等價性檢驗具有幾個優(yōu)點。首先，與仿真不同，形式化等價性檢驗?zāi)軌蛱峁┩暾牡葍r性檢驗，而仿真只驗證到一個驗證測試組是否在設(shè)計中運行的程度。另外，形式化等價性檢驗?zāi)軌蛟诤芏痰臅r間內(nèi)執(zhí)行完需要復(fù)雜仿真才能完成的任務(wù)，這就有利于將驗證和錯誤調(diào)試自動化。等價性檢驗工具通常會提供與小的獨立邏輯塊不匹配的詳細“反例”。

包括布爾等價性檢驗和時序等價性檢驗。20等價性驗證——形式化等性檢驗布爾等價性檢驗許多等價性檢驗工具是布爾等價性檢驗器，這意味著它們檢驗的是組合邏輯。運用這些工具，通常自動進行兩個設(shè)計的存儲元件（如觸發(fā)器、鎖存器等）間格式的比較，從而完成對名詞的映射。當(dāng)映射確定以后，相應(yīng)的工具就開始對存儲器的每對映射名詞的輸入的組合邏輯開始檢查是否等價。這意味著對每一種可能的輸入組合，組合邏輯輸出（也即存儲器元件的輸入）是相同的。

時序等價性檢驗有這樣一種情況：兩個設(shè)計的存儲元件的數(shù)目不同或排列不同，但是就輸入－輸出數(shù)據(jù)流的生成以及在兩個狀態(tài)機之間給定的某些初始狀態(tài)方面兩者是等價的，這就是時序等價。這樣的例子如有限狀態(tài)機的兩種實現(xiàn)方式：一個采用全譯碼方式，即用3個鎖存器編碼8個狀態(tài)；另一種采用one-hot編碼，用8個鎖存器為8個狀態(tài)編碼。然而這兩個狀態(tài)機都有同樣的輸出/入數(shù)據(jù)信號，都開始于相同的初始狀態(tài)，有相同的輸入數(shù)據(jù)流。時序等價性檢驗比布爾等價性檢驗存在更大的困難。因此能夠執(zhí)行這種任務(wù)的工具更加稀少。有很多的布爾等價性檢驗確實支持時序等價性檢驗，允許檢驗很小的有限狀態(tài)機（通常用戶必須手動地支持一些等價狀態(tài)賦值的映射，因而限制了這種檢驗只能適合于小規(guī)模的狀態(tài)機），或者允許檢驗?zāi)承┙M合邏輯器件跨越存儲器元件邊界的簡單操作。121等價性驗證——物理驗證物理驗證就是通過檢驗圖形設(shè)計的數(shù)據(jù)庫以確信物理實現(xiàn)確實是原始邏輯設(shè)計的正確表述。物理驗證包括以下三個部分：電學(xué)規(guī)則檢驗（以下簡稱ERC）、設(shè)計規(guī)則檢驗（以下簡稱DRC）及布線和電路圖檢驗（以下簡稱LVS）。標準的圖形數(shù)據(jù)庫形式是GDSII－數(shù)據(jù)流。一個設(shè)計的GDSII－數(shù)據(jù)流數(shù)據(jù)庫包括電路的多邊形表述，并對目標設(shè)計劃分成不同的設(shè)計層次。ERC指的是檢驗圖形數(shù)據(jù)庫是否有與電學(xué)設(shè)計規(guī)則相違背之處。這些電學(xué)規(guī)則就是流程說明，并包含檢驗是否有無用輸入，浮點輸入和裝載沖突等。還檢驗連接是否合法，如短路和短接。DRC指的是檢驗圖形數(shù)據(jù)庫是否有與設(shè)計流程規(guī)則相違背之處。這些規(guī)則收集在DRC規(guī)則文件中，并包含層與層之間的空間檢驗、布線寬度、層與層的相互重疊等。LVS就是檢驗提取的圖形數(shù)據(jù)庫是否有與“黃金”網(wǎng)表相違背之處。LVS工具從多邊形數(shù)據(jù)中構(gòu)建網(wǎng)表以及從物理布局中提取器件模型。提取出的網(wǎng)表需和“黃金”模型保持一致。所有的器件和互連都必須嚴格地相匹配。其他的影響時序的物理驗證如信號的完整性、串?dāng)_、金屬遷移、噪音等不在功能驗證論述的范圍內(nèi)。22驗證衡量方法

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

·語句覆蓋率：表明每條語句被執(zhí)行的次數(shù)；·信號觸發(fā)覆蓋率：表明設(shè)計信號中的哪一位被觸發(fā)；·有限狀態(tài)機覆蓋率：表明進行了多少個有限狀態(tài)機的轉(zhuǎn)變過程，可以視為路徑覆蓋率的一部分；·被訪問狀態(tài)覆蓋率：表明有限狀態(tài)機有多少個的狀態(tài)參與了仿真；·觸發(fā)覆蓋率：表明每個進程是否被敏感度列表中的每個信號唯一觸發(fā)到；·分支覆蓋率：表明哪一條“case”或者“if…else”語句被執(zhí)行；·表達式覆蓋率：表明“if”條件布爾表達式或賦值布爾表達式的執(zhí)行的好壞程度；·路徑覆蓋率：表明通過“if…else”和“case”順序結(jié)構(gòu)的哪條路徑被執(zhí)行；·信號覆蓋率：表明狀態(tài)信號或ROM尋址的執(zhí)行的好壞程度。23驗證衡量方法功能覆蓋率功能覆蓋率是一種由用戶定義的、反映在驗證過程中被運行到的功能點的范圍的衡量方法。功能點可以是對VC用戶而言可視的體系結(jié)構(gòu)特點，也可以是主要的微結(jié)構(gòu)特征。通常情況下，這些特征不能從實現(xiàn)中自動生成，因此需要在驗證testbench中的一些規(guī)范。功能覆蓋率數(shù)據(jù)一般是一些時序行為（如總線的交易）和一些數(shù)據(jù)（如交易源、目的和優(yōu)先級等）的交叉組合。附加覆蓋率信息可以從功能覆蓋率點的交叉引用中得到。比如，在一個器件的兩個引腳之間進行的數(shù)據(jù)處理的相互關(guān)系，或者在一個處理器中指令和中斷的關(guān)系等。與代碼覆蓋率不一樣的是功能覆蓋率的指標需要開發(fā)者自行定義。一個好的定義不僅與驗證平臺緊密相關(guān)，而且應(yīng)覆蓋VC中的所有主要特征。因此，功能覆蓋率比代碼覆蓋率的要求更加嚴格。經(jīng)驗表明，功能覆蓋率與bugs/每周衡量法之間有緊密聯(lián)系。雖然有些方面可以在更低或者更高的層次上評估，功能覆蓋率分析通常還是在設(shè)計的RTL級上進行。驗證什么？---功能驗證textspecificationdesignspecificationdesign??理解RTL實現(xiàn)功能驗證驗證過程示意圖功能驗證yesno驗證什么？--形式驗證形式驗證等價性檢測：兩種不同的結(jié)構(gòu)或者行為描述

在功能上是等價的。模型檢測：證明特定結(jié)構(gòu)符合預(yù)期的行為門級網(wǎng)表1門級網(wǎng)表2等價性檢測：掃描鏈的插入功能相等？模型檢測：文本規(guī)范設(shè)計應(yīng)該具有的行為形式化的編程語言設(shè)計模型檢測形式驗證示意圖驗證的方法方法黑盒子模型白盒子模型灰盒子模型驗證的級別單元級的驗證：基本模塊的驗證。

宏單元驗證：可復(fù)用單元（模塊）的驗證。IP級別。系統(tǒng)級驗證：驗證的前提是各個單元模塊是已經(jīng)經(jīng)過驗證