論文の概要: From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation
- arxiv url: http://arxiv.org/abs/2604.23100v1
- Date: Sat, 25 Apr 2026 01:46:33 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-28 17:12:07.155468
- Title: From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation
- Title（参考訳）: 言語から論理へ: ブリッジング LLM と RTL アクセレーション生成のための形式表現
- Authors: Nowfel Mashnoor, Hadi Kamali, Kimia Azar,
- Abstract要約: SystemVerilog Assertions (SVA) はデジタルハードウェアの正式な検証に不可欠である。
近年,大規模言語モデル(LLM)を用いてSVA生成を自動化する手法が研究されている。
本稿では,自然言語仕様からSVAを生成するツール拡張ReActエージェントProofLoopを提案する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: SystemVerilog Assertions (SVA) are essential for formal verification of digital hardware, yet their manual creation demands significant expertise in both the design under verification and temporal logic. Recent studies have explored using large language models (LLMs) to automate SVA generation, but existing approaches suffer from incorrect signal references, missing timing constraints, and lack of formal correctness guarantees. This paper presents ProofLoop, a tool-augmented ReAct agent that generates SVA from natural-language specifications using a solver-in-the-loop approach. The agent operates in two phases: Phase A autonomously gathers design context by invoking EDA and formal tools, including semantic search over an AST-indexed vector database and JasperGold structural queries, while Phase B generates SVA and iteratively refines it using JasperGold formal proof feedback over up to fixed (here 3) verification rounds. We evaluate ProofLoop on FVEval Design2SVA design benchmarks and demonstrate that this framework can achieve 93.7% syntax correctness and 82.0% functional correctness. An ablation study confirms that each component, i.e., retrieval-augmented generation (RAG), JasperGold tools, and the verification loop contributes significantly (and orthogonally).
- Abstract（参考訳）: SystemVerilog Assertions (SVA) はデジタルハードウェアの形式的検証に必須であるが、その手作業による作成は検証と時間論理の両方の設計において重要な専門知識を必要とする。
近年, 大規模言語モデル(LLM)を用いてSVA生成を自動化する手法が検討されているが, 既存のアプローチでは誤った信号参照, タイミング制約の欠如, 正式な正当性保証の欠如などが問題となっている。
本稿では,自然言語仕様からSVAを生成するツール拡張型ReActエージェントProofLoopを提案する。
このエージェントは2つのフェーズで動作する: フェーズAは、EDAと形式ツールを自動で呼び出し、ASTインデックス付きベクトルデータベースとJasperGold構造クエリのセマンティック検索を含む設計コンテキストを収集する。
我々は、FVEval Design2SVA設計ベンチマーク上でProofLoopを評価し、93.7%の構文正当性と82.0%の関数正当性を達成できることを実証した。
アブレーション研究では、各コンポーネント、すなわち、検索強化生成(RAG)、JasperGoldツール、検証ループが著しく(直交的に)寄与していることが確認されている。
関連論文リスト
- AgentV-RL: Scaling Reward Modeling with Agentic Verifier [63.55502685076245]
試験時間スケーリング(TTS)によるLCM推論を強化する検証器が実証されている。
本稿では,報酬モデリングを多ターンツール拡張型検討プロセスに変換するフレームワークであるエージェント検証を提案する。
Agentic Verifier は並列およびシーケンシャルTS の両方で一貫した性能向上が得られることを示す。
論文 参考訳（メタデータ） (2026-04-17T12:27:36Z) - 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) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。
数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。
我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
論文 参考訳（メタデータ） (2025-08-05T17:55:24Z) - AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction [32.14733357890831]
本稿では,高品質なSVAを自動的に生成する新しい統合フレームワークAssertCoderを提案する。
AssertCoderは、不均一な仕様フォーマットを解析するために、モダリティに敏感な事前処理を使用する。
このフレームワークは、アサーションの品質を評価するために、突然変異に基づく評価アプローチを取り入れている。
論文 参考訳（メタデータ） (2025-07-14T14:43:14Z) - Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting [0.0]
高品質なシステムVerilog Assertions (SVA) を自動生成する大規模言語モデル(LLM)に基づくフローを提案する。
サブタスクに着目したファインチューニング手法を導入し,機能的に正しいアサーションの数を7.3倍に増やした。
実験では、このアプローチを使って構文エラーのないアサーション数が26%増加した。
論文 参考訳（メタデータ） (2024-11-23T03:52:32Z) - Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。
QASemConsistencyは、人間の判断とよく相関する事実整合性スコアを得られることを示す。
論文 参考訳（メタデータ） (2024-10-09T22:53:48Z) - ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation [10.503097140635374]
ChIRAAGはOpenAI GPT4をベースとして、設計の自然言語仕様からSystem Verilog Assertion (SVA)を生成する。
実験では、LSM生成した生のアサーションの27%に誤りがあり、数回の反復で修正された。
以上の結果から,LLMはアサーション生成プロセスにおいて技術者を合理化し,支援し,検証を再構築できることが示唆された。
論文 参考訳（メタデータ） (2024-01-31T12:41:27Z) - Knowledge-Augmented Language Model Verification [68.6099592486075]
最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。
本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。
その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
論文 参考訳（メタデータ） (2023-10-19T15:40:00Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。