何必犧牲QoR？優化設計簽核，以更智能的方法實現精確功能性 ECO

什麼是等效性檢測？

作為形式驗證(formal verification)廣泛專業的一部分，等效性檢測用不同數學建模(mathematical modeling)技術來推斷兩個設計型式的行為是否相同。這包含三項基本步驟：設定(setup)、映射(mapping)和比較(comparing)。

在這個過程的第一階段，先輸入經驗證的參考設計、元件庫(library elements)和修改後的設計，並建立資料結構以啟動後續步驟。在映射階段，通常使用邏輯錐(logic cones)或組合邏輯電路區塊驅動暫存器、主要輸出連接埠和黑箱(black-box)輸入引腳等的比較點，來映射和比較不同的設計。最後，在比較階段將仔細檢測比較點，確認每個設計型式是否呈現相同行為，或是偵測到任何錯誤，在後者情況下則需要在設計中解決錯誤並重新執行此流程。

什麼是功能性 ECO？

功能性 ECO 是在閘級網表(gate-level netlist)中直接插入邏輯的流程，相當於在RTL層級進行更改。進行此修改是為了修正在 RTL 設計版本中發現的錯誤、優化設計，或是根據客戶要求修改設計。合成後的版本將直接修補於設計中，而非重新實作設計，避免額外的成本和時間。

有鑑於可能需要的變更性質各不相同，處理 ECO 可能是一個壓力大、工作時間長且充滿不確定性的過程。ECO 往往只出現在設計週期後期，且通常具有高度的複雜性，並可能影響狀態機(state machine)、時鐘重設路徑等。電子設計自動化(EDA)工具可節省時間、減少合成(synthesis)等繁瑣任務，只專注在受 ECO 影響的部分，並驗證 RTL 和修補邏輯閘層級實作的等效性。從 ECO RTL 就緒到 ECO 完成的過程，現今產業中的自動化解決方案面臨數個限制，從而影響處理時間(TAT)、多次 人工返工(iteration)以及降低結果品質(QoR)。

等效性檢測如何應對驗證挑戰？

晶片設計人員仰賴各種不同的優化解決方案和技術來提供差異化產品，並滿足 PPA 目標，包含重定時(retiming)和多位元暫存器(multibit banking)到先進資料運算優化等。這些優化範疇使設計人員能夠透過一系列優勢實現更好的 QoR，但這仍然存在問題：它們也會提高驗證難度(當兩個設計型式差異很高時)，最終會為傳統等效性檢測技術帶來壓力。

系統單晶片(SoC)繁複的設計中包含許多步驟，並時常產生影響晶片整體效能的變化。如果團隊無法驗證相關優化，那就表示這些步驟用途有限。此外，許多現有的等效性檢測產品需要大量的時間設定才能執行驗證，因此必須減少優化以實現驗證成功。當這些挑戰再加上現今高效能設計中不斷增加的運算內容，需要一個全面的、非重複性的囊括合成到簽核的全方位解決方案，以滿足不斷縮短的上市時程。

幸運的是，設計團隊可以運用Synopsys Formality®等效性檢測實現最佳 PPA 和立即可用的結果。Formality 透過部署與 Synopsys Design Compiler® 和 Synopsys Fusion Compiler™ 密切合作的引導式驗證流程來克服 QoR 障礙，以深入了解設定實作和正在執行的優化類型。透過獨特的內建以機器學習(ML)驅動的適應性分散式驗證方法，團隊可以在最少的干預下，實現快速、準確和完整的驗證。

引導式設定

對於任何簽核(signoff)解決方案而言，重要的不只是完全驗證所有優化以獲得最佳 QoR，而且還要評估設計人員簽核的速度。引導式方法讓用戶得以充分利用新思科技 Design Compiler、Fusion Compiler 和IC Compiler™ II 的進階優化功能，同時確保可靠完成度和快速設定。

