論文の概要: LLM-enabled Behavior Driven Development Workflow for Formally Verified Hardware Designs

• arxiv url: http://arxiv.org/abs/2609.15318v1
• Date: Mon, 14 Sep 2026 10:08:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-16 07:15:06.259655
• Title: LLM-enabled Behavior Driven Development Workflow for Formally Verified Hardware Designs
• Title（参考訳）: 形式的検証ハードウェア設計のためのLCM対応行動駆動開発ワークフロー
• Abstract要約: 制御された自然言語(CNL)仕様は中核として機能し、解釈可能性を維持しながら曖昧さを低減できる。 我々は,CNL仕様を正式に検証されたハードウェア設計の基礎として,FV Gherkin Scenarios(Formal Verification Gherkin Scenarios)を導入し,定義する。
• 参考スコア（独自算出の注目度）: 6.993866597392993
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recently, the use of Large Language Models (LLMs) for different tasks in the Electronic Design Automation (EDA) life-cycle has been studied extensively, but an integrated view is lacking. Specifications are the foundation of this life-cycle, but they suffer from ambiguity when written in natural language, which especially affects the quality of LLM output. Formal specifications mitigate these ambiguities, but they come with their own challenges. On the other hand, Controlled Natural Language (CNL) specifications can serve as a middle-ground, reducing ambiguity while retaining interpretability. In this work, we propose an integrated view on the use of LLMs for EDA and establish an LLM-enabled behavior driven hardware development workflow. We introduce and define Formal Verification Gherkin Scenarios (FV Gherkin Scenarios), unlocking CNL specifications as the foundation for formally verified hardware designs via Formal Property Verification (FPV). Experimental evaluation shows that our workflow is able to outperform other established LLM-based methods by 2.48x in functional correctness of generated Register Transfer Level (RTL) designs and by 2.54x in formal coverage of generated assertions for FPV.
• Abstract（参考訳）: 近年,電子設計自動化(Electronic Design Automation, EDA)のライフサイクルにおいて,様々なタスクにLarge Language Models(LLM)を用いることが広く研究されているが,統合的な視点は欠如している。 仕様は、このライフサイクルの基礎であるが、自然言語で書かれたときに曖昧さに悩まされ、特にLLM出力の品質に影響を及ぼす。 形式的な仕様はこれらの曖昧さを緩和しますが、彼ら独自の課題があります。 一方、制御された自然言語(CNL)仕様は中核として機能し、解釈可能性を維持しながら曖昧さを低減できる。 本研究では,EDA における LLM の利用を総合的に検討し,LCM を利用した行動駆動型ハードウェア開発ワークフローを構築する。 本稿では,CNL仕様をFPV (Formal Property Verification) を通じて正式に検証されたハードウェア設計の基礎として,FV Gherkin Scenarios (FV Gherkin Scenarios) を導入・定義する。 実験により,本ワークフローは,生成したレジスタ転送レベル(RTL)設計の関数的正当性を2.48倍,生成したFPVアサーションの形式的カバレッジを2.54倍に向上させることができることがわかった。

関連論文リスト

• Interpretable and Verifiable Hardware Generation with LLM-Driven Stepwise Refinement [6.8152454268325835]
  大規模言語モデル(LLM)は、ソフトウェア開発で顕著な成功を収めた。 幻覚の影響を受けやすいため、微妙な意味的・論理的な誤りを起こすことができる。 本稿では,LCMの創造性と幅広い知識と,形式的手法の説明可能性と数学的厳密さを組み合わせたハードウェア生成フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-06-16T01:28:22Z)
• LLM-Assisted Repository-Level Generation with Structured Spec-Driven Engineering [4.751657370831477]
  State-of-the-art Large Language Models (LLMs) は関数レベルでコード生成に優れるが、リポジトリレベルのシステムにスケールすると出力品質が大幅に低下する。 これを解決するために、構造化スペック駆動工学(SSDE)を提案する。 LLM入力として構造化された仕様は、優れた妥当性を提供すると同時に、高品質でリポジトリレベルのコード生成を明確な目標とします。
  論文  参考訳（メタデータ） (2026-05-04T10:58:22Z)
