EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR
For hardware designers and verification engineers, EquivFusion addresses the critical challenge of ensuring functional consistency between high-level models and low-level implementations in multi-modal design flows.
EquivFusion is an end-to-end equivalence checking tool that unifies verification across diverse hardware design abstractions (PyTorch, C/C++, Chisel, Verilog, gate-level netlists) using an MLIR-based lowering pipeline, enabling automated pairwise equivalence checking via SMT-LIB, BTOR2, and AIGER formats.
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.