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