論文の概要: FormalRTL: Verified RTL Synthesis at Scale

• arxiv url: http://arxiv.org/abs/2603.08738v1
• Date: Wed, 25 Feb 2026 04:58:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-15 16:38:22.510612
• Title: FormalRTL: Verified RTL Synthesis at Scale
• Title（参考訳）: FormalRTL: 大規模RTL合成の検証
• Authors: Kezhi Li, Min Li, Xiangyu Wen, Shibo Zhao, Jieying Wu, Junhua Huang, Qiang Xu,
• Abstract要約: 本稿では,ソフトウェア参照モデルを形式的かつ実行可能な仕様として統合する,新しいエンドツーエンドマルチエージェントフレームワークであるFormalRTLを提案する。 FormalRTLは、計画、合成、形式的等価性チェックの密結合により、スケーラブルで信頼性の高いハードウェアコード生成を実現する。 この分野における今後の研究を促進するために,FormalRTLフレームワークとベンチマークスイートをオープンソースとして公開します。
• 参考スコア（独自算出の注目度）: 13.063660438578575
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models (LLMs) have demonstrated significant potential in automating hardware synthesis, yet substantial barriers remain for industrial-scale, datapath-centric designs due to ambiguous specifications and a lack of formal correctness guarantees. In this work, we present FormalRTL, a novel end-to-end multi-agent framework that systematically integrates software reference models as formal, executable specifications to guide register-transfer level (RTL) code generation and verification. By tightly coupling planning, synthesis, and formal equivalence checking, FormalRTL achieves scalable and reliable hardware code generation that addresses the critical challenges faced in industrial contexts. The comprehensive evaluation of a new suite of complex industrial-grade benchmarks demonstrates the effectiveness and robustness of our approach. We will open-source the FormalRTL framework and the benchmark suite to facilitate future research in this area.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、ハードウェア合成の自動化において大きな可能性を証明しているが、不明瞭な仕様と正式な正当性保証の欠如により、産業規模でデータパス中心の設計には重大な障壁が残っている。 本稿では,ソフトウェア参照モデルを形式的かつ実行可能な仕様として体系的に統合し,レジスタ転送レベル(RTL)コード生成と検証をガイドする,新しいエンドツーエンドマルチエージェントフレームワークであるFormalRTLを提案する。 FormalRTLは、計画、合成、形式的等価性チェックの密結合によって、産業環境で直面する重要な課題に対処するスケーラブルで信頼性の高いハードウェアコード生成を実現する。 新しい産業レベルのベンチマークスイートの包括的な評価は、我々のアプローチの有効性と堅牢性を示している。 この分野における今後の研究を促進するために,FormalRTLフレームワークとベンチマークスイートをオープンソースとして公開します。

関連論文リスト

• Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
  大規模言語モデル(LLM)は、複雑なソフトウェア工学に必要な、深く、長期にわたる推論に苦しむことが多い。 本稿では,再構築による理解という,新しいパラダイムを提案する。 マルチエージェントシミュレーションを用いて潜在エージェント軌道を合成するフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-11T09:23:20Z)
• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。 エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
  論文  参考訳（メタデータ） (2026-01-27T16:10:23Z)
• A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs [34.387390697713556]
  本稿では、フォーマルな仕様の生成と改善を自動化するためのモジュラーできめ細かいフレームワークであるPregussについて述べる。 以上の結果から, Preguss は最先端の LLM ベースのアプローチを大きく上回っていることがわかった。 約1000LOCを超える実世界のプログラムに対して高度に自動化されたRTE-freeness検証を可能にし、80.6%88.9%の人間による検証を削減した。
  論文  参考訳（メタデータ） (2025-12-31T03:31:51Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1は、このギャップを埋めるための自動化および半自動化アプローチを調査することを目的としている。 本論文では, 課題の繰り返しと今後の研究方向性を明らかにするために, 関連文献の予備的な合成について述べる。
  論文  参考訳（メタデータ） (2025-07-18T19:15:50Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)

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

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