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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

基于名稱的算法

基于簽名的分析

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

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

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

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

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

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

調(diào)試-

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

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

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

報告和修復(fù)分析

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

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

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

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

好處

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

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

可以輕松識別錯誤。

結(jié)論

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

審核編輯：郭婷