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

• URL: http://arxiv.org/abs/2604.16571v1
• Date: Fri, 17 Apr 2026 12:09:54 GMT
• Title: EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR
• Abstract summary: EquivFusion is an end-to-end equivalence checking tool tailored for multi-modal circuit designs.<n>It unifies diverse entry points, including PyTorch, C/C++, Chisel, Verilog, and gate-level netlists, into a common intermediate representation.
• Score: 14.681439854488765
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs [5.82728420508304]
  This paper investigates sequential circuits as an intermediate representation for software verification.<n>We present Circuit-Based Program Verification (CPV), a modular framework that translates C programs into sequential circuits.
  arXiv  Detail & Related papers  (2026-08-07T16:41:07Z)
• FLARE: Diffusion for Hybrid Language Model [72.60770374799634]
  FLARE is a systematic conversion framework for hybrid-attention large language models.<n>It combines a token-equal AR-and-diffusion objective, hardware-aware kernels, and unified inference, enabling one checkpoint to support both AR-style verified decoding and diffusion-style parallel denoising.<n>Our results suggest practical dLLMs are limited not only by decoding algorithms, but also by transfer data quality and the training inefficiency of current block-diffusion objectives.
  arXiv  Detail & Related papers  (2026-06-01T06:58:15Z)
• VeriGraphi: A Multi-Agent Framework of Hierarchical RTL Generation for Large Hardware Designs [5.354071922171165]
  We present VeriGraphi, a framework that introduces a spec-anchored Knowledge Graph as the architectural substrate driving the RTL generation pipeline.<n>We show that VeriGraphi enables reliable hierarchical RTL generation with minimal human intervention for RISC-V.
  arXiv  Detail & Related papers  (2026-04-16T02:30:57Z)
• UniDial-EvalKit: A Unified Toolkit for Evaluating Multi-Faceted Conversational Abilities [70.79422099851506]
  We present UniDial-EvalKit (UDE), a unified evaluation toolkit for assessing interactive AI systems.<n>UDE standardizes heterogeneous data formats into a universal schema, streamlines complex evaluation pipelines through a modular architecture, and aligns metric calculations under a consistent scoring interface.
  arXiv  Detail & Related papers  (2026-03-24T13:01:31Z)
• Beyond Pixels: Vector-to-Graph Transformation for Reliable Schematic Auditing [34.54168175788343]
  We propose a Vector-to-Graph (V2G) pipeline that converts CAD diagrams into property graphs where nodes represent components and edges encode connectivity.<n>On a diagnostic benchmark of electrical compliance checks, V2G yields large accuracy gains across all error categories, while leading MLLMs remain near chance level.
  arXiv  Detail & Related papers  (2026-02-12T07:50:49Z)
• Plain Transformers are Surprisingly Powerful Link Predictors [57.01966734467712]
  Link prediction is a core challenge in graph machine learning, demanding models that capture rich and complex topological dependencies.<n>While Graph Neural Networks (GNNs) are the standard solution, state-of-the-art pipelines often rely on explicit structurals or memory-intensive node embeddings.<n>We present PENCIL, an encoder-only plain Transformer that replaces hand-crafted priors with attention over sampled local subgraphs.
  arXiv  Detail & Related papers  (2026-02-02T02:45:52Z)
• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  silicon-grade correctness remains bottlenecked by: (i) limited test coverage and reliability of simulation-centric evaluation, (ii) regressions and repair hallucinations, and (iii) semantic drift as intent is reinterpreted across agent handoffs.<n>We propose Veri-Sure, a multi-agent framework that establishes a design contract to align agents' intent and uses a patching mechanism guided by static dependency slicing to perform precise, localized repairs.
  arXiv  Detail & Related papers  (2026-01-27T16:10:23Z)
• VSA:Visual-Structural Alignment for UI-to-Code [29.15071743239679]
  We propose bfVSA (VSA), a multi-stage paradigm designed to synthesize organized assets through visual-text alignment.<n>Our framework yields a substantial improvement in code modularity and architectural consistency over state-of-the-art benchmarks.
  arXiv  Detail & Related papers  (2025-12-23T03:55:45Z)
• Towards Unified Semantic and Controllable Image Fusion: A Diffusion Transformer Approach [99.80480649258557]
  DiTFuse is an instruction-driven framework that performs semantics-aware fusion within a single model.<n>Experiments on public IVIF, MFF, and MEF benchmarks confirm superior quantitative and qualitative performance, sharper textures, and better semantic retention.
  arXiv  Detail & Related papers  (2025-12-08T05:04:54Z)
• OmniParser V2: Structured-Points-of-Thought for Unified Visual Text Parsing and Its Generality to Multimodal Large Language Models [58.45517851437422]
  Visually-situated text parsing (VsTP) has recently seen notable advancements, driven by the growing demand for automated document understanding.<n>Existing solutions often rely on task-specific architectures and objectives for individual tasks.<n>In this paper, we introduce Omni V2, a universal model that unifies VsTP typical tasks, including text spotting, key information extraction, table recognition, and layout analysis.
  arXiv  Detail & Related papers  (2025-02-22T09:32:01Z)
• ContextFormer: Redefining Efficiency in Semantic Segmentation [48.81126061219231]
  Convolutional methods, although capturing local dependencies well, struggle with long-range relationships.<n>Vision Transformers (ViTs) excel in global context capture but are hindered by high computational demands.<n>We propose ContextFormer, a hybrid framework leveraging the strengths of CNNs and ViTs in the bottleneck to balance efficiency, accuracy, and robustness for real-time semantic segmentation.
  arXiv  Detail & Related papers  (2025-01-31T16:11:04Z)
• Hardware-Friendly Diffusion Models with Fixed-Size Reusable Structures for On-Device Image Generation [0.4666493857924357]
  Vision Transformers and U-Net architectures have been widely adopted in the implementation of Diffusion Models.<n>We propose an architecture that utilizes a fixed-size, reusable transformer block as a core structure.<n>Our architecture is characterized by low complexity, token-free design, absence of positional embeddings, uniformity, and scalability.
  arXiv  Detail & Related papers  (2024-11-09T08:58:57Z)
• UniNet: Unified Architecture Search with Convolution, Transformer, and MLP [62.401161377258234]
  In this paper, we propose to jointly search the optimal combination of convolution, transformer, and COCO for building a series of all-operator network architectures. We identify that the widely-used strided convolution or pooling based down-sampling modules become the performance bottlenecks when operators are combined to form a network. To better tackle the global context captured by the transformer and operators, we propose two novel context-aware down-sampling modules.
  arXiv  Detail & Related papers  (2021-10-08T11:09:40Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.