Leveraging Reusable Code and Proofs to Design Complex DRAM Controllers - A Case Study

Critical real-time systems are getting more and more complex and require ever more computing power. Multi-core platforms, GPUs, and custom accelerators promise to deliver this needed performance. However, these platforms are notoriously hard to analyze and lack predictability in terms of timing properties. Computer architectures and platforms that offer both predictability and performance are thus needed. This work investigates the use of the interactive proof assistant Coq in order to model complex DRAM memory controllers (MCs) for multi-core platforms. The design of predictable high-performance MCs is particularly challenging, since memory requests have to be processed efficiently, while facing interference from other cores in the system. The problem is exacerbated by the complexity of DRAM devices and the various timing constraints they impose. Specifically, this work extends a previous Coq framework by focusing on reusability, which allows designers to develop and prove complex MCs. As a use-case, we present TDMShelve, an MC balancing performance and isolation.