一句话：提出基于 MLIR 的端到端硬件等价性检查工具，统一算法模型到门级网表并生成形式验证格式。
现代硬件设计流程跨越从深度学习框架到门级网表的异构抽象，保证高层算法模型与低层硬件实现的功能一致性十分困难，现有流程依赖孤立工具或临时翻译。EquivFusion 是面向多模态电路设计的端到端等价性检查工具，采用面向验证的 MLIR lowering 流水线，将 PyTorch、C/C++、Chisel、Verilog 和门级网表统一到公共中间表示，再转换为 SMT-LIB、BTOR2、AIGER 等标准形式验证格式，实现对不同抽象层级设计的成对等价性检查。论文展示了其弥合软件规约与硬件实现语义鸿沟的可行性，并表明其能促进面向数据通路密集型硬件设计的“shift-left”形式验证。
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 is available online1.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2604-16571,
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},
booktitle = {FSE},
year = {2026},
doi = {10.1145/3803437.3806400}
}