電子設計自動化 (EDA)
系統
矽智財 (Silicon IP)
SolvNetPlus
教育與訓練課程
定義
等效性檢查 是稱為「形式驗證」這一更廣泛學科的一部分。這項技術運用數學建模技術，用以證明設計的兩種表示形式具有相同的行为。此方法不應與「功能驗證 」混淆，後者是透過窮舉模擬來驗證設計的正確性。
一旦確定了設計的已驗證版本，即可利用「等效性檢查 」來判斷該設計的另一種表示形式是否與已驗證版本具有相同行為。此技術不使用輸入向量，因此效率更高。
等效性檢查 這有助於驗證在進行合成等操作之後，或 功能性工程變更指令 (ECO) 已套用之後，是否仍維持不變。
等效性檢查 是如何運作的？
等效性檢查 共有三個基本步驟：
- 設定
- 製圖
- 比較
設定階段的輸入包含已驗證的參考設計、函式庫元件以及修訂後的設計。在此步驟中，系統會讀取這些輸入，並建立資料結構以利後續步驟的進行。
在「映射」階段，會將設計的關鍵點進行映射並進行比較。通常會使用邏輯錐來組織比較點。邏輯錐是一種組合邏輯模組，用於驅動比較點。邏輯錐的輸入包含寄存器輸出腳位、主要輸入埠以及黑盒輸出腳位。比較點則包含寄存器、主要輸出埠以及黑盒輸入腳位。
在「比對」過程中，系統會檢視已映射的關鍵點，以判定其屬於「等效」、「非等效」或「反轉等效」。若設計中某些部分的比對結果無法明確判定，可投入更多資源重新執行比對，以解決此問題。
下圖說明了此流程：
Why Equivalence Checking is Important?
在任何典型的複雜 SoC 設計中，設計流程中都有許多工具會對設計進行各種操作。除了邏輯合成之外，還有功耗最佳化 步驟、可測試性插入以及功能性工程變更（ECO），用以處理設計問題或因應設計變更。
所有這些步驟都可能對設計行為造成細微的改變，而這些改變可能在模擬過程中被忽略，因為模擬的完整性取決於驅動它的測試平台。由於「等效性檢查 」基於無向量形式證明方法，這項技術能夠偵測到在此過程中產生的各種錯誤。這顯著提升了對最終結果的信心。
等效性檢查 的優點有哪些？
等效性檢查 為任何設計流程提供了強大的輔助工具。透過形式化方法驗證設計的一致性，能深入了解設計結果的品質，且此品質評估不取決於測試平台是否完備。具體優勢包括：
- 效率更高。較少依賴速度較慢的閘極層級模擬。
- 信心更強。較少擔心工具鏈或工程變更指令（ECOs）會引入細微的錯誤。
- 品質更佳。此技術可凸顯設計中不當的 RTL 編碼。
- 預測性更高。漏檢錯誤的機率更低。
邏輯等效性檢查 與 Sequence 的比較等效性檢查
邏輯等價性檢查（等效性檢查 ，LEC）會檢視設計的組合邏輯結構，以判斷兩種替代實現方案的結構是否會展現相同的行为。若對設計施加重新定時等操作，則該設計的結構將不再能在兩種表示法之間建立對應關係。
序列等效性檢查（SEC）會將時序因素納入考量，並在多個時鐘週期內檢視兩個設計表示形式的等效性。
等效性檢查 以及 新思科技
新思科技 提供 Formality 等效性檢查 該方法採用形式化與靜態分析技術，用以判定某項設計的兩個版本在功能上是否等價。
新思科技 此外還提供 VC Formal，這項解決方案包含一套全面的形式驗證應用程式（Apps），涵蓋屬性驗證（FPV）、自動提取屬性（AEP）、覆蓋率分析器（FCA）、連通性檢查（CC）、 序列等效性檢查 （SEQ）、寄存器驗證（FRV）、X 傳播驗證（FXP）、測試台分析器（FTA）、回歸模式加速器（RMA）、資料路徑驗證（DPV）、功能安全（FuSa），以及用於驗證標準匯流排協定的斷言 IP（AIP）產品組合。
最後， 新思科技 提供ESP，這是一款基於符號模擬的客製化設計形式驗證工具（等效性檢查 ）。ESP 是一款形式驗證工具（等效性檢查 ），常用於對客製化設計（例如嵌入式記憶體 、客製化巨集、標準單元及 I/O 單元庫）進行完整形式驗證（功能驗證 ）。其用途在於確保兩種設計表示形式在功能上等價。這些設計可呈現為 Verilog 行為模型、RTL、閘極、開關、SPICE 或 .db 網表視圖。
繼續閱讀
