[Submitted on 29 Jul 2026]

View PDF HTML (experimental)

Abstract:驗證時序重排後接續的循序重合成步驟，對現有工具而言仍具挑戰性，限制了積極最佳化的應用。常見的等價性檢查工具依賴內部重合成操作，以及容易出錯的各式模型檢查器編排，導致認證困難甚至不可行。我們提出一項以 IC3 為基礎的技術，將時序重排作為預處理步驟，並利用模擬產生候選不變量。此技術能有效驗證在時序重排與任意強度循序重合成條件下的循序等價問題，並具備同時產生認證書的附加功能。我們在多組經過時序重排與重合成的開源電路設計上的實驗結果顯示，我們相對簡單的方法大幅超越最近一屆硬體模型檢查競賽冠軍（作為通用認證模型檢查器的代表）的整個組合。與非認證方法相比，例如成熟的 ABC 等價檢查器，我們仍具競爭力，並具備額外的互補優勢。

Submission history

From: Tobias Seufert [view email]
[v1] Wed, 29 Jul 2026 22:29:27 UTC (349 KB)