等價性檢查 (Logic Equivalence Checking, LEC)

1. 3 秒看懂

LEC 是數字晶片設計的**“邏輯保鏢”。其核心任務是用數學方法，100%確保你的RTL程式碼與經過綜合、版面配置佈線後的門級網表在功能上完全一致**，杜絕任何非預期的邏輯改動。它是晶片流片前最後一道、也是強制性的一道邏輯“安檢”。

2. 3 分鐘產業解釋

一枚晶片從設計到製造，其邏輯表達會被“翻譯”多次（RTL → 門級網表 → 物理版圖）。每一次翻譯，都可能因工具最佳化、人為工程變更（ECO）或設計疏忽，引入微小的邏輯偏差。LEC 就是專門抓這種“翻譯錯誤”的警察。

• 位置：LEC 工作在邏輯綜合（RTL→網表）和物理設計（網表→版圖）的各個階段之後。它是邏輯籤核的核心環節，是“設計凍結”前的最後確認。
• 價值：它避免了流片後因邏輯錯誤導致的天價損失。據 IBS 2023 年資料，一次 5nm 晶片的流片（Mask）成本高達 1，750 萬—2，500 萬美元，一次致命邏輯錯誤足以摧毀一箇中等規模專案。沒有 LEC，就像在懸崖邊駕駛沒有安全帶的賽車。
• 現狀與剛性：隨著 AI 晶片、高效能運算（HPC）晶片設計複雜度爆炸（整合數十億至上百億電晶體）、ECO 變得極其頻繁，LEC 已從“可選項”變為所有先進數字晶片專案的必備流程和設計收斂的絕對基石。

3. 技術原理

LEC 本質上是形式驗證的一個子領域，其核心使命是解決一個數學問題：給定兩個組合或時序邏輯網路（參考設計 R 與實現設計 I），判定它們對所有可能的輸入序列是否產生完全相同的輸出。

• 數學基礎：現代 LEC 引擎主要基於兩大基礎理論：布林可滿足性（SAT）和二元判定圖（BDD）。工具會將兩個設計中對應邏輯錐的輸出進行異或（R XOR I），構成一個“等價性判定電路”。核心目標變為：證明該 XOR 電路的所有輸出，在任何輸入下都恆為 0（即永遠找不到一個反例使 R 和 I 輸出不同）。
• 狀態空間爆炸與對策：一個含有 n 個暫存器的時序設計，其理論上的狀態空間高達 2^n。直接窮舉在物理上不可能。因此，現代工具採用分而治之策略，將大規模設計遞迴切割為百萬級的小型邏輯錐體，然後分別、並行地加以證明。

3.1 核心引擎與演算法

• 比較點識別與匹配：工具首先在兩個網表中，通過拓撲分析、名稱匹配和功能特徵等方法，自動識別出成對的“比較點”（如輸入/輸出埠、暫存器的 D/Q 端、鎖存器、黑盒例項邊界），這是後續一切操作的前提。
• 等價性判定引擎：
  • 結構雜湊：第一道快速篩選，通過計算邏輯結構的雜湊值，迅速找出完全同構、顯然等價的部分節點。
  • 基於 BDD 的方法：將邏輯函式表示為規範化的、唯一形態的 BDD 圖。若兩個節點的 BDD 圖同構，則它們完全等價。優點是完備且對資料路徑（如 ALU）高效；缺點是記憶體消耗大，面對複雜控制邏輯時可能出現“BDD 爆炸”。
  • 基於 SAT 的方法：將“存在一個輸入使兩個設計輸出不同”這一命題，轉化為一個 SAT 問題。強大的 SAT 求解器若找到解，則輸出反例波形；若窮盡求解空間無解，則證明等價。優點是記憶體效率高，擅長控制邏輯和不等價定位；缺點是在證明大規模電路等價的絕對性時可能耗時極長。
  • 混合引擎（業界主流）：Synopsys Formality、Cadence Conformal 及 Siemens EDA FormalPro 均採用BDD 與 SAT 混合的動態排程引擎。工具會根據邏輯錐的結構特徵（如資料通路、控制邏輯、仲裁器等）自動選擇或組合最優策略，以在證明能力和計算資源間取得平衡。
