Skip to content

Autoformalizing Memory Specifications with Agents

🕒 Published (v1): 2026-04-30 02:01 UTC · Source: Arxiv · Venue: ICLR · link

Why this paper was selected

Agents autoformalize chip design memory specs; reduces costly design verification effort

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

This paper presents an agentic LLM pipeline that automatically converts natural-language JEDEC DRAM memory specifications into DRAMPyML, a Python-based timed Petri net formalism, enabling downstream generation of SystemVerilog assertions, stimulus, and functional coverage. The agent iteratively reads spec artifacts, writes and edits Petri net code, and runs validation tests via MCP tool calls. They also release DRAMBench, the first open benchmark for hardware autoformalization covering 12 DRAM standards.

Problem

Design verification (DV) consumes over half the chip design lifecycle. Translating natural-language JEDEC DRAM specifications—spanning hundreds of pages with timing diagrams, complex command interactions, and intricate timing constraints—into formal, executable verification models is entirely manual. Existing LLM-based SVA generation approaches only target isolated properties, are prone to syntactic and semantic errors, and cannot produce complete behavioral models or other testbench collateral (stimulus, functional coverage).

Method

The pipeline has two stages. First, command sets, timing parameters, and memory hierarchy are manually extracted from the JEDEC PDF and vendor datasheet. These are passed to an autoformalization agent operating in an interactive environment with access to: the full PDF spec, the DRAMPyML source library, optionally an example Petri net (from a prior-generation standard), and tool servers (glob, grep, bash, write) via MCP. The agent iterates—reading spec sections, generating or editing DRAMPyML code (timed Petri nets encoded as Python graphs with places, transitions, inhibitor arcs, reset arcs, and timed arcs), and running structural validation tests (well-formedness, deadlock detection, command trace cross-checking)—until the net passes all checks.

Two prompting modes are compared: agentic iterative (multi-turn tool use with feedback) and one-shot (single prompt encoding DRAMPyML conventions). Correctness of generated nets is evaluated via a conjecture (Conjecture 3.4, empirically validated on >1000 injected mutations) that checking untimed traces of length \(k \leq 4\) on configurations \((|B|=1,|R|=1)\) and \((|B|=2,|R|=1)\) is sufficient to prove full trace equivalence under DRAM symmetry conditions.

Two metrics are introduced: - Jaccard index on bounded untimed command traces: \(\text{Jacc}_k(N_\text{gen}, N_\text{gt}) = \frac{|\text{Tr}_k(N_\text{gen}) \cap \text{Tr}_k(N_\text{gt})|}{|\text{Tr}_k(N_\text{gen}) \cup \text{Tr}_k(N_\text{gt})|}\) with \(k=4\) - Timing Constraint Recall: \(\text{TCRecall} = \frac{|\text{TC}(N_\text{gen}) \cap \text{TC}(N_\text{gt})|}{|\text{TC}(N_\text{gt})|}\)

Key Contributions

  • Autoformalization agent: Iterative LLM agent with MCP tool access for generating DRAMPyML timed Petri nets from JEDEC specs, supporting DDR2/3/4/5, LPDDR2/3/4/5, GDDR5/6/7, HBM2/3.
  • DRAMBench: Open benchmark with 13 ground-truth DRAMPyML formalizations across four DRAM families, the first such dataset for hardware autoformalization.
  • Minimal configuration equivalence conjecture (Conjecture 3.4): Empirical validation (>1000 mutation tests) that \(k=4\) traces on 1- and 2-bank configurations suffice to witness all behavioral bugs, enabling tractable correctness checking without state-space explosion.
  • Evaluation metrics: Jaccard index on command traces and Timing Constraint Recall, introduced as the first metrics for this domain.

Results

  • Without any example Petri net, the agentic approach achieves near-correct results for DDR2 (Jaccard approaching 1.0) and Jaccard \(> 0.5\) even for complex standards like LPDDR5; one-shot generation fails in this regime.
  • With a cherry-picked example (adjacent generation), the agent achieves structurally perfect nets (Jaccard \(\approx 1.0\)) for HBM2, DDR2, DDR3, and DDR4.
  • One-shot Sonnet 4.5 is competitive—and occasionally outperforms the agentic method on token efficiency—for shorter specs (HBM2/3, LPDDR4, DDR4) when examples are provided.
  • DeepSeek-v3p2 surpasses GPT-5.2 on both Jaccard and timing recall in the agentic setting; Sonnet 4.5 is the strongest overall.
  • Complex modern specs (DDR5, GDDR6/7, HBM3, LPDDR5) remain hard: a representative DDR5 failure achieves Jaccard \(\approx 0.20\), timing recall \(\approx 0.15\).
  • A weak performance-vs-token scaling trend appears in the no-example regime but disappears once strong priors are provided; with examples, longer runs can degrade quality due to hallucinated tests.

Limitations

  • Command set, timing parameters, and memory hierarchy must still be manually extracted from PDF specs; the agent begins from pre-parsed inputs.
  • Performance degrades significantly on complex modern standards (DDR5, GDDR6/7, HBM3) with Jaccard scores as low as 0.20; self-refresh modes and advanced features are poorly captured.
  • Inter-run variance is substantial for agentic configurations, requiring multiple runs (three per config) and making reproducibility expensive.
  • DeepSeek and GPT-5.2 cannot be evaluated on one-shot generation for all specs due to limited context windows (\(< 10^6\) tokens).
  • Conjecture 3.4 (minimal configuration equivalence) is empirically validated but unproven; a formal proof is deferred to future work.
  • Timing arcs not modeled in ground truth (e.g., write/read latency, ODT timings) are excluded from recall computation, potentially inflating TCRecall.

Relevance to Agentic AI / LLM Agents

This paper is a concrete instantiation of an LLM agent solving a long-horizon, tool-intensive formalization task in a domain (hardware DV) where correctness is verifiable and failures are costly—making it a high-value testbed for agentic reasoning. The iterative refinement loop (read → write → execute tests → revise) mirrors the structure of software engineering agents like SWE-bench setups, but applied to a formal language (DRAMPyML/timed Petri nets) rather than general-purpose code, with structured external validation replacing test suites. The work also highlights a recurring challenge in agent evaluation: the tradeoff between token consumption and quality, and the phenomenon where extended agent runs can degrade output via hallucinated self-verification—a failure mode relevant to any agent with autonomous tool use.