EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914485355151360 |
|---|---|
| author | Zhu, Jiaying Zhang, Baoqi Tao, Mengxia Li, Kezhi Yan, Hao Xu, Qiang Li, Min |
| author_facet | Zhu, Jiaying Zhang, Baoqi Tao, Mengxia Li, Kezhi Yan, Hao Xu, Qiang Li, Min |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_16571 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR Zhu, Jiaying Zhang, Baoqi Tao, Mengxia Li, Kezhi Yan, Hao Xu, Qiang Li, Min Hardware Architecture Software Engineering 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. |
| title | EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR |
| topic | Hardware Architecture Software Engineering |
| url | https://arxiv.org/abs/2604.16571 |