• 分割槽與約簡：一個平鋪直敘的億門級網表無法直接處理。工具利用多種演算法（如使用邊界假設性化簡、利用已證明的等價點替代）持續逐級約簡問題規模，形成分層遞進的證明鏈。

3.2 時序等價性的深度處理

對於複雜的時序設計（如流水線、狀態機），工具不能僅比較組合邏輯雲端，還必須處理狀態對映問題。它通過比對兩個設計中所有暫存器的次態邏輯（next-state function），在假定二者從相同初始狀態啟動後，證明每一拍的狀態轉移在所有合法輸入下都保持一致。這一過程要求工具對暫存器重定時（retiming）、流水級重排、狀態重編碼等常見最佳化具備魯棒的模型支撐。

4. 關鍵引數

評估一款商業 LEC 工具或一個 LEC 流程的實戰能力，可聚焦以下維度：

1. 證明完備性與覆蓋率：能否實現 >99.5% 的全自動等價性證明（Proof），而無需人工干預設定複雜約束。這是衡量工具魯棒性的第一指標。
2. Turnaround Time（TAT）與記憶體效率：在給定算力（如 64 核、512GB 記憶體伺服器）下，完成一次對 5 億門級設計、數千個 ECO 點的完整 LEC 執行所需的時間和峰值記憶體。據 SNPS 2024 年使用者調查，頭部客戶對全晶片 LEC 的 TAT 容忍度已壓縮至 8 小時以內。
3. 除錯效率與根因定位精度：一旦發現不等價（Failing），工具能否輸出最少的反例（最小化波形）、並精準定位到第一個出錯的根節點（root cause cone）及其涉及的邏輯變更，是決定物理設計團隊修復週期（往往以小時計）的關鍵。
4. ECO 自動化與適應性：對物理設計階段高頻出現的 ECO（如備線邏輯插入、時鐘門控單元替換），工具能否無需更新 SDC 約束即可自適應，並提供 ECO 前後的等價性“增量證明”而非全量重跑。
5. 誤報控制：要求無誤報。任何一次被報告為不等價的案例，都必須是真實存在的不等價。一次誤報會嚴重損害工程團隊的信任，導致對工具本身產生懷疑。

5. 技術路線

技術/引擎	核心原理	優點	侷限與痛點	典型適用場景
純 BDD 引擎	將邏輯函式規範化表示為有向無環圖（BDD），通過圖同構判定等價	完備性強，一旦建立 BDD，等價性證明即為常數複雜度；對結構化資料通路效率極高	在遇到乘法器、複雜仲裁器等模組時，BDD 尺寸可能隨變數數指數級爆炸，記憶體瞬間耗盡	以加法器、多路選擇器為主的運算單元
純 SAT 引擎	將“不等價存在性”命題編譯為合取範式（CNF），交由 SAT 求解器找尋反例或證明不可滿足	記憶體控制優秀；發現不等價時反例質量高，極擅長處理控制邏輯和“找 Bug”	在證明大規模電路等價時，需窮盡搜尋空間，若無反例，可能在無法完成證明的超時邊緣徘徊	複雜控制邏輯、狀態機、Bug 搜尋
混合引擎（絕對主流）	在統一平台上動態建置 BDD 和 SAT 求解器，根據邏輯錐特徵進行分派、協同	平衡了 BDD 的證明效率與 SAT 的空間效率，魯棒性高，適合全晶片全自動流程	演算法開發門檻極高，需要頂級工程團隊數十年的持續最佳化	目前所有 7nm 以下商用晶片流片的標準流程

6. 上游

LEC 工具的精準執行高度依賴其上游輸入的質量和完整性：

• 設計輸入：RTL 原始碼（SystemVerilog/VHDL）、邏輯綜合後及物理設計後（含版面配置佈線、時鐘樹綜合、ECO 後的完整修改）的門級網表（通常為 Verilog 或 DEF/LEF 提取的檔案）。Synopsys 流程中，一般以 DC/FC 綜合後的網表為“黃金參考”。
• 工藝與單元庫：晶圓廠認證的標準單元庫、I/O 庫、儲存器/模擬 IP 的功能模擬模型（.v 或 .lib）及抽象化模型（.lef）。模型的任何時序或功能錯誤，可能導致 LEC 返回誤導性的不等價。
• 設計約束檔案：SDC（Synopsys Design Constraints）檔案中的時序例外（如多週期路徑、偽路徑）和模式設定（如測試模式、功能模式）定義，工具需要據此遮蔽無效的查詢空間。

