A Coq Framework for More Trustworthy DRAM Controllers

In order to prove conformance to memory standards and bound memory access latency, recently proposed real-time DRAM controllers rely on paper and pencil proofs, which can be troubling: they are difficult to read and review, they are often shown only partially and/or rely on abstractions for the sake of conciseness, and they can easily diverge from the controller implementation, as no formal link is established between both. We propose a new framework written in Coq, in which we model a DRAM controller and its expected behaviour as a formal specification. The trustworthiness in our solution comes two-fold: 1) proofs that are typically done on paper and pencil are now done in Coq and thus certified by it's kernel, and 2) the reviewer's job develops into making sure that the formal specification matches the standards - instead of performing a thorough check of the underlying mathematical formalism. Our framework provides a generic DRAM model capturing a set of controller properties as proof obligations, which all implementations must comply with. We focus on properties related to the respect of timing constraints imposed by the memory standards, the correctness of the DRAM command protocol and the assertiveness that every incoming request is handled in bounded time. We refine our specification with two implementations based on widely-known arbitration policies - First-in First-Out (FIFO) and Time-Division Multiplexing (TDM). We extract proved code from our model and use it as a "trusted core"on a cycle-accurate DRAM simulator.