A Framework for Formal Verification of DRAM Controllers

TL;DR

This paper introduces an automated framework for formal verification of DRAM controllers, significantly improving protocol compliance assurance and reducing verification errors compared to traditional methods.

Contribution

It presents a novel framework that automatically generates SystemVerilog Assertions for DRAM protocols, streamlining the verification process for complex memory controllers.

Findings

Framework automates assertion generation for DRAM protocols

Reduces human error in protocol verification

Enhances efficiency in memory controller development

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 simulation-based 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.