7. 下游

LEC 的結果直接決定了專案能否進入下一階段：

• 邏輯籤核：LEC 通過（所有比較點被證明為 Verified 或無影響的 Unmatched）是設計部門完成“邏輯凍結”的最終交付物之一。沒有籤核過的 LEC 報告，無法進入後續時序和物理籤核。
• 流片（Tape-out）：提供給代工廠（如 TSMC, Samsung, Intel）的最終 GDSII 版圖資料，必須是經過 LEC 驗證合格的邏輯網表的物理實現。這是晶片從虛擬進入物理世界的最終信任憑據。
• ECO 閉環流程：在物理設計的後期，每一次為了修復時序、功耗或 DRC 違規而手動或工具自動進行的 ECO，都強制觸發一次增量 LEC。它構成了一個 “修改—> 提取網表 —> LEC 驗證 —> 通過/駁回” 的嚴格閉環，是專案後期最高頻的活動之一。

8. 受益公司

LEC 是整個數字半導體產業鏈的剛性必需品，其核心受益方分為三大類：

第一梯隊：全球 EDA 三巨頭（直接業務驅動）

• Synopsys (SNPS, US)：擁有 Formality 這一標杆性 LEC 工具，與其 Design Compiler 綜合工具、PrimeTime 時序分析工具深度耦合，形成從設計到籤核的“全家桶”生態，切換成本極高。
• Cadence (CDNS, US)：Conformal Equivalence Checker 以低誤報率和強大的除錯能力著稱，並與其 Innovus 物理設計系統、Tempus 時序籤核工具緊密整合，在 IDM 端和大型 Fabless 中份額穩固。
• Siemens EDA：FormalPro（原 Mentor Graphics FormalPro）在低功耗設計（如 UPF 驗證）、可測試性設計（DFT）插入後的等價性檢查等細分領域有獨特競爭力，是西門子工業軟體數字化戰略的關鍵拼圖。

第二梯隊：國內外技術提供商（替代與補充機會）

• 國內領先的 EDA 初創公司及上市公司（如華大九天、國微芯、芯華章等），在“國產替代”與供應鏈安全兩大驅動力下，已將包括 LEC 在內的形式驗證工具作為核心攻關方向。部分已釋出的 LEC 產品在特定應用場景（如 FPGA 驗證、中低工藝節點 SoC）開始獲得客戶匯入。公開資料未見全球市場份額具體數字，但增長趨勢明確。

第三梯隊：LEC 重度應用方（生產力獲益方）

• 包括所有先進數字晶片設計公司：輝達（NVIDIA）、超威（AMD）、Apple（Apple）、高通（Qualcomm）、聯發科（MediaTek） 以及國內的 海思、燧原科技、摩爾線程 等。它們每年向 EDA 廠商支付數千萬至上億美元不等的訂閱費，LEC 是其中絕對必需的核心模組，直接關乎其數十億美元營收產品的成敗。

9. 市場規模

• 細分市場定位：LEC 是 EDA 行業中“功能驗證”大類下的“形式驗證”子領域的核心組成部分。據 SIA 與 SEMI 的 2023 年資料，全球 EDA 市場總規模約 145 億美元，其中功能驗證市場約佔 30%（~43.5 億美元）。形式驗證（含 LEC、模型檢查等）在其中約佔 20%—25%，對應 2023 年全球市場規模預估約 8.7—10.9 億美元。
• 增長驅動力與量化預測：
  1. 設計數量與複雜度：Gartner 預測，全球晶片設計團隊啟動的新專案數年均複合增長約 8-10%，而單個設計的平均門數（複雜度）每 2—3 年翻一番。
  2. 先進節點滲透率：TSMC 財報顯示，2023 年其 7nm 及以下先進製程營收佔比已達 58%。先進節點對 LEC 的需求幾近剛性。預計到 2028 年，形式驗證市場的年複合增長率（CAGR）將達 10—12%，規模有望接近 16—18 億美元。