這個過程類似這樣：演算法優化方案(recipe)在執行階段被記錄為「指引(guidance)」(由新思科技 Design Compiler 或 Fusion Compiler 生成)，用於快速設定驗證環境並避免多次執行反覆運算。然後將此資訊與 RTL 和對應的網表一起讀入 Formality 解決方案。在下一階段，指引將被獨立處理和預先驗證。最後，新思科技 Formality 套用指引來簡化最終驗證步驟。透過在比對和驗證期間使用最高效率的演算法，此種按照建構逐步校正(correct-by-construction)的資訊不僅改進效能，更能實現一次就通過(first-pass)的結果。

藉由以ML驅動的等效性檢測簡化晶片設計簽核

Formality 解算器(solver)技術歷經多年發展後，已可驗證最複雜的高效能設計。新思科技 Formality解決方案透過分散式處理(DPX)方法可同步運用一系列解算器，特別針對資料路徑進行驗證，使驗證更快速並解決驗證困難。透過「更智能」的適應性分散式驗證，該解決方案提供一套全方位替代策略，以適應性部署取代單獨部署，讓團隊即使在最具挑戰的設計上執行驗證時，亦能提升高達 5 倍的執行時間效率。集結自動設定、頂級解算器技術和分散式功能的獨特組合，讓新思科技 Formality 解決方案能夠在市場上實現最佳的可驗證 QoR。

解決功能性 ECO 的新方法

等效性檢測對於偵測SoC 設計過程中的各種錯誤至關重要，而功能性 ECO 為設計提供了關鍵的後期優化步驟。由於這些變更在設計週期後期才導入，因此團隊適時進行驗證和優化這些變更的機會微乎其微。客戶經常需要為多個設計進行多項ECO，這使得處理時間(TAT) 成為ECO 工具的關鍵衡量指標。如今，業界許多現有的工具給人一種錯誤的印象，即需要完整的 ECO RTL 綜合才能開始自動化 ECO 流程。而新思科技 Formality ECO 針對這項 要求進行了變革。

透過在 ECO RTL 準備就緒後就開始ECO 生成程序，新思科技 Formality ECO 提供了自動化功能性 ECO 以及利用新思科技 Design Compiler 和新思科技 Fusion Compiler 現有功能的全新方法，在設計後期的 ECO節省寶貴時間。新思科技 Formality ECO使用針對性合成 (targeted synthesis)技術，並著重在原始 RTL 和 ECO RTL 之間的變更區域；並利用 Formality 等效性檢測引擎，在滿足時序要求的限制下建立極小的ECO修補—而這些都不會影響到ECO修補的 QoR。

隨著對完全驗證和QoR 的期望不斷提升，新思科技的研發團隊持續試驗不同的設計特性和訓練模型，從而不斷推動新思科技 Formality 等效性檢測和Formality ECO 功能演進。透過新思科技 Formality 解決方案，團隊再也不需要每次都重頭開始進行驗證並縮減優化程序，以致於犧牲 QoR。

展望未來

想像一下，如果晶片設計驗證可以立即完成，無需多次除錯設定(iterations)和反覆重頭開始驗證。再想像有一個分散式系統，它可以配合所需工作量調用多個計算程序，得減少每次需要進行更改時，花費在重複流程的數週單調工作時間。

我們目前還在揭櫫新思科技 Formality 真正潛力的浪尖上。在不依賴人為干預的情況下，將可預測性和自動化應用於晶片設計過程，已有顯著成功的數據。透過學習型方法縮短等效性檢測週期並實現一次到位(first-time-right)的 ECO，為設計團隊創造了一系列優勢—無論設計多麼複雜，都能實現最佳的可驗證 QoR。

如果我們已經能夠透過精準的結果實現這種可能性，那麼試想一下，一旦我們開始進行特定的客戶資料學習訓練，ML 還能在這個領域揭露些什麼。敬請期待！