Autoformalizing Memory Device 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 \textit{DRAMPyML} that can be used for downstream DV tasks like the generation of SystemVerilog assertions, stimulus, and functional coverage. We also release a benchmarking evaluation harness which can be used to evaluate the evolution of model capabilities (and new approaches) at hardware autoformalization.