同じ動作の回路で検証条件の生成が変わるかを調べる
EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations
この論文をやさしく読む
ひとことで言うと
動作は同じで書き方が異なる回路をまとめ、LLMが作る検証条件が実装の見た目に左右されるかを評価するデータセットです。
何に役立つ？
回路検証用のアサーションを生成するモデルについて、意図した機能を捉える頑健性を調べるのに役立ちます。等価な回路を同じ族にまとめ、学習とテストの混入も避けています。
この研究の面白いところ
単に正解回路とバグ回路を比べるだけでなく、同じ動作を保った四つの構造を比較できます。例示したモデルでは、24族中14族で健全な生成条件の数が変わりました。
どこまで分かった？
293件中93件が形式的に健全だったという数値は、例示した一つのモデルとテスト分割の結果です。健全であることは、必要な仕様をすべて網羅したことを意味しません。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
自然言語の仕様とレジスタ転送レベル（RTL）の設計からSystemVerilog Assertionsを生成するために、大規模言語モデルが使われるようになっている。既存のデータセットとベンチマークは、大規模学習、形式評価、仕様からのアサーション生成、変異に基づくテストなどの重要な目的を支えている。これを補う課題として、生成されたアサーションが外部から観測できる動作を捉えているのか、それとも一つのRTL実装にたまたま含まれる詳細に依存しているのかを調べる必要がある。 本研究では、動作の族ごとに整理した形式検証済みデータセットEquivSVAを提示する。各族には、同じ外部観測可能な動作を持つ、構造の異なる四つのRTL実装、共通のインターフェース水準の正解プロパティ、制御された三つの変異体、形式検証の証拠が含まれる。EquivSVAは12カテゴリの120動作族、480の参照RTL実装、914の正解プロパティ、360の変異体を含む。最終的な各族は、RTLの等価性、正解プロパティの証明、プロパティの到達可能性、変異体の識別可能性、変異体での正解プロパティの確認を含む、固定の17ジョブの検証一式をすべて通過している。動作族が分割をまたがない固定の学習・開発・テスト分割も提供する。 データセットで可能になる分析の小規模な実例として、Apache-2.0ライセンスで公開されたQwen2.5-Coder-7B-Instructを、取り置いたテスト分割で評価する。インターフェースだけを参照して生成された293プロパティのうち、93が形式的に健全であり、24のテスト族のうち14では、等価な実装の間で健全なプロパティ数が異なった。これらの結果は、意図する機能を変更することなく、動作族による構成を使ってアサーション生成の頑健性を統制された条件で調べられることを示す。データセット、生成器、検証スクリプト、事例分析の成果物は https://github.com/aditigupta96/EquivSVA で公開する。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-22（UTC）
- 最新改訂
- 2026-09-22 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-22 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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.
著者のコメント
EquivSVA is a 9-page paper by FNU Aditi introducing a formally verified dataset of 120 behavior families, 480 RTL implementations, 914 gold properties, and 360 mutants across 12 categories, featuring 2 figures, 5 tables, and a case study evaluating Qwen2.5-Coder-7B-Instruct
arXiv ID: 2609.26751 ／ 要約の誤りについて