A Framework for Formal Verification of DRAM Controllers

被引:0
作者
Steiner, Lukas [1 ]
Sudarshan, Chirag [1 ]
Jung, Matthias [2 ]
Stoffel, Dominik [3 ]
Wehn, Norbert [1 ]
机构
[1] TU Kaiserslautern, Microelect Syst Design Res Grp, Kaiserslautern, Germany
[2] Fraunhofer Inst Expt Software Engn IESE, Kaiserslautern, Germany
[3] TU Kaiserslautern, Chair Elect Design Automat, Kaiserslautern, Germany
来源
PROCEEDINGS OF THE INTERNATIONAL SYMPOSIUM ON MEMORY SYSTEMS, MEMSYS 2022 | 2022年
关键词
Formal Verification; Property Checking; Petri Net; DRAM; Memory Controller;
D O I
10.1145/3565053.3565059
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
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 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 utilized in different memory controller development tasks.
引用
收藏
页数:7
相关论文
共 15 条
[1]   Formal verification of a public-domain DDR2 controller design [J].
Datta, Abhishek ;
Singhal, Vigyan .
21ST INTERNATIONAL CONFERENCE ON VLSI DESIGN: HELD JOINTLY WITH THE 7TH INTERNATIONAL CONFERENCE ON EMBEDDED SYSTEMS, PROCEEDINGS, 2008, :475-+
[2]   MCXplore: Automating the Validation Process of DRAM Memory Controller Designs [J].
Hassan, Mohamed ;
Patel, Hiren .
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2018, 37 (05) :1050-1063
[3]  
Hassan M, 2016, DES AUT TEST EUROPE, P1357
[4]  
Jacobsen L, 2011, LECT NOTES COMPUT SC, V6543, P46, DOI 10.1007/978-3-642-18381-2_4
[5]  
Jedec Solid State Technology Association, 2012, DDR4 SDRAM (JESD 79-4)
[6]   Fast Validation of DRAM Protocols with Timed Petri Nets [J].
Jung, Matthias ;
Kraft, Kira ;
Soliman, Taha ;
Sudarshan, Chirag ;
Weis, Christian ;
Wehn, Norbert .
MEMSYS 2019: PROCEEDINGS OF THE INTERNATIONAL SYMPOSIUM ON MEMORY SYSTEMS, 2019, :133-146
[7]  
Kassem Moustafa., 2013, P 2013 FORUM SPECIFI, P1
[8]   A Novel Approach for SVA Generation of DDR Memory Protocols Based on TDML [J].
Kayed, Mohamed O. ;
Abdelsalam, Mohamed ;
Guindi, Rafik .
2014 15TH INTERNATIONAL MICROPROCESSOR TEST AND VERIFICATION WORKSHOP (MTV 2014), 2015, :61-66
[9]   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 [J].
Kwon, Young-Cheon ;
Lee, Suk Han ;
Lee, Jaehoon ;
Kwon, Sang-Hyuk ;
Ryu, Je Min ;
Son, Jong-Pil ;
Seongil, O. ;
Yu, Hak-Soo ;
Lee, Haesuk ;
Kim, Soo Young ;
Cho, Youngmin ;
Kim, Jin Guk ;
Choi, Jongyoon ;
Shin, Hyun-Sung ;
Kim, Jin ;
Phuah, BengSeng ;
Kim, HyoungMin ;
Song, Myeong Jun ;
Choi, Ahn ;
Kim, Daeho ;
Kim, SooYoung ;
Kim, Eun-Bong ;
Wang, David ;
Kang, Shinhaeng ;
Ro, Yuhwan ;
Seo, Seungwoo ;
Song, JoonHo ;
Youn, Jaeyoun ;
Sohn, Kyomin ;
Kim, Nam Sung .
2021 IEEE INTERNATIONAL SOLID-STATE CIRCUITS CONFERENCE (ISSCC), 2021, 64 :350-+
[10]  
Lee SC, 2022, INT J ENVIRON SCI TE, V19, P11023, DOI [10.1007/s13762-022-03911-8, 10.1109/IECON49645.2022.9968500]