必須優(yōu)化正式驗(yàn)證流程中的初始網(wǎng)表，因此測(cè)試設(shè)計(jì)需要額外的邏輯。在這里，我們提供16 nm節(jié)點(diǎn)的形式驗(yàn)證流程和調(diào)試技術(shù)。

形式驗(yàn)證是比較用硬件描述語(yǔ)言 （HDL） 編寫的兩個(gè)設(shè)計(jì)以確保它們?cè)诠δ苌系刃У倪^程。作為功能驗(yàn)證的一個(gè)子集，it 提供了在不使用仿真的情況下檢查兩個(gè)設(shè)計(jì)的功能等效性的關(guān)鍵第一步。

這些功能等價(jià)物中的第一個(gè)稱為參考設(shè)計(jì)/黃金設(shè)計(jì)，其中基于傳輸級(jí)（RTL）代碼（如Verilog，System Verilog或VHDL）的模型用作參考網(wǎng)表。該網(wǎng)表根據(jù)第二種設(shè)計(jì)中的相應(yīng)網(wǎng)表進(jìn)行驗(yàn)證，稱為實(shí)現(xiàn)或修訂設(shè)計(jì)（圖 1）。為簡(jiǎn)單起見，在本文的其余部分中，參考/黃金設(shè)計(jì)將稱為“初始設(shè)計(jì)”，而實(shí)現(xiàn)設(shè)計(jì)/修訂設(shè)計(jì)稱為“目標(biāo)設(shè)計(jì)”。

圖1.形式驗(yàn)證方法的表示

下表顯示了可用于比較初始設(shè)計(jì)與目標(biāo)設(shè)計(jì)的組合。

表 1.初始設(shè)計(jì)與目標(biāo)設(shè)計(jì)

此過程要求初始網(wǎng)表經(jīng)過不同級(jí)別的優(yōu)化，這反過來(lái)又需要額外的測(cè)試設(shè)計(jì) （DFT） 邏輯。盡管有這些要求，但形式驗(yàn)證過程不應(yīng)改變?cè)O(shè)計(jì)的邏輯功能。

形式驗(yàn)證的類型

通常使用兩種形式驗(yàn)證技術(shù)：

等價(jià)性檢查 – 邏輯等效性檢查是一種技術(shù)，它采用兩種可以具有相同或不同抽象級(jí)別（即算法、RTL 或門級(jí)）的設(shè)計(jì)，并檢查它們之間的任何功能差異。

等價(jià)性檢查進(jìn)一步分為組合或順序檢查。組合等價(jià)性檢查包括通過將從初始設(shè)計(jì)一對(duì)一的翻牌映射到目標(biāo)設(shè)計(jì)來(lái)檢查組合邏輯，而如果一對(duì)一翻牌映射之間存在不同的組合邏輯，但如果給定相同的輸入，設(shè)計(jì)仍應(yīng)能夠產(chǎn)生相同的輸出，則使用順序等價(jià)檢查。通常，如果 SoC 或 ASIC 設(shè)計(jì)經(jīng)歷了各種轉(zhuǎn)換，如重定時(shí)、節(jié)能設(shè)計(jì)優(yōu)化等，則使用順序等效性檢查。

屬性檢查或基于斷言的驗(yàn)證 （ABV） –屬性檢查或 ABV 檢查行為是否可行，并使用屬性檢查器工具來(lái)證明設(shè)計(jì)符合其所有規(guī)范。屬性檢查使用數(shù)學(xué)程序來(lái)證明設(shè)計(jì)的準(zhǔn)確性。

屬性檢查通常使用兩種屬性語(yǔ)言：間隔時(shí)態(tài)邏輯 （ITL） 和系統(tǒng)驗(yàn)證斷言 （SVA）。一旦這些被編碼，它們就可以傳遞給數(shù)學(xué)工具，數(shù)學(xué)工具預(yù)測(cè)結(jié)果是保持或失敗。持有ITL/SVA意味著所有屬性都已經(jīng)過檢查，并保留了初始設(shè)計(jì)的屬性。ITL/SVA失敗意味著設(shè)計(jì)行為不是有意的，并且目標(biāo)設(shè)計(jì)存在沖突。

形式驗(yàn)證的要求

