論文の概要: EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations
- arxiv url: http://arxiv.org/abs/2609.26751v1
- Date: Tue, 22 Sep 2026 17:33:09 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-24 01:05:39.772479
- Title: EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations
- Title（参考訳）: EquivSVA: 等価RTL実装全体にわたる行動補助の形式的検証されたデータセット
- Abstract要約: EquivSVAは、行動家族を中心に編成されたデータセットである。
各ファミリーは、同じ外部観測可能な振る舞いの4つの構造的に異なるRTL実装を含んでいる。
RTL等価性、ゴールドプロパティ証明、プロパティリーチビリティ、ミュータント・ディスタンダビリティ、およびミュータントに対するゴールドプロパティチェックを含む固定された17-ジョブ検証スイートをパスする。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large language models are increasingly used to generate SystemVerilog Assertions from natural-language specifica- tions and register-transfer-level designs. Existing datasets and benchmarks support important goals such as large- scale training, formal evaluation, specification-to-assertion generation, and mutation-based testing. A complemen- tary need is to study whether a generated assertion cap- tures externally observable behavior or depends on inci- dental details of one RTL implementation. We present EquivSVA, a formally verified dataset organized around behavior families. Each family contains four structurally distinct RTL implementations of the same externally ob- servable behavior, shared interface-level gold properties, three controlled mutants, and formal-validation evidence. EquivSVA contains 120 behavior families across 12 cat- egories, 480 reference RTL implementations, 914 gold properties, and 360 mutants. Every final family passes a fixed 17-job validation suite covering RTL equivalence, gold-property proofs, property reachability, mutant dis- tinguishability, and gold-property checks on mutants. We also provide fixed family-safe train, development, and test splits. As a small demonstration of the analyses en- abled by the dataset, we evaluate the publicly released, Apache-2.0-licensed Qwen2.5-Coder-7B-Instruct model on the held-out test split. Of 293 interface-only generated properties, 93 are formally sound, and the number of sound properties varies across equivalent implementations for 14 of 24 test families. These results illustrate how behavior-family organization can support controlled stud- ies of assertion-generation robustness without requiring changes in intended functionality. The dataset, generators, validation scripts, and case-study artifacts are publicly released at https://github.com/aditigupta96/EquivSVA.
- Abstract（参考訳）: 大規模言語モデルは、自然言語の種別とレジスタ・トランスファーレベルの設計からSystemVerilog Assertionsを生成するために、ますます使われている。
既存のデータセットとベンチマークは、大規模なトレーニング、正式な評価、仕様から承認までの生成、突然変異ベースのテストといった重要な目標をサポートする。
コンプレメン-タリーの必要性は、生成したアサーションキャップが外部から観察可能な振る舞いを観察するか、または1つのRTL実装の切歯の細部に依存するかを調べることである。
EquivSVAは、行動家族を中心に構成された正式に検証されたデータセットである。
各ファミリーは、同じ外部観測可能な振る舞い、共有インターフェースレベルの金の特性、制御された3つのミュータント、形式検証証拠の4つの構造的に異なるRTL実装を含んでいる。
EquivSVAは12のネコエゴリー、480のリファレンスRTL実装、914のゴールド特性、360のミュータントを含む120の行動ファミリーを含んでいる。
RTL等価性、ゴールドプロパティ証明、プロパティリーチビリティ、ミュータント・ディスタンダビリティ、およびミュータントに対するゴールドプロパティチェックを含む固定された17-ジョブ検証スイートをパスする。
また、固定された家族安全列車、開発、テストスプリットも提供します。
データセットによって実現された分析の小さなデモとして、私たちは、公開されているApache-2.0ライセンスのQwen2.5-Coder-7B-Instructモデルを、ホールドアウトテストスプリット上で評価した。
293のインタフェースのみを生成する特性のうち、93は正式に音であり、24の試験ファミリーのうち14の等価実装ごとに音質の数は異なる。
これらの結果は,アサーション・ジェネレーション・ロバスト性の制御されたスタッドを,意図した機能の変更を必要とせずに支援できることを示す。
データセット、ジェネレータ、検証スクリプト、ケーススタディアーティファクトはhttps://github.com/aditigupta96/EquivSVAで公開されている。
関連論文リスト
- EvolveScaler: Synthesizing Information-Evolution Contexts via Executable State Machines and Natural-Language Rendering [57.87517047585447]
我々はEvolveScalerを紹介した。EvolveScalerはコード駆動のフレームワークで、自然言語としてレンダリングする前に情報進化を定義する。
EvolveScalerを117のタスクプロトタイプと159のファイナルクエスト演算子でインスタンス当たり約7～1200のイベントにまたがる5つの難易度でインスタンス化する。
very_longティアでは、最強のモデルが59.3%のavg@5に達し、6つのモデルが10%以下である。
論文 参考訳（メタデータ） (2026-09-08T08:40:05Z) - PROGRESS: Property-Guided Regression Search for Semantic Falsification [16.94326144914702]
提案する進歩(意味的偽造に対するPROperty-Guided Regression Search)
インテント駆動プロパティをカバレッジに基づく、検索ベースの進化的テスト生成に統合して、深いプログラム状態に到達する。
328/562の電流反転バグ(58%)をレグレッションテスト生成では検出し、スタンドアロンのjqwikでは18に対して70/150のハード・ツー・リーチ特性では条件をすべて満たしている。
論文 参考訳（メタデータ） (2026-07-29T18:12:12Z) - Causal dictionary learning reveals and validates transcription-factor binding features in genomic language models [5.237172334460829]
ゲノム基盤モデルにおいて、スパース辞書学習と因果介入を組み合わせて、解釈可能な特徴を抽出し、検証し、因果的にテストする枠組みを導入する。
位置重み行列に対するこれらの特徴の素性検証は,GC合成と反復的要素によって著しく整合されていることを示す。
我々は,特定の特徴が,単にモチーフの存在ではなく,細胞型特異的TF結合を表現するために機能的に用いられていることを確認した。
論文 参考訳（メタデータ） (2026-07-21T22:54:46Z) - Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing [6.28395649374318]
本稿では,Apache Spark計算における繰り返し特性パターンについて検討する。
我々は、プロパティテンプレートを使用して、Lean 4定理証明器の正確性を正式に検証するエージェント型デュアルトラック検証フレームワークを設計する。
評価の結果, 特性テンプレートは薬剤的証明工学的成功率を2.6倍(平均1.6倍)に向上し, 実証幻覚を59%減少させることがわかった。
論文 参考訳（メタデータ） (2026-07-10T03:33:47Z) - Beyond Value Benchmarks: Measuring Value-Structure Alignment in Large Language Models via Symmetric Q-Sorts [47.02978329409663]
そこで本研究では,Q手法に基づく対称型人間-LLM評価フレームワークを提案する。
私たちのプロトコルでは、人間とモデルは同一の140項目の道徳的ステートメントを、共有された9カラムの強制分布に分類します。
240個の複製されたQ-sortを2つの温度設定で4つのモデルファミリーにまたがる12個のLLMを評価した。
論文 参考訳（メタデータ） (2026-06-20T08:15:41Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation [0.0]
SystemVerilog Assertions (SVA) はデジタルハードウェアの正式な検証に不可欠である。
近年,大規模言語モデル(LLM)を用いてSVA生成を自動化する手法が研究されている。
本稿では,自然言語仕様からSVAを生成するツール拡張ReActエージェントProofLoopを提案する。
論文 参考訳（メタデータ） (2026-04-25T01:46:33Z) - Automated Self-Testing as a Quality Gate: Evidence-Driven Release Management for LLM Applications [51.56484100374058]
我々は,エビデンスに基づくリリース決定を伴う品質ゲートを導入する自動自己テストフレームワークを提案する。
内部展開型多エージェント対話型AIシステムの縦型ケーススタディにより,本フレームワークの評価を行った。
論文 参考訳（メタデータ） (2026-03-13T20:44:15Z) - VeriCoder: Enhancing LLM-Based RTL Code Generation through Functional Correctness Validation [11.548011504703693]
本稿では,関数的正当性を検証したデータセットを微調整した RTL コード生成モデル VERICODER を提案する。
この125,777例のデータセットに基づいて、VERICODERはVerilogEvalとRTLLMの関数的正確性に関する最先端のメトリクスを達成している。
論文 参考訳（メタデータ） (2025-04-22T07:32:46Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。