The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR
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.
A copy is held
pdf, 771.3 kB. Not published — it may be under
copyright. The facts and links here are.
@misc{zhu2026equivfusion,
title = {EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR},
author = {Jiaying Zhu and Baoqi Zhang and Mengxia Tao and Kezhi Li and Hao Yan and Qiang Xu and Min Li},
year = {2026},
}