論文の概要: EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR

• arxiv url: http://arxiv.org/abs/2604.16571v1
• Date: Fri, 17 Apr 2026 12:09:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-28 14:27:13.333277
• Title: EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR
• Title（参考訳）: EquivFusion:MLIRによるアルゴリズムからネットリストへのハードウェア等価チェックの統合
• Authors: Jiaying Zhu, Baoqi Zhang, Mengxia Tao, Kezhi Li, Hao Yan, Qiang Xu, Min Li,
• Abstract要約: EquivFusionはマルチモーダル回路の設計に適したエンドツーエンドの等価チェックツールである。 PyTorch、C/C++、Chisel、Verilog、ゲートレベルのネットリストなど、さまざまなエントリポイントを共通の中間表現に統合する。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: 高レベルのアルゴリズムモデルと低レベルのハードウェア実装間の機能一貫性を確保することは、特に、ディープラーニングフレームワークからハードウェアネットリストに至るまで、現代的な設計フローが多種多様な抽象化にまたがっているため、重要な課題である。 本稿では,マルチモーダル回路設計に適したエンドツーエンドの等価チェックツールであるEquivFusionを提案する。 サイロツールやアドホック翻訳に依存する従来のフローとは異なり、EquivFusionは検証指向のMLIRローディングパイプラインを活用して、PyTorch、C/C++、Chisel、Verilog、ゲートレベルのネットリストなどのさまざまなエントリポイントを共通の中間表現に統合する。 このアーキテクチャは、設計をSMT-LIB、BTOR2、AIGERといった標準形式に厳格に翻訳することで、様々な抽象化レベルにわたる自動化されたペアワイズ等価性チェックを可能にする。 我々は、EquivFusionがソフトウェア仕様とハードウェア実現のセマンティックギャップを埋める可能性を示し、データパス集約型ハードウェア設計の「シフトレフト」形式検証を促進する効果を示した。

関連論文リスト

• VeriGraphi: A Multi-Agent Framework of Hierarchical RTL Generation for Large Hardware Designs [5.354071922171165]
  本稿では,RTL生成パイプラインを駆動するアーキテクチャ基板として,仕様記述型知識グラフを導入するフレームワークであるVeriGraphiを紹介する。 VeriGraphi は RISC-V に対する人間の介入を最小限に抑え, 信頼性の高い階層型 RTL 生成を可能にする。
  論文  参考訳（メタデータ） (2026-04-16T02:30:57Z)
• UniDial-EvalKit: A Unified Toolkit for Evaluating Multi-Faceted Conversational Abilities [70.79422099851506]
  対話型AIシステム評価のための統合評価ツールキットUniDial-EvalKit(UDE)を提案する。 UDEは異種データフォーマットを普遍的なスキーマに標準化し、モジュールアーキテクチャを通じて複雑な評価パイプラインを合理化し、一貫したスコアリングインターフェースの下でメートル法計算を調整する。
  論文  参考訳（メタデータ） (2026-03-24T13:01:31Z)
• Beyond Pixels: Vector-to-Graph Transformation for Reliable Schematic Auditing [34.54168175788343]
  本稿では,CAD図をノードがコンポーネントを表現し,エッジが接続を符号化するプロパティグラフに変換するVector-to-Graph(V2G)パイプラインを提案する。 電気的コンプライアンスチェックの診断ベンチマークでは、V2Gは全てのエラーカテゴリで大きな精度向上を達成し、MLLMのリードは確率レベルに近づいたままである。
  論文  参考訳（メタデータ） (2026-02-12T07:50:49Z)
• Plain Transformers are Surprisingly Powerful Link Predictors [57.01966734467712]
  リンク予測はグラフ機械学習における中核的な課題であり、リッチで複雑なトポロジ的依存関係をキャプチャするモデルを必要とする。 グラフニューラルネットワーク(GNN)が標準的なソリューションであるのに対して、最先端のパイプラインは明示的な構造やメモリ集約的なノードの埋め込みに依存していることが多い。 本報告では,手作りのプリミティブに置き換えるエンコーダのみのプレーントランスであるPENCILについて,サンプリングしたローカルサブグラフに注目する。
  論文  参考訳（メタデータ） (2026-02-02T02:45:52Z)
• VSA:Visual-Structural Alignment for UI-to-Code [29.15071743239679]
  視覚テキストアライメントにより組織化された資産を合成するための多段階パラダイムであるbfVSA(VSA)を提案する。 私たちのフレームワークは、最先端のベンチマークよりもコードのモジュール化とアーキテクチャの一貫性を大幅に改善します。
  論文  参考訳（メタデータ） (2025-12-23T03:55:45Z)
• Towards Unified Semantic and Controllable Image Fusion: A Diffusion Transformer Approach [99.80480649258557]
  DiTFuseは命令駆動のフレームワークで、単一のモデル内でセマンティクスを意識した融合を実行する。 パブリックなIVIF、MFF、MEFベンチマークの実験では、より優れた量的および質的な性能、よりシャープなテクスチャ、より優れたセマンティック保持が確認されている。
  論文  参考訳（メタデータ） (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]
  VsTP(Visually-situated text parsing)は、自動化された文書理解の需要が高まり、最近顕著な進歩を遂げている。 既存のソリューションは、タスク固有のアーキテクチャと個々のタスクの目的に依存していることが多い。 本稿では,テキストスポッティング,キー情報抽出,テーブル認識,レイアウト解析など,VsTPの典型的なタスクを統一する汎用モデルであるOmni V2を紹介する。
  論文  参考訳（メタデータ） (2025-02-22T09:32:01Z)
• ContextFormer: Redefining Efficiency in Semantic Segmentation [48.81126061219231]
  畳み込み法は、局所的な依存関係をうまく捉えるが、長距離関係に苦慮する。 ビジョントランスフォーマー(ViT)は、グローバルなコンテキストキャプチャでは優れるが、高い計算要求によって妨げられる。 我々は,リアルタイムセマンティックセグメンテーションの効率,精度,堅牢性のバランスをとるために,CNN と ViT の強みを活用したハイブリッドフレームワーク ContextFormer を提案する。
  論文  参考訳（メタデータ） (2025-01-31T16:11:04Z)
• Hardware-Friendly Diffusion Models with Fixed-Size Reusable Structures for On-Device Image Generation [0.4666493857924357]
  ビジョントランスフォーマーとU-Netアーキテクチャは拡散モデルの実装において広く採用されている。 固定サイズ再利用可能なトランスブロックをコア構造として利用するアーキテクチャを提案する。 私たちのアーキテクチャの特徴は、複雑さの低い、トークンのない設計、位置埋め込みの欠如、均一性、スケーラビリティです。
  論文  参考訳（メタデータ） (2024-11-09T08:58:57Z)
• UniNet: Unified Architecture Search with Convolution, Transformer, and MLP [62.401161377258234]
  本稿では,コンボリューション,トランスフォーマー,COCOの最適組み合わせを共同で探索し,一連の全演算型ネットワークアーキテクチャを構築することを提案する。 広範に使われているストリップド・コンボリューション (strided convolution) あるいはプール・ベース・ダウンサンプリング・モジュールは,演算子を結合してネットワークを形成する場合,性能上のボトルネックとなる。 変換器と演算子によって捕捉されるグローバルなコンテキストによりよく対処するために,2つの新しいコンテキスト対応ダウンサンプリングモジュールを提案する。
  論文  参考訳（メタデータ） (2021-10-08T11:09:40Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。