论文标题
正式验证DRAM控制器的框架
A Framework for Formal Verification of DRAM Controllers
论文作者
论文摘要
最近的JEDEC DRAM标准版本及其不断增长的功能集使设计人员很难将内存控制器IP迅速升级到每个新标准。特别是由于与其前任相比，由于标准，LPDDR5或HBM3等标准的较高协议复杂性，硬件验证是具有挑战性的。通过传统的基于模拟的验证，可以保证所有可能的状态的覆盖范围，尤其是对于控制流丰富的存储器控制器的覆盖范围。这直接影响到市场上的时间。有希望的替代方法是正式验证，因为它允许基于数学证明确保协议合规性。但是，关于记忆控制器，最新的验证过程尚未提出完全自动化的验证过程，这意味着仍然存在人为错误的潜在风险。在本文中，我们提出了一个框架，该框架自动为DRAM协议生成SystemVerilog主张。此外，我们还展示了如何有效地将框架用于内存控制器开发的不同任务。
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.
