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

用于驗證的工程師的人數是RTL設計工程師的兩倍。

當一個設計完成的時候驗證代碼的長度占總代碼長度的80%。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

宏單元驗證：可復用單元（模塊）的驗證。IP級別。系統級驗證：驗證的前提是各個單元模塊是已經經過驗證