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

形式驗證是比較用硬件描述語言 （HDL） 編寫的兩個設(shè)計以確保它們在功能上等效的過程。作為功能驗證的一個子集，it 提供了在不使用仿真的情況下檢查兩個設(shè)計的功能等效性的關(guān)鍵第一步。

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

圖1.形式驗證方法的表示

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

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

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

形式驗證的類型

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

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

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

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

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

形式驗證的要求

功能等效性檢查通常需要使用相同的測試向量對兩個HDL設(shè)計進行仿真。但是，隨著ASIC技術(shù)的縮小和電路復(fù)雜性的增加，不可能使用仿真來驗證電路功能，因為仿真可能會運行數(shù)月。因此，形式化驗證通過節(jié)省仿真運行時間以及這些擴展仿真的巨大資源需求起著非常重要的作用。

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

形式驗證流程如下圖所示。

圖2.形式驗證流程圖。

形式驗證的步驟

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

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

常見比較點：輸入黑匣子;寄存器或鎖存器;主輸出

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

邏輯錐（圖4）：驅(qū)動比較點的組合邏輯塊

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

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

基于名稱的算法

基于簽名的分析

注意：然后報告任何不匹配的點。

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

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

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

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

未運行：由于流中的某些初始問題，驗證無法運行。

調(diào)試-

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

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

檢查不匹配的比較點。

報告和修復(fù)分析

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

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

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

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

好處

無需運行仿真。

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

可以輕松識別錯誤。

結(jié)論

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

審核編輯：郭婷