• 審慎宣告：以上為基於行業公開報告（SEMI, Gartner， 2023）的交叉估算，精確數值受各機構對形式驗證邊界定義影響，可能存在統計口徑差異。

10. 玩家對比

維度	Synopsys Formality	Cadence Conformal	Siemens EDA FormalPro
市場地位	市場領導者，全流程繫結性強，份額預估 > 50% (公開資料未見精確資料)	強勁的挑戰者，在大型 Fabless 與 IDM 中深獲認可，份額 ~30-35%	特色玩家，在特定流程中地位穩固，份額 ~10-15%
核心優勢與整合性	與 DC、ICC2/FC 的同源資料模型共享，ECO 流程最平滑，生態閉環堅固	低誤報率與 BDD/SAT 混合引擎效率備受除錯工程師推崇；與 Innovus 系統協同佳	在 UPF 低功耗驗證、DFT 網表等價性檢查方面有精準獨特的模型支援
證明能力與自動化	對億門級設計的全自動證明率行業領先，手冊干預少	複雜狀態機對映、重定時最佳化後的證明魯棒性強	處理大量異質 IP 拼接設計時，自動匹配與偵錯有獨到之處
商業模式	訂閱制（通常三至五年長約），與大版本更新捆綁	靈活的 Token 計費或多年訂閱，常與驗證全家桶打包	隨 Siemens PAE 整體解決方案銷售，在西門子工業軟體大客戶中滲透率高
國產化狀態	已無法為國內特定實體提供最新版本服務	部分受限	風險較低，但生態相對封閉

11. 風險

• 技術鎖定與供應鏈中斷風險（★★★★★）：產業生態被Synopsys Formality + Design Compiler的閉環深度鎖定。地緣政治因素可能導致某些具有決定性技術迭代的版本無法獲取，對國內先進製程設計造成“卡脖子”風險，迫使向效率可能較低的代替方案或舊版本遷移。
• 證明能力不足風險（★★★）：面對 3nm 以下工藝、數百億電晶體、含大量自研最佳化算術單元的設計，存在工具無法在合理時間（如一夜間）完成證明的機率。這可能導致專案進度被迫延期，或不得不投入大量高階工程師編寫複雜約束以“引導”工具。
• 假陽性（False Negative）導致進度延遲（★★）：儘管機率極低，但引擎 Bug 或庫模型錯誤可能導致誤報不等價。這迫使工程師花費寶貴時間去除錯一個本不存在的“幽靈”問題，直接侵蝕專案後期本已壓縮到極致的時間表。
• 人才斷層風險（★★★）：熟練操作 LEC 工具並能精準分析失敗根因的工程師培養週期長（至少 1-2 年）。國內半導體產業爆發式增長導致此類人才供給極度短缺，高流動性會直接拉低專案執行效率。

12. 誤讀糾偏

• 誤讀一：“有了高覆蓋率的動態模擬，就不需要 LEC 了。” 糾偏：這是一個根本性認知錯誤。動態模擬（如 UVM 環境）是抽樣檢查，其覆蓋率取決於編寫的測試向量，理論上永遠無法窮盡所有狀態組合。LEC 是窮舉數學證明，對所有合法的輸入組合給出 100% 的斷言。二者是互補關係，而非替代。在所有現代化、追求“首次即成功”的流片流程中，LEC 籤核是解除邏輯風險的唯一強制手段。

• 誤讀二：“LEC 會顯著拖慢設計週期。” 糾偏：恰好相反，LEC 是加速設計收斂的利器。它通過在設計後期（尤其是凍結前頻繁的 ECO 階段）以高度自動化、分鐘至小時級的執行速度快速識別邏輯錯誤，避免了將問題帶入更慢的時序籤核迴圈，甚至流片後才暴露，從而造成數週乃至數月的災難性延誤。前期的 LEC 計算資源投入，是為了規避後期指數級的成本與時間代價。

• 誤讀三：“LEC 只能檢查組合邏輯雲端。” 糾偏：這是對現代 LEC 的巨大誤解。解決時序邏輯等價性是商用工具的核心價值所在。它通過自動推導並演算法匹配兩個設計中成千上萬個暫存器的狀態轉移關係，來證明有限狀態機、流水線、帶握手的介面邏輯的整體功能完全等價。

