Autoformalizing Memory Specifications with Agents
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
LTL Verification of Memoryful Neural Agents
We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications. In MN-MAS, agents interact with a non-deterministic, partially observable enviro…
State Space ModelsAutoformalizing Euclidean Geometry
Autoformalization involves automatically translating informal math into formal theorems and proofs that are machine-verifiable. Euclidean geometry provides an interesting and controllable domain for studying autoformaliz…
MathAutoformalizing and Simulating Game-Theoretic Scenarios using LLM-augmented Agents
Game-theoretic simulations are a versatile tool for exploring interactions of both natural and artificial agents. However, modelling real-world scenarios and developing simulations often require substantial human experti…
Distributed Differentially Private Control Synthesis for Multi-Agent Systems with Metric Temporal Logic Specifications
In this paper, we propose a distributed differentially private receding horizon control (RHC) approach for multi-agent systems (MAS) with metric temporal logic (MTL) specifications. In the MAS considered in this paper, e…
Formalizing Mathematics at Scale
We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped with formal verification tools, dependen…