論文の概要: Autoformalizing Memory Specifications with Agents

• arxiv url: http://arxiv.org/abs/2605.00058v1
• Date: Thu, 30 Apr 2026 02:01:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-04 17:43:28.659088
• Title: Autoformalizing Memory Specifications with Agents
• Title（参考訳）: エージェントによるメモリ仕様の自動生成
• Authors: Jan Ole Ernst, Dmitri Michelangelo Saberi, Derek Christ, Thomas Zimmermann, Rajath Salegame, Suhaas M. Bhat, Stanislav Levental, Thomas Dybdahl Ahle, Matthias Jung,
• Abstract要約: 本稿では,メモリチップ仕様をDRAMPyMLという形式表現にする方法を示す。 これはSystemVerilogアサーション、刺激、機能カバレッジの生成に使用できる。 ベンチマークデータセットであるDRAMBenchもリリースしています。
• 参考スコア（独自算出の注目度）: 3.897906533095668
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The primary goal of Design Verification (DV) is to ensure that a proposed chip design implementation (either in code, or physical form) exactly matches its specification and is free of functional errors in order to avoid costly re-designs. Achieving this often demands extensive manual interpretation, translating the specification document into a formal, testable representation. While AI has made progress in DV, current approaches typically focus on narrow, isolated tasks rather than full end-to-end specification compliance of modern chip designs, failing to capture the complexity of real-world verification. Our method automatically formalizes natural language memory chip specifications, for industry relevant Dynamic Random Access Memory (DRAM) standards, into a formal representation called DRAMPyML that can be used for downstream DV tasks like the generation of SystemVerilog assertions, stimulus, and functional coverage. We also release our benchmarking dataset, DRAMBench, which can be used to evaluate the evolution of model capabilities (and new approaches) at hardware autoformalization.
• Abstract（参考訳）: 設計検証(DV)の第一の目的は、提案されたチップ設計実装(コードまたは物理形式)が仕様と正確に一致し、コストのかかる再設計を避けるために機能的エラーがないことを保証することである。 これを達成するためには、仕様文書を形式的でテスト可能な表現に変換する、広範囲な手作業による解釈が必要となることが多い。 AIはDVで進歩しているが、現在のアプローチは一般的に、現代のチップ設計の完全なエンドツーエンドの仕様準拠ではなく、狭く孤立したタスクに重点を置いており、現実の検証の複雑さを捉えていない。 本手法は,動的ランダムアクセスメモリ(DRAM)規格の自然言語メモリチップ仕様を自動的に形式化し,システムVerilogアサーション,刺激,機能カバレッジの生成など,下流DVタスクに使用可能なDRAMPyMLという形式表現に変換する。 ベンチマークデータセットであるDRAMBenchもリリースしています。これは、ハードウェアの自動形式化におけるモデル機能(および新しいアプローチ)の進化を評価するために使用できます。

関連論文リスト

• Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications [12.783777562919383]
  メモリ操作プログラムの形式的検証は、専門家によって書かれたメモリ状態をキャプチャする正確な機能仕様に依存している。 本稿では,Cプログラムのメモリ対応形式関数仕様を自動生成するニューロシンボリックフレームワークを提案する。 我々は,メモリ対応の形式関数仕様を生成するための200Cプログラミング問題のベンチマークであるLeetCode-C-Specを紹介する。
  論文  参考訳（メタデータ） (2026-03-12T15:02:26Z)
• Beyond Short-Horizon: VQ-Memory for Robust Long-Horizon Manipulation in Non-Markovian Simulation Benchmarks [96.60530830276281]
  RuleSafeは、スケーラブルなLLM支援シミュレーションフレームワーク上に構築された、新しいオペレーティングベンチマークである。 VQ-Memoryはベクトル量子化変分オートエンコーダを用いたコンパクトで構造化された時間表現である。
  論文  参考訳（メタデータ） (2026-03-10T11:13:54Z)
• Scaling LLM Speculative Decoding: Non-Autoregressive Forecasting in Large-Batch Scenarios [76.85739138203014]
  本稿では,一方向および注目メカニズムを加速する新しいアーキテクチャであるSpecFormerを紹介する。 また,SpecFormerはトレーニング要求の低減と計算コストの削減を実現している。
  論文  参考訳（メタデータ） (2025-11-25T14:20:08Z)
• QiMeng-CRUX: Narrowing the Gap between Natural Language and Verilog via Core Refined Understanding eXpression [48.84841760215598]
  大規模言語モデル(LLM)はハードウェア記述言語(HDL)生成において有望な能力を示している。 既存のアプローチは、しばしば曖昧で冗長で構造化されていない自由形式の自然言語記述に依存している。 我々は、ハードウェアコード生成を、オープンな自然言語空間からドメイン固有の高度に制約されたターゲット空間への複雑な変換として扱う。 構造化された中間空間であるCore Refined Understanding eXpression (CRUX)を導入し、ユーザの意図の本質的な意味を捉えながら、正確なVerilogコード生成のための式を整理する。
  論文  参考訳（メタデータ） (2025-11-25T09:17:32Z)
• VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification [28.196015311346024]
  本稿では、推論に基づくVerilogコード生成用に設計された新しいデータセットであるVeriThoughtsを紹介する。 我々は,生成したハードウェア記述の品質と正確性を評価するために,形式的検証手法に基づく新しいベンチマークフレームワークを構築した。 We present a suite of small-scale model based for Verilog generation。
  論文  参考訳（メタデータ） (2025-05-16T21:33:14Z)
• Quantifying Memory Utilization with Effective State-Size [73.52115209375343]
  「我々は、テキスト・メモリ利用の尺度を策定する。」 この計量は、textitinput-invariant および textitinput-variant linear operator を持つシステムの基本的なクラスに適合する。
  論文  参考訳（メタデータ） (2025-04-28T08:12:30Z)
• Steering Masked Discrete Diffusion Models via Discrete Denoising Posterior Prediction [88.65168366064061]
  本稿では,確率論的推論の課題として,事前学習したMDMを操る作業を行う新しいフレームワークであるDDPPを紹介する。 私たちのフレームワークは、3つの新しい目標のファミリーにつながります。 Wet-lab Validation(ウェット・ラブ・バリデーション)を用いて,報酬最適化タンパク質配列の過渡的発現を観察する。
  論文  参考訳（メタデータ） (2024-10-10T17:18:30Z)
• HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction [2.977255700811213]
  ハードウェア確認ソフトの共検証は、信頼できるシステムの設計に不可欠である。 ハードウェアを手動で抽象化したり、ヒントを手動で生成することで、ファームウェア検証中の状態空間を削減できる有望な方法がある。 本稿では,シミュレーションに基づく検証のスケーラビリティと形式検証の完全性とを効果的に組み合わせる。
  論文  参考訳（メタデータ） (2023-09-14T19:24:57Z)

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

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