必須優化正式驗證流程中的初始網表，因此測試設計需要額外的邏輯。在這里，我們提供16 nm節點的形式驗證流程和調試技術。

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

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

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

下表顯示了可用于比較初始設計與目標設計的組合。

表 1.初始設計與目標設計

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

形式驗證的類型

通常使用兩種形式驗證技術：

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

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

屬性檢查或基于斷言的驗證 （ABV） –屬性檢查或 ABV 檢查行為是否可行，并使用屬性檢查器工具來證明設計符合其所有規范。屬性檢查使用數學程序來證明設計的準確性。

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

形式驗證的要求

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

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

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

圖2.形式驗證流程圖。

形式驗證的步驟

在形式驗證期間執行以下步驟：

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

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

不太常見的比較點：多驅動網絡;圈;切割點

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

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

火柴–匹配過程將首先嘗試驗證指導文件并應用已設置的任何指導。比賽還將嘗試根據以下內容匹配比較點：

基于名稱的算法

基于簽名的分析

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

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

成功：實現等效于引用

失敗：實現不等于參考，這意味著存在邏輯差異或設置問題。

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

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

調試-

檢查是否有任何警告標志。

檢查是否有任何被拒絕的 SVF 指導命令。

檢查不匹配的比較點。

報告和修復分析

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

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

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

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

好處

無需運行仿真。

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

可以輕松識別錯誤。

結論

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

審核編輯：郭婷