EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR

TL;DR

EquivFusion is a unified MLIR-based tool that enables automated equivalence checking across various hardware and software design abstractions, improving formal verification workflows.

Contribution

It introduces a verification-oriented MLIR lowering pipeline that unifies diverse design representations for automated equivalence checking.

Findings

Successfully bridges the semantic gap between software models and hardware implementations.

Enables pairwise equivalence checking across multiple abstraction levels.

Facilitates shift-left formal verification for complex hardware designs.

Abstract

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.