草榴社区

什麼是等效性检测？

作為形式验证(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)繁複的设计中包含許多步驟，並時常產生影響晶片整體效能的變化。如果團隊無法验证相關優化，那就表示這些步驟用途有限。此外，許多現有的等效性檢測产物需要大量的時間設定才能執行验证，因此必須減少優化以實現验证成功。當這些挑戰再加上現今高效能设计中不斷增加的運算內容，需要一個全面的、非重複性的囊括合成到签核的全方位解决方案，以滿足不斷縮短的上市時程。

幸運的是，设计團隊可以運用草榴社区 Formality?等效性檢測實現最佳 PPA 和立即可用的結果。Formality 透過部署與 草榴社区 Design Compiler? 和 草榴社区 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 還能在這個領域揭露些什麼。敬請期待！