{"id":15383,"date":"2026-04-24T12:45:21","date_gmt":"2026-04-24T10:45:21","guid":{"rendered":"https:\/\/www.iese.fraunhofer.de\/blog\/?p=15383"},"modified":"2026-04-27T09:58:51","modified_gmt":"2026-04-27T07:58:51","slug":"drambench-autoformalizing-dram-specifications","status":"publish","type":"post","link":"https:\/\/www.iese.fraunhofer.de\/blog\/drambench-autoformalizing-dram-specifications\/","title":{"rendered":"DRAMBench: Autoformalizing DRAM Specifications with Timed Petri Nets"},"content":{"rendered":"

Chip design verification is dominated by manual interpretation of complex DRAM standards. With DRAMPyML and DRAMBench, Fraunhofer IESE and Normal Computing introduce timed Petri net models and an open benchmark to autoformalize memory specifications. This post shows how AI can bridge the gap between natural language specs and formal verification artifacts.<\/p>\n

\n

\"Jan
\nCo-Author<\/strong>
\nDr. Jan Ole Ernst<\/p>\n

Send email<\/a><\/p>\n

 <\/p>\n

Dr. Jan Ole Ernst is a Research Scientist at Normal Computing with a background in physics and machine learning. Currently, he works on AI for chip design & verification and novel computing architectures.<\/p>\n<\/div>\n

Chip design verification is one of the most critical and labor-intensive steps in the semiconductor industry, estimated to take up to 70% of the verification effort. Before a chip can be manufactured, engineers must ensure that the design implementation exactly matches its specification and is free of functional errors – because a bug found after fabrication can mean months of delay and millions for costly respins. Today, this verification process demands extensive manual effort: engineers read through hundreds of pages of natural language specifications and painstakingly translate them into formal, testable representations, a process that is slow, error-prone, and does not scale well as specifications grow in complexity. At Fraunhofer IESE, together with Normal Computing, we believe that AI and formal methods can fundamentally change this situation. To help make this vision concrete, we are releasing DRAMBench \u2013 an open benchmark and formal modelling framework for memory chips \u2013 as well as DRAMPyML, our Python-based framework for timed Petri net models of DRAM protocols.<\/p>\n

The Problem: Specifications Are Written for Humans, Not Machines<\/h2>\n

Industry standards bodies like JEDEC publish detailed specifications for memory chips such as DDR, LPDDR, GDDR, and HBM. These documents define how such chips work: which commands a memory chip must support, the legal orderings of those commands, and the precise timing constraints between them. A single DRAM standard can contain hundreds of timing parameters and complex state-dependent rules governing how commands interact across banks, ranks, and channels.
\nToday, translating these specifications into something a verification tool can consume is almost entirely manual. Verification engineers read the spec, interpret its intent, and encode it into SystemVerilog assertions, stimulus sequences and other artifacts. This translation step is where spec misinterpretations enter the design and where schedules tend to slip. While AI has made progress in isolated design verification tasks, current approaches typically focus on narrow problems rather than full end-to-end specification compliance of modern chip designs, failing to capture the complexity of real-world verification workflows.<\/p>\n

Our Approach: Timed Petri Nets as a Formal Target<\/h2>\n

Rather than jumping directly from natural language to low-level verification artifacts, we introduce an intermediate formal representation based on timed Petri nets. Petri nets are a well-established mathematical formalism for modeling concurrent systems – they capture states, transitions, and the constraints governing when transitions may fire. By extending them with timing, we can faithfully represent the temporal requirements that are central to DRAM protocols.<\/p>\n

Our framework, DRAMPyML, models each DRAM standard as a timed Petri net where:<\/p>\n