產(chǎn)品概述
FPGA設(shè)計越來越復(fù)雜，成本越來越高，盡早發(fā)現(xiàn)錯誤能降低風(fēng)險，但傳統(tǒng)的FPGA功能驗證周期過長，且功能仿真很難達到覆蓋率，故障分析效率很低，此外，編寫大量的測試用例也會耗費大量的時間，因此，傳統(tǒng)的功能驗證已經(jīng)難以滿足現(xiàn)在的設(shè)計。
現(xiàn)在一般會使用形式化驗證工具作為替代，形式化驗證就是從數(shù)學(xué)算法上完備地證明設(shè)計功能的正確性，能實現(xiàn)功能驗證的快速覆蓋，再針對未覆蓋的特殊功能編寫測試用例，進行完善測試，它的主要優(yōu)點是完備性，能夠快速的達到一定程度的驗證覆蓋。
DV Verify采用形式化方式對FPGA設(shè)計進行功能驗證，包含代碼缺陷自動檢查功能，能夠自動生成與代碼結(jié)構(gòu)和安全性相關(guān)的功能斷言，快速發(fā)現(xiàn)如數(shù)組越界等代碼缺陷，它提供形式化分析引擎，可以對自定義功能斷言進行驗證，并提供覆蓋率度量分析。
DV Verify包含DV Inspect，屬性檢查，覆蓋率檢查和故障注入四個部分，DV Inspect用于快速發(fā)現(xiàn)模塊中的錯誤，屬性檢查運用斷言進行屬性檢查，覆蓋率檢查提供特有的覆蓋率驅(qū)動的驗證，故障注入則能模擬各種故障場景。
DV Verify工作流程
功能特性
DV Inspect主要用于快速發(fā)現(xiàn)模塊中的錯誤，能夠在設(shè)計送入綜合器編譯之前執(zhí)行功能驗證，檢查的效率很高且檢查的種類很多。這個工具能夠進行結(jié)構(gòu)檢查、安全性檢查和檢查。
DV Inspect工作流程
結(jié)構(gòu)檢查
結(jié)構(gòu)檢查能快速進行RTL代碼的語法和語義分析，還可以在GUI中對兩次的檢查結(jié)果進行比對，發(fā)現(xiàn)改動后檢查結(jié)果的不同，便于快速定位錯誤原因。
安全性檢查
安全性檢查包括以下檢查內(nèi)容：
安全性檢查的內(nèi)容
檢查
檢查包括無效代碼檢查、FSM檢查和翻轉(zhuǎn)檢查。
●無效代碼檢查以輸入源碼的各個分支為目標(biāo)，檢查這些分支條件是否都被執(zhí)行。包括if-then-else和switch條件，以及default都會分析，對避免沒有考慮的條件特別有用，通過x賦值，還能檢查仿真和綜合結(jié)果不匹配的情況。
●狀態(tài)機的檢查主要是檢查狀態(tài)機中沒有死循環(huán)的存在，檢查狀態(tài)機在復(fù)位時是否正確回到初始狀態(tài)。工具自動識別源碼中的狀態(tài)機，對發(fā)現(xiàn)多個狀態(tài)機間的錯誤內(nèi)部連鎖條件十分有用。
●翻轉(zhuǎn)檢查主要是分析信號的開關(guān)能力。這項檢查依賴于信號類型。例如如果信號是布爾型，工具就要檢查它是否能從0變?yōu)?，從1變?yōu)?。
屬性檢查
這個功能就是通過編寫功能斷言進行屬性驗證，可以在沒有Testbench的條件下開始驗證設(shè)計，支持標(biāo)準(zhǔn)的基于斷言的驗證形式驗證流程。它支持的斷言語言包括：SVA、PSL和OVL。
屬性檢查具有獨特結(jié)構(gòu)的斷言調(diào)試器，波形調(diào)試中使用不同顏色區(qū)分被測信號，指向故障原因，以及帶有活動值注釋和主動驅(qū)動程序跟蹤的源代碼分析。在斷言開發(fā)過程中常見且耗時的其中一個步驟中，工具提供這種集成且高度直觀的調(diào)試環(huán)境使工程師能夠大大加快調(diào)試周期。
屬性檢查工作流程
覆蓋率檢查
覆蓋率檢查提供特有的覆蓋率驅(qū)動的驗證，它可以對形式化驗證過程進行定量分析，與仿真覆蓋度量合并，提供必要的覆蓋度量來確認(rèn)安全關(guān)鍵功能的徹底驗證，評估驗證進展并確定仍有待完成的工作，而驗證中的間隙可以被自動標(biāo)注在驗證計劃上，并用不同的顏色標(biāo)注起來，表明不同的覆蓋程度，覆蓋率報告能夠?qū)С鰹閁CDB格式，可以和仿真中產(chǎn)生的覆蓋率報告進行合并。
Quantify可以將仿真結(jié)構(gòu)覆蓋衡量測試平臺和測試套件對設(shè)計的覆蓋程度，以及基于模型的變異覆蓋衡量斷言對設(shè)計的覆蓋程度，這兩個指標(biāo)集成到單個覆蓋視圖中。此外，工程師還可以編寫驗證計劃，以表明哪些目標(biāo)將通過仿真、上板仿真和形式化工具來實現(xiàn)。可以將結(jié)果集成并注釋回計劃，包括的形式度量，如有界的和完整的證明。
故障注入
形式化故障注入測試系統(tǒng)（FIA）能夠簡單靈活地自動模擬各種故障場景，從應(yīng)被視為故障注入候選的信號開始，無需更改設(shè)計或執(zhí)行代碼檢測步驟，提高對設(shè)計行為破壞的可見性，加快對失敗斷言的分析，消除了對特殊驗證流或環(huán)境的需求，減少了工程工作。工程師可以從預(yù)先定義的庫中選擇或自定義故障模式，通常情況下，場景包含了位級故障位置、故障注入時間和故障類型的大量組合。
故障注入系統(tǒng)工作流程
