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