論文の概要: Using LLMs to Facilitate Formal Verification of RTL
- arxiv url: http://arxiv.org/abs/2309.09437v2
- Date: Thu, 28 Sep 2023 15:27:39 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-23 07:31:06.403437
- Title: Using LLMs to Facilitate Formal Verification of RTL
- Title（参考訳）: LLMを用いたRTLの形式的検証
- Authors: Marcelo Orenes-Vera, Margaret Martonosi and David Wentzlaff
- Abstract要約: GPT4 は設計ミスを反映することなく, 欠陥のある RTL に対しても正しい SVA を生成することができることを示す。
我々は、改良されたGPT4ベースのフローを統合して安全性特性を生成することにより、オープンソースのAutoSVAフレームワークを拡張した。
- 参考スコア（独自算出の注目度）: 7.45362896000302
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal property verification (FPV) has existed for decades and has been shown
to be effective at finding intricate RTL bugs. However, formal properties, such
as those written as SystemVerilog Assertions (SVA), are time-consuming and
error-prone to write, even for experienced users. Prior work has attempted to
lighten this burden by raising the abstraction level so that SVA is generated
from high-level specifications. However, this does not eliminate the manual
effort of reasoning and writing about the detailed hardware behavior. Motivated
by the increased need for FPV in the era of heterogeneous hardware and the
advances in large language models (LLMs), we set out to explore whether LLMs
can capture RTL behavior and generate correct SVA properties.
First, we design an FPV-based evaluation framework that measures the
correctness and completeness of SVA. Then, we evaluate GPT4 iteratively to
craft the set of syntax and semantic rules needed to prompt it toward creating
better SVA. We extend the open-source AutoSVA framework by integrating our
improved GPT4-based flow to generate safety properties, in addition to
facilitating their existing flow for liveness properties. Lastly, our use cases
evaluate (1) the FPV coverage of GPT4-generated SVA on complex open-source RTL
and (2) using generated SVA to prompt GPT4 to create RTL from scratch.
Through these experiments, we find that GPT4 can generate correct SVA even
for flawed RTL, without mirroring design errors. Particularly, it generated SVA
that exposed a bug in the RISC-V CVA6 core that eluded the prior work's
evaluation.
- Abstract（参考訳）: 形式的特性検証(FPV)は数十年前から存在し、複雑なRTLバグを見つけるのに有効であることが示されている。
しかし、systemverilog asserts(sva)のような形式的プロパティは、経験豊富なユーザでさえ、記述に時間がかかるし、エラーもやすい。
以前の作業では、SVAが高レベル仕様から生成されるように抽象化レベルを上げることで、この負担を緩和しようと試みていた。
しかし、これはハードウェアの詳細な振る舞いを推論して記述する手作業を排除するものではない。
ヘテロジニアスハードウェア時代におけるFPVの必要性の高まりと大規模言語モデル(LLM)の進歩により、LLMがRTLの挙動を捉え、正しいSVA特性を生成できるかどうかを探究した。
まず、SVAの正しさと完全性を測定するFPVに基づく評価フレームワークを設計する。
そして、GPT4を反復的に評価し、より優れたSVAを作成するのに必要な構文とセマンティックルールのセットを作成する。
当社は、改良したgpt4ベースのフローを統合して安全性特性を生成し、既存のライブネスプロパティのフローを容易にすることで、オープンソースのautosvaフレームワークを拡張します。
最後に,1) 複雑なオープンソースRTL上での GPT4 生成 SVA の FPV カバレッジ,(2) 生成された SVA を用いて GPT4 をスクラッチから生成する。
これらの実験により, GPT4 は設計誤差を反映することなく, 欠陥のある RTL に対しても正しい SVA を生成することができることがわかった。
特に、SVAはRISC-V CVA6コアのバグを露呈し、以前の作業の評価を損なっていた。
関連論文リスト
- 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) - FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware [4.480157114854711]
FVEvalは,形式的検証(FV)に関わるタスクにおいて,大規模言語モデル(LLM)のパフォーマンスを特徴付ける最初の総合ベンチマークである。
ベンチマークは3つのサブタスクで構成され、異なるレベルでLLM能力を測定する。
本稿では,FVに整合した合成例を生成するための,専門家による検証手法と手法のコレクションについて述べる。
論文 参考訳（メタデータ） (2024-10-15T21:48:57Z) - OVLW-DETR: Open-Vocabulary Light-Weighted Detection Transformer [63.141027246418]
本稿では,OVLW-DETR(Open-Vocabulary Light-Weighted Detection Transformer)を提案する。
本稿では,視覚言語モデル(VLM)からオブジェクト検出器への知識伝達を簡易なアライメントで行うエンド・ツー・エンドのトレーニングレシピを提案する。
実験により,提案手法は標準ゼロショットLVISベンチマークにおいて,既存の実時間開語彙検出器よりも優れていることが示された。
論文 参考訳（メタデータ） (2024-07-15T12:15:27Z) - Can Feedback Enhance Semantic Grounding in Large Vision-Language Models? [61.899791071654654]
本稿では,視覚言語モデル(VLM)が,フィードバックの「受信」によって意味的接地を改善することができるかどうかを検討する。
適切に刺激すれば、VLMは1ステップと反復の両方でフィードバックを活用できる。
検討したすべての設定において、すべてのモデルにまたがる自動フィードバックを用いて、基底精度を一貫して改善することを示す。
論文 参考訳（メタデータ） (2024-04-09T17:59:04Z) - Test-Time Model Adaptation with Only Forward Passes [68.11784295706995]
テストタイム適応は、トレーニング済みのモデルを、潜在的に分布シフトのある未確認テストサンプルに適応させるのに有効であることが証明されている。
テスト時間フォワード最適化適応法(FOA)を提案する。
FOAは量子化された8ビットのViTで動作し、32ビットのViTで勾配ベースのTENTより優れ、ImageNet-Cで最大24倍のメモリ削減を実現する。
論文 参考訳（メタデータ） (2024-04-02T05:34:33Z) - A Critical Evaluation of AI Feedback for Aligning Large Language Models [60.42291111149438]
教師が既存のRLAIFパイプラインより優れていることを示す。
より一般的には、RLAIFの利得は、ベースモデルファミリ、テスト時間評価プロトコル、批判モデルによって大きく異なることが分かる。
論文 参考訳（メタデータ） (2024-02-19T18:53:54Z) - 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) - Silkie: Preference Distillation for Large Visual Language Models [56.10697821410489]
本稿では,大型視覚言語モデル(LVLM)の嗜好蒸留について検討する。
まず,AIアノテーションを用いた視覚言語フィードバックデータセットを構築した。
我々は, GPT-4V を用いて, 有用性, 視覚的忠実性, 倫理的考察のアウトプットを評価する。
結果として得られたモデルSilkieは、認知能力と認知能力に関するMMEベンチマークで6.9%と9.5%の相対的な改善を達成している。
論文 参考訳（メタデータ） (2023-12-17T09:44:27Z) - GPT-4V-AD: Exploring Grounding Potential of VQA-oriented GPT-4V for Zero-shot Anomaly Detection [51.43589678946244]
本稿では、一般的な視覚異常検出(AD)タスクにおけるVQA指向のGPT-4Vの可能性について検討する。
MVTec ADとVisAデータセットで定性的かつ定量的な評価を行ったのは、これが初めてである。
論文 参考訳（メタデータ） (2023-11-05T10:01:18Z) - LLM4DV: Using Large Language Models for Hardware Test Stimuli Generation [5.905138464855556]
本稿では,大規模言語モデル(LLM)からテスト刺激を抽出するための新しいベンチマークフレームワークを提案する。
LLM4DVと従来の制約ランダムテスト(CRT)を3つのDUTモジュールを用いて比較する。
LLM4DVは、基本的な数学的推論と事前学習された知識を活用する能力を利用して、単純なDUTシナリオを効率的に処理できることを実証した。
論文 参考訳（メタデータ） (2023-10-06T19:02:04Z) - AutoWeka4MCPS-AVATAR: Accelerating Automated Machine Learning Pipeline
Composition and Optimisation [13.116806430326513]
本稿では,サロゲートモデル(AVATAR)を用いて,実行せずにMLパイプラインの有効性を評価する手法を提案する。
AVATARは、データセットの特徴に対するMLアルゴリズムの機能と効果を自動的に学習することで、知識ベースを生成する。
AVATARはその妥当性を評価するためにオリジナルのMLパイプラインを実行する代わりに、MLパイプラインコンポーネントの機能と効果によって構築されたサロゲートモデルを評価する。
論文 参考訳（メタデータ） (2020-11-21T14:05:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。