Formal verification of datapath circuits is challenging as they are subject to intense optimization effort in the design phase. Industrial vendors and design companies deploy equivalence checking against a golden or existing reference design to satisfy correctness concerns. State-of-the-art datapath equivalence checking tools deploy a suite of techniques, including rewriting. We propose a rewriting framework deploying bitwidth dependent rewrites based on the e-graph data structure, providing a powerful assistant to existing tools. The e-graph can generate a path of rewrites between the reference and implementation designs that can be checked by a trusted industry tool. We will demonstrate how the intermediate proofs generated by the assistant enable convergence in a state of the art tool, without which the industrial tool runs for 24 hours without making progress. The intermediate proofs automatically introduced by the assistant also reduce the total proof runtime by up to 6x.

翻译：数据通路电路的形式化验证极具挑战性，因其在设计阶段需经历深度优化。工业供应商与设计公司通过对黄金参考设计或现有参考设计进行等价性检查来满足正确性需求。当前最先进的数据通路等价性检查工具采用包括重写在内的多种技术。我们提出一种基于E-图数据结构的位宽相关性重写框架，为现有工具提供强力辅助。该E-图能够生成参考设计与实现设计之间的重写路径，该路径可被可信的工业工具验证。我们将展示该辅助工具生成的中间证明如何使某款最先进工业工具实现收敛——若无此辅助，该工业工具运行24小时仍无进展。此外，辅助工具自动引入的中间证明还可将总验证运行时间缩短至原来的1/6。