論文の概要: AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs

• arxiv url: http://arxiv.org/abs/2604.22285v1
• Date: Fri, 24 Apr 2026 07:02:58 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-27 15:36:26.373029
• Title: AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs
• Title（参考訳）: AutoINV:高レベル合成設計における形式検証のための自動不変生成フレームワーク
• Authors: Xiaofeng Zhou, Linfeng Du, Guangyu Hu, Sharad Sinha, Hongce Zhang, Wei Zhang,
• Abstract要約: 高レベル合成(HLS)は、ハードウェアのアルゴリズムによる記述を高い抽象化からレジスタ転送レベル(RTL)設計に変換する。 HLSには、ツールの制限やエラーによる大きな機能的バグやセキュリティ脆弱性が含まれている可能性がある。 モデルチェッカーの誘導を目的としたヘルパーアサーションのセットを構築するために,HLSフローから高レベルな設計特徴を活用することを提案する。
• 参考スコア（独自算出の注目度）: 5.472549507568446
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: High-level synthesis (HLS) transforms an algorithmic description of hardware from a higher abstraction (e.g., C/C++) into a register-transfer level (RTL) design, offering reduced development time and greater flexibility in design space exploration. However, such machine-generated RTL designs may contain major functional bugs or security vulnerabilities due to limitations or errors in the HLS tools. One of the most reliable methods to identify these vulnerabilities is formal verification, particularly model checking. Nevertheless, the large size of the generated RTL often causes model checking to struggle to conclude within reasonable time or resource limits. In this study, we propose utilizing the high-level design features from the HLS flow to construct a set of helper assertions aimed at guiding the model checker and accelerating the verification process. To identify the most effective set of helpers to assist the model checker, we develop a proving mechanism that iteratively reuses proving information to select the potentially most useful set of helpers. We evaluate the proposed framework on a set of HLS design benchmarks. Experimental results demonstrate that, when compared to vanilla model checking, our approach achieves a speedup of up to 6.05x, and 2.23x on average.
• Abstract（参考訳）: 高レベル合成(HLS)は、ハードウェアのアルゴリズムによる記述を、より高い抽象化(例えばC/C++)からレジスタ-トランスファーレベル(RTL)設計に変換し、開発時間を短縮し、設計空間探索の柔軟性を高める。 しかし、そのようなマシン生成RTL設計は、HLSツールの制限やエラーにより、機能上の重大なバグやセキュリティ上の脆弱性を含む可能性がある。 これらの脆弱性を特定する最も信頼できる方法の1つは、正式な検証、特にモデルチェックである。 それでも、生成されたRTLの大きなサイズは、モデルチェックが妥当な時間やリソース制限内で結論付けるのに苦労する原因となることが多い。 本研究では,モデルチェッカーの誘導と検証プロセスの高速化を目的としたヘルパーアサーションを構築するために,HLSフローから高レベルな設計特徴を活用することを提案する。 モデルチェッカーを補助する最も効果的なヘルパー群を特定するため,実証情報を反復的に再利用し,潜在的に有用なヘルパー群を選択するための証明機構を開発した。 提案するフレームワークをHLS設計ベンチマークを用いて評価する。 実験の結果,バニラモデル検査と比較すると,提案手法は平均6.05倍,平均2.23倍の高速化を実現している。

関連論文リスト

• EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning [4.8941849720433686]
  ハードウェアモデルチェックベンチマークを生成するフレームワークであるEvolveGenを紹介する。 提案手法は、RLエージェントが計算グラフを構築することを学習するアルゴリズム的な抽象レベルで機能する。 実験の結果,EvolveGenは標準フォーマットの多様なベンチマークセットを効率的に作成できることがわかった。
  論文  参考訳（メタデータ） (2026-02-26T04:32:07Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。 本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
  論文  参考訳（メタデータ） (2025-10-02T06:25:10Z)
• FVDebug: An LLM-Driven Debugging Assistant for Automated Root Cause Analysis of Formal Verification Failures [8.530369312832084]
  障害トレースを実行可能な洞察に変換するインテリジェントなシステムであるFV Debugを紹介します。 提案手法は,(1)非巡回グラフに障害トレースを構造化する因果グラフ合成,(2)不審なノードの特定を促すバッチ型Large Language Model (LLM)解析を用いたグラフスキャナ,(3)高レベルの因果説明を生成するためのエージェント的物語探索を活用したInsight Roverを特徴とする。
  論文  参考訳（メタデータ） (2025-09-16T20:22:10Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  より大規模なモデルではなく、推論時間の増加を活用する統合されたテスト時間計算スケーリングフレームワークを提案する。 当社のフレームワークには,内部TTCと外部TTCの2つの補完戦略が組み込まれている。 当社の textbf32B モデルは,DeepSeek R1 671B や OpenAI o1 など,はるかに大きなモデルを上回る 46% の課題解決率を実現している。
  論文  参考訳（メタデータ） (2025-03-31T07:31:32Z)
• Can Reasoning Models Reason about Hardware? An Agentic HLS Perspective [18.791753740931185]
  OpenAI o3-mini と DeepSeek-R1 は Chain-of-Thought (CoT) を通じて推論を強化している 本稿では, LLM の推論が高レベル合成(HLS)設計空間探索と最適化の課題に対処できるかどうかを検討する。
  論文  参考訳（メタデータ） (2025-03-17T01:21:39Z)
• Reference Trustable Decoding: A Training-Free Augmentation Paradigm for Large Language Models [79.41139393080736]
  大規模言語モデル(LLM)は急速に進歩し、印象的な機能を示している。 In-Context Learning (ICL) など。 効率的なファインチューニング(PEFT)は、現在2つの主要な拡張方法である。 下流タスクへのLLM。 我々は、モデルが微調整なしで新しいタスクに迅速に適応できるパラダイムである参照信頼復号(RTD)を提案する。
  論文  参考訳（メタデータ） (2024-09-30T10:48:20Z)
• AIvril: AI-Driven RTL Generation With Verification In-The-Loop [0.7831852829409273]
  LLM(Large Language Models)は、複雑な自然言語処理タスクを実行できる計算モデルである。 本稿では,RTL対応LLMの精度と信頼性を高めるためのフレームワークであるAIvrilを紹介する。
  論文  参考訳（メタデータ） (2024-09-03T15:07:11Z)

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

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