AI 中文总结
该研究针对现有工具难以验证重定时后顺序综合步骤的问题，提出基于IC3的可证明顺序扫描技术，其性能优于通用可证明模型检查器，且具备生成证明的特性，与非可证明方法相比有竞争力。
AI 中文摘要
对于现有工具而言，验证重定时后再进行额外的顺序综合步骤仍具有挑战性，这限制了激进的优化。常用的等价性检查工具依赖内部综合操作以及不同模型检查器的易错编排，这使得证明变得困难甚至不可行。我们提出一种基于IC3的技术，该技术将重定时作为预处理步骤，并利用仿真生成疑似不变量。我们的技术可高效验证重定时和任意强顺序综合下的顺序等价问题，且具有生成完整证明的附加特性。我们在一组经过重定时和综合的开源电路设计上的结果表明，我们这种相当简单的方法，作为通用可证明模型检查器的代表，其性能远超最新硬件模型检查竞赛获胜者的整套工具。与非可证明方法（如成熟的ABC等价性检查器）相比，我们仍具有竞争力，且具备额外的互补优势。
英文摘要
Verifying retiming followed by additional sequential resynthesis steps remains challenging for existing tools, limiting aggressive optimizations. Commonly-used equivalence checking tools rely on internal resynthesis operations and error-prone or- chestration of different model checkers, which makes certification difficult or even infeasible. We present an IC3-based technique that uses retiming as a preprocessing step and uses simulation to generate suspected invariants. Our technique efficiently verifies sequential equivalence problems under retiming and arbitrarily strong sequential resynthesis, and has the additional feature of producing certificates all the same. Our results on a selection of retimed and resynthesized open circuit designs show that our rather simple approach vastly outperforms the whole portfolio of the winner of the latest Hardware Model Checking Competition as a representative of general-purpose certifying model checkers. Compared to non- certifying approaches, like the mature equivalence checker of ABC, we are still competitive with additional complementary strengths.
