A Coq Framework for More Trustworthy DRAM Controllers
TimeWednesday, July 13th6pm - 7pm PDT
LocationLevel 2 Lobby
DescriptionAiming at proving conformance to memory standards and bounding memory access latency, recently proposed real-time DRAM controllers rely on paper and pencil proofs, which can be difficult to read and review. Lacking a formal link between implementation and proofs, they can easily diverge. We propose a new framework written in Coq, in which we model a DRAM system as a formal specification. The timing requirements are written as proof obligations, which all arbiter instances must comply with. We refine the specification with two implementations, extract code from our model and use it as a “trusted core” on a cycle-accurate simulator.