論文の概要: Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement
- arxiv url: http://arxiv.org/abs/2608.18482v1
- Date: Wed, 19 Aug 2026 03:14:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-20 20:13:55.264625
- Title: Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement
- Title（参考訳）: ホルム探索とニューロシンボリックリファインメントを用いたカバー駆動型RTLアサーション生成
- Abstract要約: NeuroAssertionはカバレッジ駆動アサーション生成フレームワークである。
形式的トレース生成、構文誘導合成、エージェントインスパイアされた洗練を組み合わせている。
従来のアサーションマイニング法よりも約2倍のアサーションと約2倍の突然変異カバレッジを提供する。
- 参考スコア（独自算出の注目度）: 3.5085139194562456
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Hardware functional verification relies on high-quality assertions to expose design bugs and establish confidence in Register Transfer Level (RTL) designs. Yet existing assertion mining methods still struggle to produce complete and reliable assertion sets: random or limited traces fail to cover hard-to-reach behaviors, and one-shot generation provides little feedback about what remains unverified or how the assertion set should be improved. As a result, critical design behaviors can remain uncovered even when many assertions are generated. We present NeuroAssertion, a coverage-driven assertion generation framework that combines formal trace generation, syntax-guided synthesis (SyGuS), and an agent-inspired refinement process within a unified framework. Our framework first converts hard-to-reach control-flow conditions into formal reachability objectives, uses model checking to generate behaviorally diverse traces, and mines initial assertions from these traces with SyGuS. It then performs targeted agent-inspired refinement under verification feedback: one LLM first proposes candidate assertions for uncovered regions, and if a candidate fails formal checking, a second LLM generates a repair grammar that guides constrained symbolic synthesis in a neuro-symbolic repair procedure. Experimental results show that this framework delivers around 2X more assertions and about 2X higher mutation coverage than traditional assertion mining methods.
- Abstract（参考訳）: ハードウェア機能検証は、設計バグを公開し、レジスタ転送レベル(RTL)設計の信頼性を確立するために、高品質なアサーションに依存している。
しかし、既存のアサーションマイニング手法は、完全で信頼性の高いアサーションセットを生成するのに依然として苦労している: ランダムまたは制限されたトレースは、ハード・トゥ・リーチ動作をカバーすることができず、ワンショット生成は、まだ検証されていないものやアサーションセットをどのように改善すべきかについてほとんどフィードバックを提供していない。
その結果、多くのアサーションが生成される場合でも、重要な設計行動が発見される。
本稿では,形式的トレース生成,構文誘導合成(SyGuS),および統合フレームワーク内のエージェントインスパイアされた洗練プロセスを組み合わせた,カバレッジ駆動型アサーション生成フレームワークであるNeuroAssertionを紹介する。
我々のフレームワークは、まず、難解な制御フロー条件を形式的到達性目標に変換し、モデルチェックを使用して振る舞いに多様性のあるトレースを生成し、これらのトレースから初期アサーションをSyGuSでマイニングする。
1つのLSMは、未発見領域の候補アサーションを最初に提案し、もし候補が正式なチェックに失敗した場合、第2のLSMは、ニューロシンボリックな修復手順で制約付きシンボル合成をガイドする修復文法を生成する。
実験結果から,本フレームワークは従来のアサーションマイニング法よりも約2倍のアサーションと約2倍の突然変異カバレッジを実現することが示された。
関連論文リスト
- SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs [10.916179875278326]
我々は、形式的なコード合成をアトミックで再利用可能なスキルのライブラリに分解するフレームワークであるSKILLFORGEを紹介する。
検証駆動ハーネスはこれらのスキルを編成する。
Dafny仕様のペアに対する自然言語のキュレートされたベンチマークでは、SKILLFORGEは最先端のエージェントアプローチよりも大幅に優れている。
論文 参考訳（メタデータ） (2026-08-30T15:15:00Z) - Execution-Anchored Hallucination Calibration Reranking for Verilog Code Generation [19.257000641887828]
大規模言語モデル(LLM)はコード生成において顕著な能力を示しているが、その性能は低リソース言語では著しく低下している。
本稿では,実行行動に対する推論判断をアンロックするEAHCを提案する。
論文 参考訳（メタデータ） (2026-08-24T08:11:43Z) - Agent-Based Test Assertion Generation via Diverse Perspective Aggregation [13.443058740546164]
AssertMateはエージェントベースのアサーション生成フレームワークである。
これにより、大きな言語モデル(LLM)の生成したアサーションの品質と信頼性が向上する。
コンピレーションの成功とパスレートにおいて、最先端の技術よりも大幅に優れています。
論文 参考訳（メタデータ） (2026-08-06T09:51:43Z) - Escaping Confidence Trap: Evolutionary Decoding for Mathematical Reasoning in Diffusion LLMs [69.52853771994451]
我々はLLaDA 2.0の復号軌道を解析し、繰り返し拡散信頼トラップを同定する。
本稿では,拡散復号化を進化過程とみなす訓練不要なテスト時間スケーリングフレームワークである進化復号法を提案する。
論文 参考訳（メタデータ） (2026-08-01T11:48:25Z) - AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications [7.797719198801956]
本稿では,ハードウェア検証における現実的なアサーション生成のためのオープンソースのベンチマークであるAssertLLM2を紹介する。
AssertLLM2には13の機能カテゴリにわたる83の現実世界の設計が含まれている。
それぞれの設計について、このベンチマークは構造化された設計仕様、検証済みの依存性完全ゴールデンRTL、系統的に変更されたバグギーRTLの亜種を提供する。
論文 参考訳（メタデータ） (2026-05-26T10:49:25Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - 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) - Metacognitive Self-Correction for Multi-Agent System via Prototype-Guided Next-Execution Reconstruction [58.51530390018909]
大規模言語モデルに基づくマルチエージェントシステムは、協調的な問題解決において優れているが、エラーのカスケードには脆弱である。
我々は,MASにリアルタイム,教師なし,ステップレベルの誤り検出と自己補正を付与するメタ認知フレームワークMASCを提案する。
論文 参考訳（メタデータ） (2025-10-16T05:35:37Z) - Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳（メタデータ） (2025-05-28T17:57:47Z) - Are LLMs Ready for Practical Adoption for Assertion Generation? [6.3585378855805725]
ハードウェア検証の品質、すなわちコーナーケース設計バグの検出と診断は、アサーションの品質に大きく依存する。
TransformersやLarge-Language Models (LLMs)のような生成AIが登場したことで、関数型およびセキュリティアサーションを生成する新しい、効果的でスケーラブルな技術の開発への関心が高まっている。
論文 参考訳（メタデータ） (2025-02-28T01:34:45Z) - Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。
RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。
これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。
我々は、無害な」知識基盤の著作権保護の名称を提案する。
論文 参考訳（メタデータ） (2025-02-10T09:15:56Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。