## A Framework for Formal Verification of DRAM Controllers
## Lukas Steiner
Microelectronic Systems Design Research Group, TU Kaiserslautern Kaiserslautern, Germany lsteiner@eit.uni-kl.de
## Chirag Sudarshan
Microelectronic Systems Design Research Group, TU Kaiserslautern Kaiserslautern, Germany sudarshan@eit.uni-kl.de
## Dominik Stoffel
Chair of Electronic Design Automation, TU Kaiserslautern Kaiserslautern, Germany stoffel@eit.uni-kl.de
## Matthias Jung
Fraunhofer Institute for Experimental Software Engineering (IESE) Kaiserslautern, Germany matthias.jung@iese.fraunhofer.de
## Norbert Wehn
Microelectronic Systems Design Research Group, TU Kaiserslautern Kaiserslautern, Germany wehn@eit.uni-kl.de
Figure 1: JEDEC Standard Releases Over Time [5]
<details>
<summary>Image 1 Details</summary>
### Visual Description
## Memory Technology Timeline
### Overview
The image is a timeline illustrating the introduction of various memory technologies from approximately 2000 to 2020. The timeline displays different types of memory, including DDR, GDDR, LPDDR, Wide I/O, and HBM, showing their approximate release years.
### Components/Axes
* **X-axis:** Represents time, spanning from 2000 to 2020, with tick marks at 1-year intervals.
* **Y-axis:** Represents different memory technologies. The technologies are vertically arranged, with HBM at the top and DDR at the bottom.
* **Memory Technologies:**
* DDR (Dark Blue)
* GDDR (Orange)
* LPDDR (Yellow)
* Wide I/O (Green)
* HBM (Purple)
### Detailed Analysis
* **DDR Series (Dark Blue):**
* DDR: Appears around 2000.
* DDR2: Appears around 2003.
* DDR3: Appears around 2007.
* DDR4: Appears around 2014.
* DDR5: Appears around 2020.
* Trend: The DDR series shows a steady progression over time, with new generations appearing roughly every 3-7 years.
* **GDDR Series (Orange):**
* GDDR3: Appears around 2005.
* GDDR5: Appears around 2008.
* GDDR5X: Appears around 2015.
* GDDR6: Appears around 2017.
* Trend: The GDDR series also shows a progression, with new generations appearing at irregular intervals.
* **LPDDR Series (Yellow):**
* LPDDR: Appears around 2007.
* LPDDR2: Appears around 2009.
* LPDDR3: Appears around 2011.
* LPDDR4: Appears around 2014.
* LPDDR5: Appears around 2019.
* Trend: The LPDDR series shows a progression, with new generations appearing roughly every 2-3 years.
* **Wide I/O Series (Green):**
* Wide I/O: Appears around 2011.
* Wide I/O2: Appears around 2013.
* Trend: The Wide I/O series has only two data points on the timeline.
* **HBM Series (Purple):**
* HBM: Appears around 2014.
* HBM2: Appears around 2015.
* HBM2E: Appears around 2018.
* HBM3: Appears around 2020.
* Trend: The HBM series shows a progression, with new generations appearing roughly every 1-3 years.
### Key Observations
* The timeline provides a visual representation of the evolution of different memory technologies over time.
* Each memory technology series (DDR, GDDR, LPDDR, Wide I/O, HBM) shows a progression with new generations being introduced.
* The intervals between new generations vary across different memory technologies.
### Interpretation
The timeline illustrates the advancements in memory technology over the past two decades. It highlights the parallel development of different types of memory, each catering to specific needs and applications. The progression within each series indicates ongoing efforts to improve performance, capacity, and efficiency. The varying intervals between new generations suggest different rates of innovation and development for each technology. The presence of multiple memory types at any given time indicates that different technologies serve different purposes and markets, and that no single technology has completely replaced the others.
</details>
included new refresh commands, different burst lengths, on-die error correction and 3D-stacked devices only to mention some of the new protocol-relevant features. This is also reflected in the length of each standard (DDR3: 226 pages, DDR4: 270 pages, DDR5: 490 pages) and also projects to the other domains like HBM or LPDDR. Moreover, first working samples of DRAM-based processing-inmemory (PIM) devices have been published by Samsung and SK Hynix recently [8, 9], which require additional extensions on top of the implemented base protocol. Due to the complexity of these protocols, the verification of memory controller IPs is extremely challenging nowadays.
Even though simulation-based verification is still widely used in hardware design, it has the major drawback that it cannot prove the absence of errors, but only reveal their presence. Especially in control flow rich designs like memory controllers there is a high chance of missing some corner cases with the provided test inputs. Analternative to simulation-based verification is formal verification , which ensures the behavior of a design subject to specified properties based on mathematical proofs. This approach has also been applied to DRAM controllers in the past [1, 6]. The disadvantage of these works is that all properties have to be extracted manually from the JEDEC documents and translated manually into a property specification language (e.g., SystemVerilog Assertions (SVA)), posing a potential source of human error. In [7] this problem is addressed by transferring timing diagrams of JEDEC standards into the socalled Timing Diagram Markup Language (TDML), from which SVA code is generated automatically. Consequently, this approach is limited to those parts of the specification that are illustrated as timing diagrams. However, JEDEC standards also use tables and state machine diagrams to define the protocols. The authors of [5] have
## ABSTRACT
The large number of recent JEDEC DRAM standard releases and their increasing feature set makes it difficult for designers to rapidly upgrade the memory controller IPs to each new standard. Especially the hardware verification is challenging due to the higher protocol complexity of standards like DDR5, LPDDR5 or HBM3 in comparison with their predecessors. With traditional simulationbased verification it is laborious to guarantee the coverage of all possible states, especially for control flow rich memory controllers. This has a direct impact on the time-to-market. A promising alternative is formal verification because it allows to ensure protocol compliance based on mathematical proofs. However, with regard to memory controllers no fully-automated verification process has been presented in the state-of-the-art yet, which means there is still a potential risk of human error. In this paper we present a framework that automatically generates SystemVerilog Assertions for a DRAM protocol. In addition, we show how the framework can be used efficiently for different tasks of memory controller development.
## KEYWORDS
Formal Verification, Property Checking, Petri Net, DRAM, Memory Controller
## 1 INTRODUCTION
Recently, we are witnessing a vast increase in memory-intensive applications (e.g., neural networks), which brings the memory subsystem more into focus. To keep up with this trend, the DRAM standardization committee JEDEC has released multiple domainspecific standards over the years, shown in Figure 1, and also upgraded them to meet the constantly increasing bandwidth, storage density and energy efficiency demands of the compute platforms. This poses a major challenge for system designers because the complex protocols described in new JEDEC standards have to be supported by their memory controller IPs. Furthermore, the number of new features introduced in each standard grows substantially from generation to generation, while the time-to-market for today's products is extremely short. E.g., the only major upgrade from DDR3 to DDR4 that affected the existing protocol was the introduction of bank groups, while the switch from DDR4 to DDR5
introduced a comprehensive and formal mathematical model based on Petri nets that contains all states, state transitions, commands and timings appearing in today's JEDEC standards. This model can also be represented in a compact and machine-readable format with a domain-specific language called DRAMml , which serves as a unique formal description. As a result, DRAMml can directly be used for the specification of future JEDEC standards. In their paper, an executable software model for simulation-based verification of virtual controller prototypes is generated from the description.
In this paper, we extend the generation approach to formal verification with the following new contributions:
- We present a framework that automatically generates SVA from DRAMml.
- Besides ensuring protocol compliance, we show that the framework can also identify the unsupported protocol features of a given controller.
- Wepresent a technique to detect timing-related performance limitations of a given controller using slightly-modified properties.
- Weintroduce a methodology to upgrade an existing memory controller to a different JEDEC standard by revealing the minimum set of required changes.
In our experiments we show that for one specific configuration the framework detected protocol violations and overestimated timings within an open-source DDR4 controller. In addition, we were able to identify all unimplemented protocol features of the controller without any prior knowledge or documentation. This demonstrates the power and versatility of formal verification for memory controller development.
The remaining paper is structured as follows: Section 2 introduces the required background. Section 3 presents a new Petri net model for the DDR4 standard. In Section 4 the property generation process within the framework is explained in detail. Experimental results of the framework application are presented in Section 5. Section 6 discusses related work before the paper is concluded in Section 7.
## 2 BACKGROUND
In this section we explain the basics of DRAMs, reintroduce timed Petri nets and the DRAM modeling language DRAMml [5], and give an overview of formal verification.
## 2.1 DRAMBasics
DRAM is organized in a multi-hierarchical fashion of channels, ranks, banks, rows and columns. Newer standards add additional hierarchies like bank groups (DDR4), logical ranks (DDR5) or pseudo channels (HBM2). Channels are completely independent entities with separate command/address and data buses. Each channel can be composed of multiple ranks, which are separate devices that also work independently of each other, but share common buses to the controller. Each rank is internally composed of several banks with a shared I/O region. Inside a bank, memory cells are organized in rows and columns.
Before data can be read ( RD ) from or written ( WR ) to cells, a row has to be activated ( ACT ), and only one row per bank can be active at the same time. In order to switch to another row, the currently active one has to be precharged ( PRE ) first. Since DRAM is a charge-based memory with leakage effects, each cell has to be refreshed regularly (usually every 64 ms). The internal refresh operation is triggered externally by the controller with a special refresh command ( REFA ) and makes the device inaccessible for a certain time. During idle periods, the controller can send DRAM devices into various powerdown modes (PDN, SREF) to save power. While in power-down, the devices are also inaccessible. Due to internal delays and shared hardware resources in the devices, a variety of different timings has to be observed by the controller between commands.
The memory controller itself is composed of a front end and back end. While the front end performs arbitration and scheduling of incoming read and write requests subject to certain priorities, the back end translates the requests into a sequence of commands that complies with the implemented standard. Hence, the back end is also the part of a DRAM controller that has to be adapted to new standards over and over.
## 2.2 Timed Petri Nets and DRAMml
Whenever a new DRAM standard is released by JEDEC, developers of memory controllers and memory simulation models must adopt the changes of the new protocol in order to guarantee compliance of their designs. JEDEC standards describe the memory protocols, i.e., legal DRAM command sequences and timings between commands, using a mixture of state machine diagrams, tables, and timing diagrams. However, even JEDEC themselves admit that parts of the state diagrams are simplified and some events are not captured in full detail [11]. Therefore, it is a difficult task for developers to extract the required information from the standards in a comprehensive and formally correct way. To facilitate this task, the authors of [5] have introduced a domain-specific language called DRAMml , which can serve as a unique formal description of a JEDEC standard's protocol. The language is both compact and extendable, so it can also be used to describe the latest standards with all their additional features in a compressed form. The semantics of DRAMml are based on timed Petri nets [4].
Because of the large number of parallel operating entities within each channel (e.g., ranks and banks), modeling a current DRAM subsystem with a finite state machines leads to a state explosion. Petri nets, on the other hand, allow the modeling of the DRAM subsystem's concurrency very efficiently.
As shown in Figure 2, the hierarchies of a DRAM subsystem are directly adopted in the Petri net. DRAM commands can be mapped to transitions, while different states (i.e., ACTIVE, PDN, SREF) are modeled by the assignment of tokens to places. Constraints in the sequence of commands are modeled by four types of arcs:
- (1) Place-to-transition arcs ( ) allow the connected transition to fire only if a token is present in the connected place. E.g., the arc between an ACTIVE state and a RD command implies that the RD command can only be executed if the respective bank is active. Firing the transition consumes one token.
- (2) Transition-to-place arcs ( ) add one token to the connected place if the connected transition fires.
- (3) Inhibitor arcs ( ) inhibit the connected transition from firing (i.e., command to be executed) if a token is present in
Figure 2: Revised DDR4 Petri Net Model [5]
<details>
<summary>Image 2 Details</summary>
### Visual Description
## Diagram: Memory Bank Power Management
### Overview
The image is a diagram illustrating the power management and refresh mechanisms within a memory bank architecture. It depicts the flow of power-down (PDN) and self-refresh (SREF) signals across different components of the memory system, including bank groups, banks, and individual memory cells. The diagram highlights the interaction between active states, refresh operations, and power-down sequences.
### Components/Axes
* **Hierarchical Structure:** The diagram shows a hierarchical memory organization, with levels including "Rank 0", "Bank Group 0", "Bank BA-1", and "Bank 0". A similar structure exists for "Bank Group BG-1".
* **Power-Down Management:** This section illustrates the sequence of states involved in power-down, including SRE, SREF, and SRX, as well as PDE, PDN, and PDX.
* **Refresh Management:** This section shows the REFA state, indicating a refresh operation.
* **Active States:** The diagram features "ACTIVE[0][0]" and "ACTIVE[BG-1][0]" states, representing the active state of memory cells.
* **Memory Operations:** The diagram includes nodes representing memory operations such as RD (Read), WR (Write), RDA (Read with Activate), and WRA (Write with Activate). PRE (Precharge) and PREA (Precharge All).
* **Signal Indicators:** The diagram uses dotted lines to indicate PDN and SREF signals.
### Detailed Analysis
* **Bank Group 0:**
* **Rank 0:** Top level of the hierarchy.
* **Bank Group 0:** Second level of the hierarchy.
* **Bank BA-1:** Third level of the hierarchy.
* **Bank 0:** Contains the core memory operations and active state.
* **ACT:** Connected to PDN and SREF signals.
* **ACTIVE[0][0]:** Central node connected to RD, WR, RDA, WRA, and PRE.
* **RD:** Connected to PDN signal.
* **WR:** Connected to PDN signal.
* **RDA:** Connected to PDN signal.
* **WRA:** Connected to PDN signal.
* **PRE:** Connected to PDN and SREF signals.
* **Bank Group BG-1:**
* **Rank 0:** Top level of the hierarchy.
* **Bank Group BG-1:** Second level of the hierarchy.
* **Bank BA-1:** Third level of the hierarchy.
* **Bank 0:** Contains the core memory operations and active state.
* **ACT:** Connected to PDN and SREF signals.
* **ACTIVE[BG-1][0]:** Central node connected to RD, WR, RDA, WRA, and PRE.
* **RD:** Connected to PDN signal.
* **WR:** Connected to PDN signal.
* **RDA:** Connected to PDN signal.
* **WRA:** Connected to PDN signal.
* **PRE:** Connected to PDN and SREF signals.
* **Power-Down Management:**
* **ACTIVE:** Connected to PDN and SREF signals.
* **SRE:** State in the power-down sequence.
* **SREF:** State in the power-down sequence.
* **SRX:** State in the power-down sequence.
* **PDE:** State in the power-down sequence.
* **PDN:** State in the power-down sequence.
* **PDX:** State in the power-down sequence.
* **Refresh Management:**
* **ACTIVE:** Connected to PDN and SREF signals.
* **REFA:** State indicating a refresh operation.
* **Interconnections:**
* The "ACTIVE[0][0]" state is connected to "PREA" via a red line, indicating a direct transition.
* The "ACTIVE[BG-1][0]" state is connected to "PREA" via a red line, indicating a direct transition.
### Key Observations
* The diagram illustrates the flow of control signals (PDN, SREF) through different states and operations within the memory bank.
* The "ACTIVE" states are central nodes, connecting to various memory operations and power management sequences.
* The red lines highlight a specific transition from the active state to the precharge all state.
* The diagram shows a mirrored structure for Bank Group 0 and Bank Group BG-1, suggesting a similar architecture and operation.
### Interpretation
The diagram provides a high-level overview of the power management and refresh mechanisms in a memory bank. It demonstrates how the memory system transitions between active, power-down, and refresh states. The hierarchical structure indicates a modular design, where individual banks are grouped into larger units. The red lines connecting the active states to the precharge all state suggest a critical path or a common operation performed during memory management. The diagram is useful for understanding the control flow and state transitions within the memory system, which is essential for optimizing power consumption and performance.
</details>
- the connected place. For example, a REFA command can only be issued if the DRAM is neither in ACTIVE nor in PDN nor in SREF state.
- (4) Reset arcs ( ) remove all tokens from the connected place(s) if the connected transition fires. E.g., if a PREA commandis executed all tokens are removed from ACTIVE banks, making them idle again.
Timing constraints between two transitions are modeled by custom command-to-command timing arcs ( 𝑡 𝑥 ). For example, between the ACT and the RD command there exists a timing arc with the value of 𝑡 𝑅𝐶𝐷 . More complex timing constraints like the four activate window 1 require a combination of custom timed arcs and places with timed tokens (see [5]).
DRAMml is a domain-specific language to describe the complete Petri net structure in a textual way, while the user does not need to understand the underlying Petri net semantics. E.g., the place-to-transition arc between ACTIVE and RD is specified as ACTIVE -> RD , the inhibitor arc between ACTIVE and REFA is specified as ACTIVE -o REFA , the reset arc between ACTIVE and PREA is specified as ACTIVE ->> PREA , and the timing arc between ACT and RD is specified as ACT -<> RD (tRCD) . For a more comprehensive explanation of DRAMml we refer to [5].
1 The four activate window limits the number of issued activate commands within a rolling time window to four.
## 2.3 Formal Verification
Over the last two decades, functional hardware verification using formal methods has reached a high level of maturity. The formal tools that are commercially available today are capable of handling designs of realistic size, and they have become standard components in many industrial hardware design and verification flows.
The approach presented in this paper is based on formal property checking . A property checker takes as input an RTL description of a hardware design (e.g., in Verilog/SystemVerilog or VHDL), and a set of properties in a property specification language such as SystemVerilog Assertions (SVA). A property usually has the form of an implication between an antecedent ('assumption') describing an input scenario to be considered, and a consequent ('commitment') describing the behavior expected from the design according to the specification [12]. Both assumption and commitment are specified by logic formulas over design signals at different time points. Property specification languages such as SVA contain a rich set of syntactic elements that enable the user to write concise and expressive specifications of design intent.
For each property, the tool searches for a sequence of inputs to the design such that the property is violated . Such a sequence is called a counterexample to the property. If the property checker finds a counterexample it is returned to the user as a timing diagram similar to a simulation waveform, displaying all relevant signal values of the RTL model and indicating the time points and signals where the commitment of the property is being violated. If the tool reports that no counterexample exists, the property is guaranteed to hold for the design under any possible input sequence. It is
this mathematical rigor that allows detecting bugs in corner-case states and hard-to-activate input scenarios, which are difficult to anticipate for a human verification engineer.
In our approach we use formal property checking to verify that a memory controller design fulfills the specification of a particular JEDEC standard expressed in DRAMml. Section 4 describes how the individual Petri net elements underlying the DRAMml specification are translated into SVA properties that can then be verified for a given controller.
## 3 DDR4 PETRI NET
As explained in Section 2.2 the semantics of DRAMml are based on timed Petri nets. In [5] the authors have presented an example Petri net for the DDR3 JEDEC standard. However, in this work we aim to verify a memory controller for the successor standard DDR4, which introduces bank groups as an additional device hierarchy. Moreover, the Petri net in [5] does not fully comply with the specified protocol because it allows a precharge command to be issued only if the associated bank is active. This constraint is not described in the standard. Therefore, we present a revised version of the Petri net in Figure 2, which fully complies with the DDR4 standard. It includes bank groups and allows issuing precharge commands also when the respective bank is idle. The key difference in the structure is the elimination of the common idle place. Instead, some additional inhibitor and reset arcs ensure proper command cycling. For the sake of clarity, no timing arcs are shown in the figure.
## 4 PROPERTY GENERATION
The main task of our framework is the generation of SVA from a DRAMml description of a standard by parsing the input file and translating all language elements into SVA equivalents. In the following, the most important translations are explained with short examples.
As shown in Section 2.2, DRAMml describes a timed Petri net with different hierarchies that correspond to ranks, banks, etc. These hierarchies consist of places, transitions and different types of arcs. First, all hierarchies are translated into nested loop generate constructs where the number of iterations is equivalent to the number of instances in each hierarchy (see Listings 1 and 2).
## Listing 1: DRAMml Hierarchy
```
<num_inst> : <hier> {
// placeholder
}
```
## Listing 2: SVA Hierarchy
```
genvar <hier>_id;
generate
for (<hier>_id = 0; <hier>_id < <num_inst>; <hier>_id++) begin
// placeholder
end
endgenerate
```
Each place is translated into a logic variable whose value, i.e., number of tokens, depends on all connected place-to-transition, transition-to-place and reset arcs (see Listings 3 and 4). Modeling a place as a separate logic variable is required to specify properties that consider only input and output signals of a controller design, but do not need access to internal signals. Places with more than one token can be implemented as packed arrays, initial tokens can be assigned during reset. If a place is located inside a hierarchy, an additional dimension is added to the array. Similarly, for transitions within a hierarchy the target instance (i.e., <hier>\_id ) has to be considered.
## Listing 3: DRAMml Place
```
Place {
<place>;
}
Arcs {
<trans_in> -> <place>;
<place> -> <trans_out>;
<place> -> <trans_reset>;
}
```
## Listing 4: SVA Place
```
logic <place>;
always @(posedge clk) begin
if (reset)
<place> <= 1'b0;
else begin
if (cmd == <trans_in>)
<place> <= <place> + 1'b1;
else if (cmd == <trans_out>)
<place> <= <place> - 1'b1;
else if (cmd == <trans_reset>)
<place> <= 1'b0;
end
```
Self loops, i.e., a place and a transition that are connected by two arcs in a loop (e.g., the RD transition and ACTIVE place within a bank in Figure 2), do not have to be added to the always block because they would decrease the variable by 1 and increase it again by 1 in the same clock cycle.
Properties are generated by three different types of arcs. First, a place-to-transition arc is translated into an overlapped implication (see Listings 5 and 6). If the command denoted by the transition is executed (assumption), a token must be present in the connected place (commitment). Otherwise, the command sequence is illegal.
## Listing 5: DRAMml Place-To-Transition Arc
```
Arcs {
<place> -> <trans>;
}
```
## Listing 6: SVA Place-To-Transition Arc
```
property arc_<place>_<trans>;
@(posedge clk) disable iff (reset)
(cmd == <trans>) |-> (<place> >= 1'b1);
endproperty;
assert property(arc_<place>_<trans>);
```
An inhibitor arc is translated in a similar way. A place with a token implies the non-firing of the connected transition, i.e., the command is not allowed to be executed in the current state (see Listings 7 and 8).
## Listing 7: DRAMml Inhibitor Arc
```
Arcs {
<place> -o <trans>;
}
```
## Listing 8: SVA Inhibitor Arc
```
property inhibitor_<place>_<trans>;
@(posedge clk) disable iff (reset)
(<place> >= 1'b1) |-> not (cmd == <trans>);
endproperty;
assert property(@(posedge clk) inhibitor_<place>_<trans>);
```
The custom command-to-command timing arc is translated into a negated implication with a timing window (see Listings 9 and 10), which means that after issuing the command denoted by trans\_a (assumption), a command of the type denoted by trans\_c cannot be issued during the specified timing window (commitment).
## Listing 9: DRAMml Command-To-Command Timing Arc
```
Arcs {
<trans_a> -<> <trans_c> (<timing>);
}
```
## Listing 10: SVA Command-To-Command Timing Arc
```
property timing_<trans_a>_<trans_c>;
@(posedge clk) disable iff (reset)
(cmd == <trans_a>) |->
not ##[1:(<timing> - 1)] (cmd == <trans_c>);
endproperty;
assert property(timing_<trans_a>_<trans_c>);
```
Depending on the location of arcs and their connected places as well as transitions within the Petri net, the properties are inserted inside the loop generates and the target instances are taken into consideration (e.g., for a RD command the target bank, bank group and rank is also checked).
More complex timing constraints like the four activate window, which are modeled by a combination of custom timed arcs and places with timed tokens (see Section 2.2 and [5]), cannot directly be translated into an implication with a timing window as shown in Listing 10, because they depend on a sequence of commands over a period of time. However, [1] presents a method to check such constraints with SVA. We use the same approach in our generator and refer to this paper for more information.
## 5 EXPERIMENTAL RESULTS
The versatility of our framework is demonstrated by three application examples. First, the standard compliance of an open-source DDR4 controller is verified and its unsupported protocol features are identified. Second, we show how a slightly modified subset of properties can be used to detect performance limitations that result from overestimated timings between commands. Third, we introduce a methodology similar to the idea of property-driven development to upgrade an existing memory controller to a different JEDEC standard.
## 5.1 Evaluation of Standard Compliance and Unsupported Features
Due to the lack of open-source controllers for the latest JEDEC standards DDR5, LPDDR5 or HBM3, a low power, low latency DDR4 controller [14, 15] is used for demonstration purposes. In order to generate properties for the target hardware, several input parameters of the generator have to be configured. These are the standard, specific timing values in clock cycles and the number of
Table 1: Overview of Properties for DDR4 Controller
| Banks | Generated | Unique | Violated | Unreachable |
|---------|-------------|----------|------------|---------------|
| 16 | 448 | 124 | 0 | 91 |
| 8 | 270 | 124 | 4 | 91 |
banks, bank groups and ranks. Afterwards, the generated SVA code as well as the RTL description of the controller can directly be read by a property checker, in our case OneSpin 360 DV.
Weverify two different controller configurations. In the first case, the default DDR4 configuration with 16 banks distributed over 4 bank groups is used. In the second case, the memory controller is reconfigured to a stripped down version that only supports 8 banks distributed over 2 bank groups. This configuration is required to drive special DDR4 devices with a wider 16 bit data bus. The number of ranks is fixed to 1 because the controller only provides a single chip select signal and, thus, does not support multi-rank operation.
In the case of 16 banks all generated properties hold, which proves that the controller complies with the DRAM protocol. With the reduced number of banks, 4 different properties are violated. Since all violated properties are related to bank group timings, it suggests that the controller was not intended to be operated with only 2 bank groups and this special configuration was not tested. However, with our framework it was straightforward to detect the protocol violations because input parameters are restricted to valid values and both configurations could be checked within one day.
Besides verifying whether a property holds, the checker also proves if the scenarios described in the properties are reachable, i.e., if there exists a sequence of inputs that triggers the corresponding commands. For the given DDR4 controller, some properties are in fact unreachable. Even if this does not result in any protocol violations, it means that some parts of the standard have not been implemented, which, in the worst case, prevents the controller from proper operation. Fortunately, the unreachable properties exclusively relate to read and write commands with auto-precharge 2 and power-down entry and exit commands, which are both optional features.
The possibility to identify unsupported features is extremely helpful for designers that use third party IPs because they can directly compare the feature set of a controller with their requirements without having any prior knowledge and without checking the documentation. A summary of the total number of generated properties, unique properties (i.e., without considering loop generates), unique violated properties and unique unreachable properties for both controller configurations is provided in Table 1.
## 5.2 Detection of Performance Limitations
Besides issuing commands according to the protocol, another main objective of the memory controller is to maximize the performance of the DRAM subsystem. This can be achieved, e.g., by reordering incoming requests to increase the number of consecutive accesses to the same row in a bank (called row hits), which is usually done by a scheduler in the front end. However, the back end can influence
2 Read and write with auto-precharge allow to trigger a read or write operation and a subsequent precharge with a single command.
Figure 3: Controller-Induced Performance Limitation
<details>
<summary>Image 3 Details</summary>
### Visual Description
## Timing Diagram: Clock, Command, and Data Signals
### Overview
The image is a timing diagram illustrating the relationship between a clock signal (CLK), a command signal (CMD), and a data signal (DATA). The diagram shows how these signals interact over time, with specific commands (NOP, RD) and data values (D0, D1, D2, D3) being transmitted in relation to the clock signal. The diagram also indicates a time interval labeled "tCCD + 1".
### Components/Axes
* **CLK (Clock):** A square wave signal that alternates between high and low states. The clock signal provides the timing reference for the other signals.
* **CMD (Command):** A signal that represents commands being sent. The commands shown are "NOP" (No Operation) and "RD" (Read). The CMD signal alternates between gray filled boxes with the command inside and white boxes with the command inside.
* **DATA:** A signal that represents data being transmitted. The data values shown are "D0", "D1", "D2", and "D3". The DATA signal consists of white boxes with the data value inside.
* **tCCD + 1:** A red double-headed arrow indicating a time interval. The arrow spans from the rising edge of the clock signal before the "RD" command to the rising edge of the clock signal before the next "RD" command.
### Detailed Analysis
* **CLK (Clock):** The clock signal is a periodic square wave. It alternates between a high state and a low state.
* **CMD (Command):** The command signal alternates between "NOP" (No Operation) and "RD" (Read" commands. The sequence is NOP, NOP, RD, NOP, NOP, RD, NOP, NOP, RD, NOP, NOP.
* **DATA:** The data signal transmits data values D0, D1, D2, and D3. The data is transmitted when the CMD signal is "RD". When the CMD signal is "NOP", the DATA signal remains at a constant level (blue line).
* **tCCD + 1:** The time interval "tCCD + 1" represents the time between consecutive read operations.
### Key Observations
* The "RD" command is associated with the transmission of data values D0, D1, D2, and D3.
* The "NOP" command indicates no operation, and the data signal remains constant during this time.
* The clock signal provides the timing reference for the command and data signals.
### Interpretation
The timing diagram illustrates a synchronous communication protocol where commands and data are transmitted in relation to a clock signal. The "RD" command triggers the transmission of data values, while the "NOP" command indicates an idle state. The time interval "tCCD + 1" represents the cycle time between consecutive read operations. This type of diagram is used to understand and analyze the timing relationships between different signals in a digital system.
</details>
the performance as well. If all properties hold, it is ensured that the controller is compliant to a specific JEDEC standard (see Section 5.1). Unfortunately, the timing-related properties only prove that the minimum delay between two commands is always observed. The reverse case, i.e., that two commands are actually issued with the minimum delay if possible, is not ensured. In the worst case, the controller could overestimate timings between successive commands and compromise the overall performance. Figure 3 shows an example where the memory controller always issues read commands with a distance of 𝑡 𝐶𝐶𝐷 + 1, while the minimum timing is 𝑡 𝐶𝐶𝐷 . As a result, the data bus is only utilized in two of three clock cycles and the maximum bandwidth is reduced by 33 %.
Using formal property checking, we are not able to directly prove this reverse case, but we can at least prove whether there exists one scenario in which the two commands are issued with minimum distance. In addition, if no such scenario is found, a lower bound can be determined successively. For this purpose, the framework generates all reachable timing-related properties from Section 5.1 with each timing incremented by one clock cycle. If a property still holds, a possible candidate for a design flaw is found, which can then be investigated in more detail. This process is repeated until the point is reached where all properties are violated.
For the given DDR4 controller, 9 unique properties still hold with one additional clock cycle added. All these properties include one refresh-related command (either precharge all ( PREA ), which is usually used before a refresh command to precharge all banks at once, or refresh itself ( REFA )), which shows that the switch from normal operation to refresh operation is not handled optimally in the controller and extra delays are induced. Only after adding 22 additional clock cycles all properties are violated. However, since refresh commands are issued very rarely, the resulting performance impact is negligible. In fact, it is likely that the extra delays are added on purpose to safely meet all timing constraints before refresh operation is started and save hardware resources by implementing a single clock cycle counter for the worst-case timing assumption.
## 5.3 Memory Controller Upgrade
Due to the large number of recent JEDEC standard releases, upgrading an existing memory controller to support a new protocol is one of the main development tasks. The continuously-increasing feature set and the resulting hardware complexity makes this task very challenging. As a starting point of the upgrade process it is important for a designer to know which existing parts of the hardware can be adopted, which parts have to be changed and which features have to be added to create a properly functioning controller implementation as fast as possible.
Based on formal property checking, we present a methodology that identifies the minimum set of changes required to perform such an upgrade. For demonstration, the DDR4 controller from the previous sections should be upgraded to the successor standard DDR5. As a first step, a set of properties for DDR5 is generated with input parameters that match the DDR4 input parameters as closely as possible. In the evaluation in Section 5.1 the unsupported controller features have already been identified. All DDR5 properties related to these features are discarded as a next step. The remaining DDR5 properties are then verified by the property checker for the DDR4 controller.
Afterwards, the necessary upgrades can be derived from the results of the verification. A property that is reachable and still holds means that no further action is required. E.g., the legal and illegal command sequences have not changed from DDR4 to DDR5. Similarly, a subset of the timings is still valid. However, there are also timings that have been newly added. E.g., with DDR5, the minimum timing between two write operations to the same bank group is longer than between two read operations, which was still identical with DDR4. Consequently, the corresponding properties are violated and additional checks have to be implemented in the hardware. Some of the properties are also unreachable. They are related to features that have been newly added with DDR5, e.g., same-bank refresh or a second burst length that can be selected on the fly. For these features the designer must make individual decisions depending on whether they are optional or not and whether they are expected to be required for the controller implementation. The upgrade is completed when all relevant properties hold and are reachable.
## 6 RELATED WORK
The idea of applying formal property checking to DRAM controllers has already been presented by Datta and Singhal back in 2008 [1]. They write a set of SVA to formally verify the standard compliance of the Sun OpenSPARC DDR2 controller. The problem is that all properties are extracted manually from the DDR2 JEDEC standard and afterwards translated into SVA code, which takes a lot of time and is prone to human error. In addition, there is no guarantee that all timings and legal command sequences are covered. Similar work is presented in [6] for an LPDDR3 controller.
Kayed et al. [7] address the problem of manual extraction and use a timing diagram tool to translate timing diagrams from a JEDEC standard into a Timing Diagram Markup Language (TDML) based format. From this description they automatically generate SVA. While the generation reduces manual work and thus possible sources of human error, the approach still has a major drawback.
Since only some parts of the DRAM protocol are illustrated in timing diagrams, the verification is incomplete and does not prove full standard compliance. Especially the legal and illegal command sequences are not covered at all.
MCXplore, a framework presented in [2, 3], uses a model checker to generate counterexamples for properties with an optimal number of memory requests that serve as test templates for RTL DRAM controllers or DRAM simulators. These test patterns can be used both to validate the memory controller front end (scheduling, etc.) and back end (interactions between memory commands). The approach is design independent and provides quick feedback to a designer, but it also does not cover the entire protocol and does not give any formal guarantees.
In [13], the authors use the language of Symbolic Analysis Laboratory (SAL) to model the architectural design of a DRAM cache controller in terms of interacting transition systems. This design is then verified using model checking. The work covers lots of cache-related properties, but only includes a subset of protocol constraints.
The paper [10] proposes a framework written in Coq to model DRAM controllers. Using the framework, the authors prove the legality of command sequences as well as timings between commands, and in addition they check if each incoming request is handled in bounded time. However, as in other works, only a subset of the protocol is checked and a reviewer has to verify that the formal specification matches the standard.
## 7 CONCLUSION
In this paper we have presented a framework that automatically generates SVA for the formal verification of DRAM controllers. The framework is useful for different tasks of controller development, which was demonstrated in three application examples. During the experiments, we have also detected protocol violations in an open-source DDR4 controller. As a next step, we plan to find more applications of formal verification in memory controller development to easily handle future JEDEC standard releases.
## ACKNOWLEDGMENTS
This work was supported within the Fraunhofer and DFG cooperation programme (Grant no. 248750294) and supported by the Fraunhofer High Performance Center for Simulation- and Softwarebased Innovation. Furthermore, we thank Bryan Daniel Olmos Suquillo for his support.
## REFERENCES
- [1] Abhishek Datta and Vigyan Singhal. 2008. Formal Verification of a Public-Domain DDR2 Controller Design. In 21st International Conference on VLSI Design (VLSID 2008) . 475-480. https://doi.org/10.1109/VLSI.2008.94
- [2] M. Hassan and H. Patel. 2016. MCXplore: An automated framework for validating memory controller designs. In 2016 Design, Automation Test in Europe Conference Exhibition (DATE) . 1357-1362.
- [3] M. Hassan and H. Patel. 2018. MCXplore: Automating the Validation Process of DRAM Memory Controller Designs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37, 5 (May 2018), 1050-1063. https: //doi.org/10.1109/TCAD.2017.2705123
- [4] Lasse Jacobsen, Morten Jacobsen, Mikael H. Møller, and Jiří Srba. 2011. Verification of Timed-Arc Petri Nets. In SOFSEM 2011: Theory and Practice of Computer Science , Ivana Černá, Tibor Gyimóthy, Juraj Hromkovič, Keith Jefferey, Rastislav Králović, Marko Vukolić, and Stefan Wolf (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 46-72.
- [5] Matthias Jung, Kira Kraft, Taha Soliman, Chirag Sudarshan, Christian Weis, and Norbert Wehn. 2019. Fast Validation of DRAM Protocols with Timed Petri Nets. In Proceedings of the International Symposium on Memory Systems (Washington, District of Columbia) (MEMSYS '19) . ACM, New York, NY, USA, 133-147. https: //doi.org/10.1145/3357526.3357556
- [6] Moustafa Kassem, Marianne Michel, Mohamed AbdelSalam, and Ashraf Salem. 2013. A novel approach for assertion based verification of DDR memory protocols. In Proceedings of the 2013 Forum on specification and Design Languages (FDL) . 1-4.
- [7] M. O. Kayed, M. Abdelsalam, and R. Guindi. 2014. A Novel Approach for SVA Generation of DDR Memory Protocols Based on TDML. In 2014 15th International Microprocessor Test and Verification Workshop . 61-66. https://doi.org/10.1109/ MTV.2014.15
- [8] Young-Cheon Kwon, Suk Han Lee, Jaehoon Lee, Sang-Hyuk Kwon, Je Min Ryu, Jong-Pil Son, O Seongil, Hak-Soo Yu, Haesuk Lee, Soo Young Kim, Youngmin Cho, Jin Guk Kim, Jongyoon Choi, Hyun-Sung Shin, Jin Kim, BengSeng Phuah, HyoungMin Kim, Myeong Jun Song, Ahn Choi, Daeho Kim, SooYoung Kim, EunBong Kim, David Wang, Shinhaeng Kang, Yuhwan Ro, Seungwoo Seo, JoonHo Song, Jaeyoun Youn, Kyomin Sohn, and Nam Sung Kim. 2021. 25.4 A 20nm 6GB Function-In-Memory DRAM, Based on HBM2 with a 1.2TFLOPS Programmable Computing Unit Using Bank-Level Parallelism, for Machine Learning Applications. In 2021 IEEE International Solid- State Circuits Conference (ISSCC) , Vol. 64. 350-352. https://doi.org/10.1109/ISSCC42613.2021.9365862
- [9] Seongju Lee, Kyuyoung Kim, Sanghoon Oh, Joonhong Park, Gimoon Hong, Dongyoon Ka, Kyudong Hwang, Jeongje Park, Kyeongpil Kang, Jungyeon Kim, Junyeol Jeon, Nahsung Kim, Yongkee Kwon, Kornijcuk Vladimir, Woojae Shin, Jongsoon Won, Minkyu Lee, Hyunha Joo, Haerang Choi, Jaewook Lee, Donguc Ko, Younggun Jun, Keewon Cho, Ilwoong Kim, Choungki Song, Chunseok Jeong, Daehan Kwon, Jieun Jang, Il Park, Junhyun Chun, and Joohwan Cho. 2022. A 1ynm 1.25V 8Gb, 16Gb/s/pin GDDR6-based Accelerator-in-Memory supporting 1TFLOPS MAC Operation and Various Activation Functions for Deep-Learning Applications. In 2022 IEEE International Solid- State Circuits Conference (ISSCC) , Vol. 65. 1-3. https://doi.org/10.1109/ISSCC42614.2022.9731711
- [10] Felipe Lisboa Malaquias, Mihail Asavoae, and Florian Brandner. 2022. A Coq Framework for More Trustworthy DRAM Controllers. In Proceedings of the 30th International Conference on Real-Time Networks and Systems (Paris, France) (RTNS 2022) . Association for Computing Machinery, New York, NY, USA, 140-150. https://doi.org/10.1145/3534879.3534907
- [11] Jedec Solid State Technology Association. 2012. DDR4 SDRAM (JESD 79-4).
- [12] Minh D. Nguyen, Max Thalmaier, Markus Wedler, Jörg Bormann, Dominik Stoffel, and Wolfgang Kunz. 2008. Unbounded Protocol Compliance Verification using Interval Property Checking with Invariants. IEEE Transactions on Computer-Aided Design 27, 11 (November 2008), 2068-2082.
- [13] Debiprasanna Sahoo, Swaraj Sha, Manoranjan Satpathy, Madhu Mutyam, S. Ramesh, and Partha Roop. 2018. Formal Modeling and Verification of Controllers for a Family of DRAM Caches. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37, 11 (2018), 2485-2496. https://doi.org/10.1109/ TCAD.2018.2857318
- [14] Chirag Sudarshan, Jan Lappas, Christian Weis, Deepak M. Mathew, Matthias Jung, and Norbert Wehn. 2019. A Lean, Low Power, Low Latency DRAM Memory Controller for Transprecision Computing. In Embedded Computer Systems: Architectures, Modeling, and Simulation , Dionisios N. Pnevmatikatos, Maxime Pelcat, and Matthias Jung (Eds.). Springer International Publishing, Cham, 429-441.
- [15] Chirag Sudarshan, Jan Lappas, Christian Weis, Deepak M. Mathew, Matthias Jung, and Norbert Wehn. 2021, Last Access: 20.07.2022. SYSTEM-VERILOG CODE for DDR4 Memory Controller with XILINX Phy. https://github.com/oprecomp/ DDR4\_controller.