SoC設(shè)計方法與實現(xiàn)SoC功能驗證(1)第九章SoC設(shè)計方法與實現(xiàn)功能驗證概述及驗證方法功能驗證概述及驗證方法驗證規(guī)劃基于斷言的驗證內(nèi)容大綱通用驗證方法學功能驗證概述及驗證方法隨著設(shè)計的進行，越接近最后的產(chǎn)品，修正一個設(shè)計缺陷的成本就會越高。新的驗證方法不斷出現(xiàn)，提高驗證效率、在設(shè)計的早期發(fā)現(xiàn)問題。功能驗證功能驗證的概念一般是指設(shè)計者通過各種方法比較設(shè)計完成的電路和設(shè)計文檔規(guī)定的功能是否一致，保證邏輯設(shè)計的正確性。不包括面積、速度、功耗等硬件實現(xiàn)的性能檢測。SoC功能驗證模塊內(nèi)驗證內(nèi)容主要是模塊功能，如算法、數(shù)據(jù)傳輸?shù)取Ｃ恳粋€功能是獨立的，通常比較容易找到設(shè)計錯誤。模塊內(nèi)部的設(shè)計錯誤通?？梢酝ㄟ^直接仿真就能捕獲到。芯片層把所有模塊的獨立驗證集成，在芯片頂層（top-level）執(zhí)行。由SoC架構(gòu)的復雜性所決定，這一層的驗證是一項艱難的任務(wù)。系統(tǒng)應(yīng)用層需要盡可能模仿真實的應(yīng)用程序和應(yīng)用環(huán)境。SoC功能驗證的發(fā)展趨勢新的方法學及更好的工具理解系統(tǒng)容易找到產(chǎn)生問題的原因可重用驗證模塊驗證自動化通用的驗證方法學基于仿真的功能驗證方法仿真硬件模擬形式驗證及半形式驗證仿真驗證平臺示例：帶約束的隨機激勵生成，保證產(chǎn)生的激勵的合法性。隨機激勵生成x1和x2為系統(tǒng)的兩個輸入，它們經(jīng)過獨熱碼編碼器編碼之后產(chǎn)生與被驗證設(shè)計（DUV）直接相連的輸入。輸入約束：in[1]+in[3]+in[2]<=1產(chǎn)生有效的隨機測試激勵x1x2帶約束的隨機測試向量生成器被驗證器件（DUV）in[1]+in[2]+in[3]<=1in[1]in[2]in[3]可視化的波形檢查響應(yīng)的檢查直觀，但不適用于復雜系統(tǒng)設(shè)計。自動比對檢查通過相應(yīng)的檢測模型或驗證模型來自動完成輸出結(jié)果的比對。覆蓋率的檢測覆蓋率數(shù)據(jù)通常是在多個仿真中收集的。覆蓋率的模型由針對結(jié)構(gòu)覆蓋率（StructuralCoverage）和功能覆蓋率（FunctionalCoverage）兩種目標而定義的模型所組成?？杉毣癁椋河邢逘顟B(tài)機覆蓋率（FSMCoverage）表達式覆蓋率（ExpressionCoverage）交叉覆蓋率（CrossCoverage）斷言覆蓋率（AssertionCoverage）硬件模擬器硬件模擬器（Emulator），使用硬件來模擬設(shè)計基于FPGA的硬件系統(tǒng)成為硬件模擬器的主流提供系統(tǒng)級測試環(huán)境接近實際芯片運行速度的設(shè)計原型由大型FPGA陣列組成的硬件模擬器形式驗證邏輯等效性檢查。驗證兩個時序邏輯設(shè)計再每一個有效的狀態(tài)是否相等。靜態(tài)時序分析一起，構(gòu)成設(shè)計的靜態(tài)驗證?？梢垣@得最大的驗證覆蓋率。但不檢查設(shè)計的功能。模型檢測給出一個系統(tǒng)的模型，自動檢查該模型是否滿足定義。主要應(yīng)用于屬性檢查。半形式驗證在行為層的仿真結(jié)束后，采用形式驗證的方法檢測是否有不滿足規(guī)范的地方。這些“規(guī)范”通常采用“斷言”描述“屬性”通過仿真中報錯，找出設(shè)計中的錯誤。通過形式驗證，可以證明“錯誤”不會發(fā)生。通過屬