DRAMPyML: A Formal Description of DRAM Protocols with Timed Petri Nets

TL;DR

DRAMPyML presents a Python-based Timed-Inhibitor-Reset Petri net framework to formalize JEDEC DRAM protocols, capturing both functional behavior and intricate timing dependencies. By making the model executable, the authors enable verification of memory controllers and DRAM logic, and they demonstrate generation of DRAMSys-compatible code and verification artifacts from the Petri-net description. Key innovations include timing-arc integration for complex command-to-command constraints and a scalable, hierarchical representation that remains adaptable to standards such as DDR, LPDDR, and HBM. The work aims to standardize DRAM protocol expression, facilitate thorough verification, and streamline code-generation workflows for DRAM controllers and memory simulators, with open-source release planned.

Abstract

The JEDEC committee defines various domain-specific DRAM standards. These standards feature increasingly complex and evolving protocol specifications, which are detailed in timing diagrams and command tables. Understanding these protocols is becoming progressively challenging as new features and complex device hierarchies are difficult to comprehend without an expressive model. While each JEDEC standard features a simplified state machine, this state machine fails to reflect the parallel operation of memory banks. In this paper, we present an evolved modeling approach based on timed Petri nets and Python. This model provides a more accurate representation of DRAM protocols, making them easier to understand and directly executable, which enables the evaluation of interesting metrics and the verification of controller RTL models, DRAM logic and memory simulators.

Figures (11)

• Figure 1: JEDEC standard releases over time junkra_19.
• Figure 2: Petri net example according to mur_89.
• Figure 3: Petri net model of a single bank.
• Figure 4: Simplified DRAM Petri nets.
• Figure 5: Definition of the general Petri net graph structure.