[2026 年 7 月 29 日提交]

查看 PDF HTML（实验性）

摘要：验证重定时后额外的顺序重合成步骤对现有工具仍具挑战性，限制了激进优化。常用等价性检查工具依赖内部重合成操作以及易出错的不同模型检查器编排，使认证变得困难甚至不可行。我们提出一种以重定时为预处理步骤并利用模拟生成可疑不变式的 IC3 技术。该技术能高效验证在重定时和任意强顺序重合成下的顺序等价问题，同时具备生成证书的附加功能。我们在经过重定时和重合成的若干公开电路设计上的结果表明，我们这一相对简单的方法大幅优于最新硬件模型检查竞赛获胜者的全部模型检查器组合（作为通用认证模型检查器的代表）。与非认证方法（如成熟的 ABC 等价性检查器）相比，我们的方法仍具竞争力，并具有额外的互补优势。

提交历史

来自：Tobias Seufert [查看邮箱]
[v1] 2026 年 7 月 29 日，UTC 22:29:27 (349 KB)