Autoformalizing Memory Specifications with Agents

• URL: http://arxiv.org/abs/2605.00058v1
• Date: Thu, 30 Apr 2026 02:01:48 GMT
• Title: Autoformalizing Memory Specifications with Agents
• Abstract summary: We show how to formalize memory chip specifications into a formal representation called DRAMPyML.<n>This can be used for the generation of SystemVerilog assertions, stimulus, and functional coverage.<n>We also release our benchmarking dataset, DRAMBench, which can be used to evaluate the evolution of model capabilities.
• Score: 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.

Related papers

• SpecAlign: Efficient Specification-Grounded Alignment of Large Language Models via Synthetic Data [46.83043333985018]
  We propose specification-grounded alignment, a new alignment paradigm that treats provider-authored model specifications as the primary alignment target.<n>We introduce SpecAlign, a framework that synthesizes alignment data directly from specification documents.
  arXiv  Detail & Related papers  (2026-06-15T06:30:52Z)
• The Model Is Not the Product: A Dual-Pillar Architecture for Local-First Psychological Coaching [51.56484100374058]
  This report introduces Psych LM, an iOS application that validates the thesis that, for such applications, the surrounding architecture is paramount.<n>Psych LM runs a local, on-device language model within a purpose-built, local-first runtime designed for behavioral and life-coaching applications.
  arXiv  Detail & Related papers  (2026-05-23T05:49:11Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications [12.783777562919383]
  Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts.<n>We propose a neuro-symbolic framework for automatically generating memory-aware formal function specifications for C programs.<n>We introduce LeetCode-C-Spec, a new benchmark of 200 C programming problems for generating memory-aware formal function specifications.
  arXiv  Detail & Related papers  (2026-03-12T15:02:26Z)
• Beyond Short-Horizon: VQ-Memory for Robust Long-Horizon Manipulation in Non-Markovian Simulation Benchmarks [96.60530830276281]
  RuleSafe is a new articulated manipulation benchmark built upon a scalable LLM-aided simulation framework.<n>VQ-Memory is a compact and structured temporal representation that uses vector-quantized variational autoencoders.
  arXiv  Detail & Related papers  (2026-03-10T11:13:54Z)
• Scaling LLM Speculative Decoding: Non-Autoregressive Forecasting in Large-Batch Scenarios [76.85739138203014]
  We present SpecFormer, a novel architecture that accelerates unidirectional and attention mechanisms.<n>We demonstrate that SpecFormer achieves lower training demands and reduced computational costs.
  arXiv  Detail & Related papers  (2025-11-25T14:20:08Z)
• QiMeng-CRUX: Narrowing the Gap between Natural Language and Verilog via Core Refined Understanding eXpression [48.84841760215598]
  Large language models (LLMs) have shown promising capabilities in hardware description language (HDL) generation.<n>Existing approaches often rely on free-form natural language descriptions that are often ambiguous, redundant, and unstructured.<n>We treat hardware code generation as a complex transformation from an open-ended natural language space to a domain-specific, highly constrained target space.<n>We introduce Core Refined Understanding eXpression (CRUX), a structured intermediate space that captures the essential semantics of user intent while organizing the expression for precise Verilog code generation.
  arXiv  Detail & Related papers  (2025-11-25T09:17:32Z)
• Preguss: It Analyzes, It Specifies, It Verifies [14.717270519465218]
  Large language models (LLMs) have recently demonstrated their potential for enhancing the degree of automation in formal verification.<n>This paper outlines Preguss - a modular, fine-grained framework for automating the generation and refinement of formal specifications.
  arXiv  Detail & Related papers  (2025-08-20T08:40:22Z)
• VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification [28.196015311346024]
  This paper introduces VeriThoughts, a novel dataset designed for reasoning-based Verilog code generation.<n>We establish a new benchmark framework grounded in formal verification methods to evaluate the quality and correctness of generated hardware descriptions.<n>We present a suite of specialized small-scale models optimized specifically for Verilog generation.
  arXiv  Detail & Related papers  (2025-05-16T21:33:14Z)
• Quantifying Memory Utilization with Effective State-Size [73.52115209375343]
  We develop a measure of textitmemory utilization'<n>This metric is tailored to the fundamental class of systems with textitinput-invariant and textitinput-varying linear operators
  arXiv  Detail & Related papers  (2025-04-28T08:12:30Z)
• Steering Masked Discrete Diffusion Models via Discrete Denoising Posterior Prediction [88.65168366064061]
  We introduce Discrete Denoising Posterior Prediction (DDPP), a novel framework that casts the task of steering pre-trained MDMs as a problem of probabilistic inference. Our framework leads to a family of three novel objectives that are all simulation-free, and thus scalable. We substantiate our designs via wet-lab validation, where we observe transient expression of reward-optimized protein sequences.
  arXiv  Detail & Related papers  (2024-10-10T17:18:30Z)
• HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction [2.977255700811213]
  Hardware-firmware co-verification is critical to design trustworthy systems. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification.
  arXiv  Detail & Related papers  (2023-09-14T19:24:57Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.