Ensuring functional consistency between high-level algorithmic models and low-level hardware implementations is a critical challenge, particularly as modern design flows increasingly span heterogeneous abstractions--from deep learning frameworks to hardware netlists. In this paper, we present EquivFusion, an end-to-end equivalence checking tool tailored for multi-modal circuit designs. Unlike traditional flows that rely on siloed tools or ad-hoc translation, EquivFusion leverages a verification-oriented MLIR lowering pipeline to unify diverse entry points, including PyTorch, C/C++, Chisel, Verilog, and gate-level netlists, into a common intermediate representation. This architecture enables automated, pairwise equivalence checking across diverse abstraction levels by rigorously translating designs into standard formal verification formats, i.e., SMT-LIB, BTOR2, AIGER. We demonstrate EquivFusion's feasibility to bridge the semantic gap between software specifications and hardware realizations, showcasing its effectiveness in facilitating "shift-left" formal verification for datapath-intensive hardware designs.

翻译：摘要：确保高层算法模型与低层硬件实现之间的功能一致性是一项关键挑战，尤其是在现代设计流程日益跨越异构抽象层次（从深度学习框架到硬件网表）的背景下。本文提出EquivFusion，一种面向多模态电路设计的端到端等价性检查工具。与传统依赖于孤立工具或临时性翻译的流程不同，EquivFusion利用面向验证的MLIR降级流水线，将PyTorch、C/C++、Chisel、Verilog及门级网表等多样化入口统一到公共中间表示中。该架构通过将设计严格翻译为标准形式化验证格式（即SMT-LIB、BTOR2、AIGER），实现了跨不同抽象层次的自动化配对等价性检查。我们证明了EquivFusion弥合软件规约与硬件实现之间语义鸿沟的可行性，并展示了其在促进数据路径密集型硬件设计的"左移"形式化验证方面的有效性。