Petri Nets Validating DRAM Protocols. Innovation in Verification

A Petri nets blog scored highest in engagement last year. This month we review application of the technique to validating an expanding range of JEDEC memory standards. Paul Cunningham (Senior VP/GM, Verification at Cadence), Raúl Camposano (Silicon Catalyst, entrepreneur, former Synopsys CTO and now Silvaco CTO) and I continue our series on research ideas. As always, feedback welcome.

The Innovation

This month’s pick is Fast validation of DRAM protocols with timed petri nets. The authors presented the paper at the 2019 MEMSYS conference and are from Fraunhofer and TU Kaiserslautern in Germany.

JEDEC standards for memory protocols describe the complexities of command behaviors and timing through a mix of state machine diagrams, tables, and timing diagrams. Validating an implementation through simulation depends on creating meaningful tests and checks through manual comparison with the standard doc. JEDEC themselves acknowledge that their reference based on a combination of FSMs, tables and timing diagrams is not fully complete and makes automated test generation problematic. This paper uses Timed Petri Nets to provide a full model of the DRAM states, the logical command dependencies and the internal timing dependencies of the system under test, from which a complete SystemC reference model can be automatically generated and used as a reference with popular DRAM simulators for verification.

In addition to the value of the ideas, this paper provides a useful intro to the mechanics of DRAM operation for novices like me!

Paul’s view

This is an easy to read, self-contained paper, providing a great example of the opportunity for domain specific languages in design and verification. In this paper the authors tackle the problem of verifying DDR interfaces. They build on prior art describing the DDR3 protocol using a Petri Net, a wonderful graph-based notation for visually representing interactions between concurrent state machines.

The authors’ key contribution is to upgrade this prior art to a “Timed” Petri Net containing additional arcs and annotations to model the timing dependences between commands in the DDR protocol standard. They create a nice little textual language, DRAMml, for describing these Timed Petri Nets which is able to represent the complete DDR3 command protocol on one page. Nice!

They also develop a compiler for DRAMml to generate simulatable SystemC code which can be used as a “golden” model as a reference for verification. As final icing on the cake, they use their golden model to find a bug in DRAMSys, a well cited popular DRAM simulator in the literature. I would be really interested to see if this work could be applied to other protocols such as PCIe or Ethernet.

Raúl’s view

This is the first paper on the validation of dynamic memory controllers for DDR that we have reviewed in this series. JEDEC has issued 19 standards since the original DDR in 2000, including DDR5 and HBM3. It is easy to see that the specification of such memories – with multiple banks, 2¹² to 2¹⁸ rows, where each row can store 512 B to 2 KB of data, recharge, refresh requirements – can get very complex, particularly regarding the timing requirements. As an example, the authors cite that to model the complete state space of a DDR4 with 16 banks requires 65,536 states with over a billion transitions.

To simplify and formalize memory specifications, the paper builds models using extended Petri Nets. Petri nets are bipartite graphs with places and transitions connected by weighted directed arcs (section 3.2). They are extended by:

-> [t1, t2] timed-arc with guard [t1,t2] meaning the transition can only fire in that time interval

->>            reset-arc which clears a place of all tokens

-o              inhibitor-arc which prevents a transition to fire

With such extensions Petri Nets become as powerful as Turing Machines. These Petri Nets model DRAMs with reasonable complexity, e.g. 4 places and 8 transitions, plus a place and 6 transitions per bank. Power can be modeled directly; timing gets a bit more complicated requiring also timing dependencies between transitions.

The paper then goes on to define a DSL (domain specific language) called DRAMml using the MPS Software from Jetbrains, to describe this Petri Net and convert it to SystemC. The generated executable model was simulated with several DRAM simulators, namely DRAMSim2, DRAMSys, Ramulator, and the DRAM controller in gem5, uncovering a timing violation in DRAMSys.

I found the paper interesting and easy to read given that I also worked with Petri Nets before. Following the DRAM specs in detail is more for the specialist but can be educational. The claim that “DRAMml, which describes all the timing, state and command information of the JEDEC standards in a formal, short, comprehensive, readable and understandable format” is not obvious. It requires understanding of Petri Nets, which may be a barrier to the adoption of the methodology, despite improved simplicity and expressive power. It would be interesting to know what JEDEC thinks of this approach since in principle it should allow them to provide or at least build definite reference models for new standard releases.