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

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

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

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

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

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

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

對(duì)某個(gè)IP的功能（如：單元測試）進(jìn)行驗(yàn)證的過程。系統(tǒng)驗(yàn)證

對(duì)包含一個(gè)或多個(gè)IP的SoC進(jìn)行功能驗(yàn)證的過程。概述6適合目的性驗(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)仿真、半形式化仿真）軟、硬件協(xié)同驗(yàn)證硬件仿真物理樣機(jī)虛擬樣機(jī)概述7目的性驗(yàn)證——?jiǎng)討B(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)降低?；谥芷诘姆抡妫夯谥芷诘姆抡娌捎昧瞬煌姆椒ā＿@種仿真不再具有內(nèi)部周期時(shí)鐘的概念，它在單個(gè)周期中對(duì)狀態(tài)及/或各端口之間進(jìn)行邏輯評(píng)估。由于每個(gè)邏輯元素在每個(gè)周期中只賦值一次，因此這種方法極大地縮短了執(zhí)行時(shí)間。8目的性驗(yàn)證——?jiǎng)討B(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)證的臨界狀態(tài)、臨界序列以及依賴于數(shù)據(jù)的狀態(tài)。用這種方法，任何算法錯(cuò)誤都能在設(shè)計(jì)周期的早期就能被發(fā)現(xiàn)和更正。9目的性驗(yàn)證——?jiǎng)討B(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)并將它送回仿真器。10目的性驗(yàn)證——?jiǎng)討B(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ò)。11目的性驗(yàn)證——形式驗(yàn)證形式驗(yàn)證利用數(shù)學(xué)方法對(duì)設(shè)計(jì)結(jié)果的功能進(jìn)行驗(yàn)證。它依賴于對(duì)設(shè)計(jì)的數(shù)學(xué)分析，無需使用驗(yàn)證測試序列。適用于目的性驗(yàn)證和等價(jià)性檢驗(yàn)。性能/模型驗(yàn)證

性能/模型驗(yàn)證是運(yùn)用公式化的數(shù)學(xué)技巧來校驗(yàn)設(shè)計(jì)的功能特性。模型驗(yàn)證器搜索一個(gè)設(shè)計(jì)在所有可能條件下的狀態(tài)空間，去尋找通過仿真很難發(fā)現(xiàn)的缺陷。模型驗(yàn)證不需要建立任何測試平臺(tái)，其要驗(yàn)證的性質(zhì)是用以特殊的規(guī)范語言描述的查詢表形式。當(dāng)模型驗(yàn)證工具發(fā)現(xiàn)錯(cuò)誤的時(shí)候，它會(huì)產(chǎn)生自初始狀態(tài)開始，到行為或特性出錯(cuò)的地方為止的完全搜索路徑。包含數(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ì)報(bào)告錯(cuò)誤。12目的性驗(yàn)證——形式驗(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ā)生的原因。13目的性驗(yàn)證——軟、硬件協(xié)同驗(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)試。雖然協(xié)同驗(yàn)證環(huán)境的建立需要大量的時(shí)間和豐富的經(jīng)驗(yàn)，但是使用軟、硬件聯(lián)合驗(yàn)證技術(shù)的回報(bào)也是十分豐厚的。首先，使用軟、硬件協(xié)同驗(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é)果是，軟、硬件協(xié)同驗(yàn)證技術(shù)通過在設(shè)計(jì)的早期就很快的解決了問題而提高了整個(gè)產(chǎn)品開發(fā)周期的質(zhì)量，節(jié)省了時(shí)間和金錢。

14目的性驗(yàn)證——硬件仿真硬件仿真器是通常由某些可重構(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ì)流程中是介于硬件和軟件之間的。15目的性驗(yàn)證——硬件仿真有很多不同的體系結(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)證方法。硬件仿真器在某種程度上可以看作有限精度的樣機(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ù)目。16目的性驗(yàn)證——物理樣機(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ì)有不同的性能。17目的性驗(yàn)證——虛擬樣機(jī)一個(gè)虛擬樣機(jī)就是一個(gè)產(chǎn)品、一個(gè)元件或一個(gè)系統(tǒng)的計(jì)算機(jī)模擬模型。同其它基于其自身特性的“模型”術(shù)語不一樣的是，“虛擬樣機(jī)”這個(gè)術(shù)語并不是指任何特殊的模型特性，而指在設(shè)計(jì)流程中做模型的角色。一般來說，一個(gè)虛擬模型應(yīng)該支持下列任務(wù)：試探開發(fā)設(shè)計(jì)的替代品證明設(shè)計(jì)的概念測試需求的滿意度和正確度虛擬樣機(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ī)需要有詳細(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ù)目。

18等價(jià)性驗(yàn)證確定性仿真：給模型施加明確定義的信號(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í)遷移。119等價(jià)性驗(yàn)證——形式化等性檢驗(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)。20等價(jià)性驗(yàn)證——形式化等性檢驗(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ǔ)器元件邊界的簡單操作。121等價(jià)性驗(yàn)證——物理驗(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)。22驗(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í)行的好壞程度。23驗(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)行。驗(yàn)證什么？---功能驗(yàn)證textspecificationdesignspecificationdesign??理解RTL實(shí)現(xiàn)功能驗(yàn)證驗(yàn)證過程示意圖功能驗(yàn)證yesno驗(yàn)證什么？--形式驗(yàn)證形式驗(yàn)證等價(jià)性檢測：兩種不同的結(jié)構(gòu)或者行為描述

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

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