Autoformalizing Memory Specifications with Agents

TL;DR

This paper presents an automated method to formalize natural language DRAM specifications into a formal representation, aiding design verification and providing a benchmark dataset for evaluating such models.

Contribution

The authors introduce DRAMPyML, a formal language for DRAM specs, and release DRAMBench, a dataset for evaluating hardware autoformalization models.

Findings

Successfully formalized industry-relevant DRAM specifications.

Generated SystemVerilog assertions, stimulus, and coverage from formalized specs.

Provided a benchmark dataset for future model evaluation.

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.