• LLM-FSM: Scaling Large Language Models for Finite-State Reasoning in RTL Code Generation [3.4714122723537333]
  LLM-FSMは,大規模言語モデル (LLM) が有限状態マシン (FSM) の動作をどの程度回復できるかを評価するベンチマークである。 手動で構築された例に依存する以前の仕様-RTLベンチマークとは異なり、LLM-FSMは完全に自動化されたパイプラインで構築されている。
  論文  参考訳（メタデータ） (2026-02-03T04:48:26Z)
• Latent Factor Models Meets Instructions: Goal-conditioned Latent Factor Discovery without Task Supervision [50.45597801390757]
  Instruct-LFはゴール指向の潜在因子発見システムである。 命令フォロー機能と統計モデルを統合して、ノイズの多いデータセットを処理する。
  論文  参考訳（メタデータ） (2025-02-21T02:03:08Z)
• FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware [4.480157114854711]
  FVEvalは,形式的検証(FV)に関わるタスクにおいて,大規模言語モデル(LLM)のパフォーマンスを特徴付ける最初の総合ベンチマークである。 ベンチマークは3つのサブタスクで構成され、異なるレベルでLLM能力を測定する。 本稿では,FVに整合した合成例を生成するための,専門家による検証手法と手法のコレクションについて述べる。
  論文  参考訳（メタデータ） (2024-10-15T21:48:57Z)
• Embodied Agent Interface: Benchmarking LLMs for Embodied Decision Making [85.24399869971236]
  我々は,大規模言語モデル(LLM)を具体的意思決定のために評価することを目指している。 既存の評価は最終的な成功率にのみ依存する傾向がある。 本稿では,様々なタスクの形式化を支援する汎用インタフェース (Embodied Agent Interface) を提案する。
  論文  参考訳（メタデータ） (2024-10-09T17:59:00Z)
• SELF-GUIDE: Better Task-Specific Instruction Following via Self-Synthetic Finetuning [70.21358720599821]
  大規模言語モデル(LLM)は、適切な自然言語プロンプトを提供する際に、多様なタスクを解決するという約束を持っている。 学生LLMからタスク固有の入出力ペアを合成する多段階メカニズムであるSELF-GUIDEを提案する。 ベンチマークの指標から,分類タスクに約15%,生成タスクに18%の絶対的な改善を報告した。
  論文  参考訳（メタデータ） (2024-07-16T04:41:58Z)
• $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks [21.12437562185667]
  本稿では,形式構文を自然言語に翻訳する際のLLM評価のスケールアップ手法を提案する。 我々は、文脈自由文法(CFG)を用いて、その場で配布外のデータセットを生成する。 我々はまた、このパラダイムの実現可能性と拡張性を示すために、複数のSOTAクローズドおよびオープンソースLCMの評価を行う。
  論文  参考訳（メタデータ） (2024-03-27T08:08:00Z)
• FOFO: A Benchmark to Evaluate LLMs' Format-Following Capability [70.84333325049123]
  FoFoは、大規模言語モデル(LLM)の複雑なドメイン固有のフォーマットに従う能力を評価するための先駆的なベンチマークである。 本稿では,大規模言語モデル(LLM)の複雑なドメイン固有フォーマットに従う能力を評価するための先駆的ベンチマークであるFoFoを提案する。
  論文  参考訳（メタデータ） (2024-02-28T19:23:27Z)
• If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
  大型言語モデル(LLM)は、自然言語と形式言語(コード)の組み合わせに基づいて訓練される コードは、標準構文、論理一貫性、抽象化、モジュール性を備えた高レベルの目標を実行可能なステップに変換する。
  論文  参考訳（メタデータ） (2024-01-01T16:51:20Z)
• Assessing the Reliability of Large Language Model Knowledge [78.38870272050106]
  大規模言語モデル(LLM)は、知識探索タスクにおける高い性能のため、知識ベースとして扱われてきた。 LLMが実際に正しい答えを連続的に生成する能力をどのように評価するか。 LLMの信頼性を直接測定するための新しい指標であるMOdel kNowledge relIabiliTy score (MONITOR)を提案する。
  論文  参考訳（メタデータ） (2023-10-15T12:40:30Z)

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

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