功能等效性檢查通常需要使用相同的測(cè)試向量對(duì)兩個(gè)HDL設(shè)計(jì)進(jìn)行仿真。但是，隨著ASIC技術(shù)的縮小和電路復(fù)雜性的增加，不可能使用仿真來(lái)驗(yàn)證電路功能，因?yàn)榉抡婵赡軙?huì)運(yùn)行數(shù)月。因此，形式化驗(yàn)證通過節(jié)省仿真運(yùn)行時(shí)間以及這些擴(kuò)展仿真的巨大資源需求起著非常重要的作用。

此外，由于設(shè)計(jì)要經(jīng)歷從綜合、布局和布線、簽核和工程變更單（ECO）的各個(gè)階段，因此形式驗(yàn)證必須確保電路邏輯功能不會(huì)受到任何階段的影響。

形式驗(yàn)證流程如下圖所示。

圖2.形式驗(yàn)證流程圖。

形式驗(yàn)證的步驟

在形式驗(yàn)證期間執(zhí)行以下步驟：

讀–讀取步驟讀取初始設(shè)計(jì)和目標(biāo)設(shè)計(jì)以及所有相關(guān)技術(shù)庫(kù)（圖 3）。它進(jìn)一步將設(shè)計(jì)劃分為邏輯錐的關(guān)鍵等價(jià)檢查概念和比較點(diǎn)：

常見比較點(diǎn)：輸入黑匣子;寄存器或鎖存器;主輸出

不太常見的比較點(diǎn)：多驅(qū)動(dòng)網(wǎng)絡(luò);圈;切割點(diǎn)

邏輯錐（圖4）：驅(qū)動(dòng)比較點(diǎn)的組合邏輯塊

設(shè)置 – 綜合工具提供所有自動(dòng)設(shè)置信息，包括時(shí)鐘門控和掃描插入，這些信息由形式驗(yàn)證識(shí)別。

火柴–匹配過程將首先嘗試驗(yàn)證指導(dǎo)文件并應(yīng)用已設(shè)置的任何指導(dǎo)。比賽還將嘗試根據(jù)以下內(nèi)容匹配比較點(diǎn)：

基于名稱的算法

基于簽名的分析

注意：然后報(bào)告任何不匹配的點(diǎn)。

？驗(yàn)證 – 驗(yàn)證周期驗(yàn)證參考設(shè)計(jì)的每個(gè)邏輯錐與相應(yīng)實(shí)現(xiàn)設(shè)計(jì)的邏輯等效性。形式驗(yàn)證算法使用許多求解器來(lái)證明等價(jià)或不等價(jià)。有四種可能的結(jié)果：

成功：實(shí)現(xiàn)等效于引用

失?。簩?shí)現(xiàn)不等于參考，這意味著存在邏輯差異或設(shè)置問題。

定論：沒有點(diǎn)失敗，但分析未完成，這可能是由于超時(shí)或復(fù)雜性。

未運(yùn)行：由于流中的某些初始問題，驗(yàn)證無(wú)法運(yùn)行。

調(diào)試-

檢查是否有任何警告標(biāo)志。

檢查是否有任何被拒絕的 SVF 指導(dǎo)命令。

檢查不匹配的比較點(diǎn)。

報(bào)告和修復(fù)分析

正式驗(yàn)證運(yùn)行完成后，可以生成報(bào)告分析并在必要時(shí)執(zhí)行修復(fù)。

下面的圖 5 顯示了匹配報(bào)告。這里總共報(bào)告了 30 個(gè)失敗的比較點(diǎn)，包括 4 個(gè)黑匣子引腳 （BBPins）、17 個(gè) D 觸發(fā)器 （DFF） 和 9 個(gè)鎖存器。此外，該報(bào)告指示驗(yàn)證失?。▓D 6）。

由于可能會(huì)發(fā)生從正常翻牌到多位翻牌的一些轉(zhuǎn)換，從而導(dǎo)致翻牌被報(bào)告為非等效點(diǎn)，因此 DFF 表示潛在的修復(fù)。

圖7.普通翻牌與多位翻牌。

好處

無(wú)需運(yùn)行仿真。

功能檢查可以通過在任何階段之后獲取網(wǎng)表來(lái)完成。

可以輕松識(shí)別錯(cuò)誤。

結(jié)論

本文介紹了形式驗(yàn)證流程、形式驗(yàn)證中使用的技術(shù)以及 16 nm 技術(shù)節(jié)點(diǎn)的調(diào)試。形式驗(yàn)證可以輕松檢測(cè)在時(shí)序修復(fù)、ECO 實(shí)現(xiàn)或任何后端過程中可能發(fā)生的任何錯(cuò)誤或邏輯故障。

審核編輯：郭婷