• 誤讀四：“工具報告‘Unmatched’，就是設計不等價。” 糾偏：非也。LEC 報告的比較點中，“Verified”意味著已證明等價；“Failing”意味著已證明不等價；而“Unmatched”僅表示工具因缺乏足夠的名字、結構或功能資訊而無法自動建立對應關係。這通常需要工程師介入，通過新增展望約束來協助工具完成匹配，它本身並不等同於功能錯誤。

13. 最新事件

2024-2025 年關鍵動態更新：

• 終端需求爆炸推動工具革新：為應對 NVIDIA H200/B200、AMD MI300 系列等 AI 訓練/推論晶片的超大規模（超 1500 億電晶體）和 Chiplet 架構，Synopsys 在 2024 年 SNUG 全球使用者大會上釋出了 Formality 的下一代層級化與並行證明架構，旨在處理由多個 3D 堆疊裸片構成的系統的跨 die 等價性。
• 國產替代實質性突破：據公開報道，2024 年國內頭部 EDA 公司已完成其 LEC 工具在數家領先 Fabless 的 7nm/14nm AI SoC 和 5G 基帶晶片專案中的全流程驗證試點，並開始與部分代工廠的參考流程進行互認證測試。這是國產形式驗證工具走向主流的關鍵節點。
• AI 技術反向賦能 EDA：Cadence 在 2023 年底推出的 Verisium AI 平台，宣佈了一項關鍵能力——使用 AI 模型輔助引導 Conformal LEC 的“除錯根因分析”，聲稱能將不等價點的根因定位速度平均提升 4-5 倍，這預示著 AI 正在開始解決 LEC 長期以來的最大人力瓶頸。

注：以上資訊均源自公開的產業新聞及公司官方釋出（Synopsys Press Release, Cadence Blog， 2024; 國內券商半導體研究報告， 2024），不構成任何投資建議。

14. 追蹤指標

追蹤 LEC 行業景氣度與企業價值，可長期觀察以下量化指標：

1. EDA 巨頭財報之“功能驗證”營收增速：監控 Synopsys 在其 Verification 細分業務、Cadence 在其 Functional Verification 板塊（含形式驗證）的季度年增率/季增率營收增長率。此指標是形式驗證市場最直接的溫度計。
2. 全球最先進量產晶片的電晶體整合度：追蹤 NVIDIA、AMD、Intel、Apple 最新旗艦晶片的電晶體數量，其指數級增長是 LEC 需求的最底層、最剛性的驅動力。
3. TSMC、Samsung 先進製程（≤7nm）的季度營收佔比：此佔比的提升，意味著正片晶圓越來越多地來自必須使用 LEC 的先進設計，與 LEC 市場規模呈強正相關。
4. 國內獲 EDA 招標的政企專案數量與金額：通過中國政府採購網、各省工信廳公示，追蹤含有“形式驗證”、“等價性檢查”關鍵詞的國產化 EDA 採購標的規模，是衡量國產替代節奏的先行指標。
5. 頭部公司的設計 ECO 頻次（觀察性指標）：通過行業會議（如 CDNLive, SNUG）的案例演講，可非正式追蹤大型設計專案中流片前 ECO 的平均次數。次數的增加意味著 LEC 在專案中被呼叫的強度更高。

15. 信源

本報告基於截至 2025 年 5 月的公開資訊編撰，關鍵信源包括：

• 官方技術文件與出版物：Synopsys Formality、Cadence Conformal、Siemens EDA FormalPro 各自的產品資料手冊、白皮書及使用者指南。
• 行業權威報告：SEMI《全球半導體裝置市場報告》（2023）；Gartner《Market Share Analysis: EDA Software, Worldwide》（2023）。
• 學術與產業前沿會議：IEEE/ACM 的 DAC（設計自動化會議）、ICCAD（國際計算機輔助設計會議）中關於形式驗證、SAT 求解演算法的歷年論文集。
• 企業財報與投資者關係：Synopsys、Cadence、西門子歷次季度財報及電話會議紀要；國內相關上市 EDA 公司的定期報告與投資者活動記錄表。
• 行業分析與智庫：IBS（International Business Strategies）年度流片成本模型（2023 版）；國內頭部券商研究部關於 EDA 國產化的專題研究報告（2023-2024）。