論文の概要: FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols

• arxiv url: http://arxiv.org/abs/2504.17226v1
• Date: Thu, 24 Apr 2025 03:34:37 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-02 19:15:53.237512
• Title: FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols
• Title（参考訳）: FLAG:オンチップ通信プロトコルの形式仕様のための形式およびLCM支援SVA生成
• Authors: Yu-An Shih, Annie Lin, Aarti Gupta, Sharad Malik,
• Abstract要約: オンチップ通信プロトコルの正式な仕様は、システムオンチップ(SoC)の設計と検証に不可欠である。 非公式な文書から正式なプロトコル仕様を構築するための2段階のフレームワークであるFLAGを提案する。
• 参考スコア（独自算出の注目度）: 2.242458166492809
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal specifications of on-chip communication protocols are crucial for system-on-chip (SoC) design and verification. However, manually constructing these formal specifications from informal documents remains a tedious and error-prone task. Although recent efforts have used Large Language Models (LLMs) to generate SystemVerilog Assertion (SVA) properties from design documents for Register-Transfer Level (RTL) design verification, in our experience these approaches have not shown promise in generating SVA properties for communication protocols. Since protocol specification documents are unstructured and ambiguous in nature, LLMs often fail to extract the necessary information and end up generating irrelevant or even incorrect properties. We propose FLAG, a two-stage framework to help construct formal protocol specifications from informal documents. In the first stage, a predefined template set is used to generate candidate SVA properties. To avoid missing necessary properties, we develop a grammar-based approach to generate comprehensive template sets that capture critical signal behaviors for various communication protocols. In the second stage, we utilize unambiguous timing diagrams in conjunction with textual descriptions from the specification documents to filter out incorrect properties. A formal approach is first implemented to check the candidate properties and filter out those inconsistent with the timing diagrams. An LLM is then consulted to further remove incorrect properties with respect to the textual description, obtaining the final property set. Experiments on various open-source communication protocols demonstrate the effectiveness of FLAG in generating SVA properties from informal documents.
• Abstract（参考訳）: オンチップ通信プロトコルの正式な仕様は、システムオンチップ(SoC)の設計と検証に不可欠である。 しかし、これらの形式仕様を非公式な文書から手作業で構築することは、面倒でエラーを起こしやすい作業である。 近年,登録-転送レベル (RTL) 設計検証のための設計文書からシステムVerilog Assertion (SVA) プロパティを生成するために,LLM (Large Language Models) を使用してきたが,我々の経験では,これらのアプローチは通信プロトコルのSVA プロパティを生成する上で有望なものではない。 プロトコル仕様文書は本質的には構造化されておらず曖昧であるため、LCMは必要な情報を抽出し、不適切なプロパティや不正なプロパティを生成するのに失敗することが多い。 非公式な文書から正式なプロトコル仕様を構築するための2段階のフレームワークであるFLAGを提案する。 最初の段階では、事前定義されたテンプレートセットを使用して候補SVAプロパティを生成する。 必要な特性の欠如を避けるため,様々な通信プロトコルにおいて重要な信号の振る舞いをキャプチャする包括的テンプレートセットを生成する文法ベースの手法を開発した。 第2段階では、仕様文書からのテキスト記述とあいまいなタイミング図を用いて、不正なプロパティをフィルタリングする。 形式的なアプローチが最初に実装され、候補プロパティをチェックし、タイミング図と矛盾するプロパティをフィルタリングする。 LLMは、テキスト記述に関してさらに不正なプロパティを削除し、最終的なプロパティセットを取得するために相談される。 各種オープンソース通信プロトコルの実験は、非公式文書からSVA特性を生成するためのFLAGの有効性を示した。

関連論文リスト

• Validating Network Protocol Parsers with Traceable RFC Document Interpretation [11.081773172066766]
  オラクルとトレーサビリティの問題は、プロトコルの実装がいつバグがあると考えられるかを決定する。 この研究はどちらも考慮し、大規模言語モデル(LLM)の最近の進歩を利用した効果的なソリューションを提供する。 我々は、C、Python、Goで書かれた9つのネットワークプロトコルとその実装を使用して、我々のアプローチを広く評価してきた。
  論文  参考訳（メタデータ） (2025-04-25T03:39:19Z)
• AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL [6.062811197376495]
  本稿では,仕様とRTLの両方から知識グラフ(KG)を構築する新しい手法を提案する。 仕様から初期KGを作成し、RTLコードから抽出された情報と体系的に融合し、統合された総合KGとなる。 4つの設計実験により,提案手法は従来手法よりもSVAの品質を著しく向上させることが示された。
  論文  参考訳（メタデータ） (2025-03-24T21:53:37Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [91.981439746404]
  本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。 まず,人間のアノテーションに対するQASemConsistency法の有効性を示す。 そこで我々は,局所的な事実の不整合を自動的に検出するいくつかの手法を実装した。
  論文  参考訳（メタデータ） (2024-10-09T22:53:48Z)
• Object-Attribute Binding in Text-to-Image Generation: Evaluation and Control [58.37323932401379]
  現在の拡散モデルは、入力としてテキストプロンプトが与えられたイメージを生成するが、テキストで言及されている属性を画像の正しいオブジェクトに正しく結び付けるのに苦労する。 入力文中の構文的制約により視覚的注意マップを制御できる集中的横断注意(FCA)を提案する。 我々は、T2I生成の大幅な改善、特にいくつかのデータセットに対する属性オブジェクトのバインディングを示す。
  論文  参考訳（メタデータ） (2024-04-21T20:26:46Z)
• Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach [3.9155346446573502]
  本稿では,5GおよびNextGプロトコル(AVRE)のための実世界プロンプトを用いた形式検証の自動モデリングを提案する。 AVREは次世代通信プロトコル(NextG)の正式な検証のために設計された新しいシステムである。
  論文  参考訳（メタデータ） (2023-12-28T20:41:24Z)
• Validation of Rigorous Requirements Specifications and Document Automation with the ITLingo RSL Language [0.0]
  ITLingoイニシアチブは、技術的文書の厳密さと一貫性を高めるためにRSLという要求仕様言語を導入した。 本稿では、要求検証と文書自動化の分野における既存の研究・ツールについてレビューする。 我々は、カスタマイズされたチェックと、RSL自体で動的に定義された言語規則に基づいて、仕様の検証によりRSLを拡張することを提案する。
  論文  参考訳（メタデータ） (2023-12-17T21:39:26Z)
• FLIP: Fine-grained Alignment between ID-based Models and Pretrained Language Models for CTR Prediction [49.510163437116645]
  クリックスルーレート(CTR)予測は、パーソナライズされたオンラインサービスにおいてコア機能モジュールとして機能する。 CTR予測のための従来のIDベースのモデルは、表形式の1ホットエンコードされたID特徴を入力として取る。 事前訓練された言語モデル(PLM)は、テキストのモダリティの文を入力として取る別のパラダイムを生み出した。 本稿では,CTR予測のためのIDベースモデルと事前学習言語モデル(FLIP)間の細粒度特徴レベルのアライメントを提案する。
  論文  参考訳（メタデータ） (2023-10-30T11:25:03Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。 本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。 その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
  論文  参考訳（メタデータ） (2023-10-19T15:40:00Z)
• Towards Formal Verification of a TPM Software Stack [0.5074812070492739]
  本稿では,Frama-C 検証プラットフォームを用いた tpm2-ts の形式的検証について述べる。 リンクされたリストと複雑なデータ構造に基づいて、ライブラリのコードは検証ツールにとって非常に難しいように思える。
  論文  参考訳（メタデータ） (2023-07-31T16:35:16Z)
• MetricPrompt: Prompting Model as a Relevance Metric for Few-shot Text Classification [65.51149771074944]
  MetricPromptは、数発のテキスト分類タスクをテキストペア関連性推定タスクに書き換えることで、言語設計の難易度を緩和する。 広範に使われている3つのテキスト分類データセットを4つのショット・セッティングで実験する。 結果から,MetricPromptは,手動弁証法や自動弁証法よりも優れた性能を示した。
  論文  参考訳（メタデータ） (2023-06-15T06:51:35Z)
• Unified Pretraining Framework for Document Understanding [52.224359498792836]
  文書理解のための統合事前学習フレームワークであるUDocを紹介する。 UDocは、ほとんどのドキュメント理解タスクをサポートするように設計されており、Transformerを拡張してマルチモーダル埋め込みを入力とする。 UDocの重要な特徴は、3つの自己管理的損失を利用して汎用的な表現を学ぶことである。
  論文  参考訳（メタデータ） (2022-04-22T21:47:04Z)
• SPECTER: Document-level Representation Learning using Citation-informed Transformers [51.048515757909215]
  SPECTERは、Transformer言語モデルの事前学習に基づいて、科学文書の文書レベルの埋め込みを生成する。 SciDocsは、引用予測から文書分類、レコメンデーションまでの7つの文書レベルのタスクからなる新しい評価ベンチマークである。
  論文  参考訳（メタデータ） (2020-04-15T16:05:51Z)

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

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