MSimDRAM: Formal Model Driven Development of a DRAM Simulator
Debiprasanna Sahoo, Manoranjan Satpathy · 2016
The authors have developed a formal model based DRAM simulator called MSimDRAM. The authors start with the DRAM controller (DRAM-C) requirements. The authors next develop an architectural design in terms of interacting agents along with the constraints associated with each agent and its interface. Keeping the architecture in mind, they develop a formal model in terms of interacting state machines. Rigorous verification methodologies are applied, so that the formal model satisfies the requirement and design level constraints. They have developed the formal model of a truncated simulator which preserves the behaviour of each agent and agent-interaction; formal methods are used to verify/validate these constraints. This formal model is used as a reference for implementing MSimDRAM, our final simulator.