Post-model validation of victim DRAM caches

Formal modeling and analysis of a victim DRAM cache has already been discussed in the existing literature. These works use interacting state machines to model states and transitions of a victim DRAM cache. In this work, we address model-code conformance between a formal model of the victim DRAM cache and a simulator obtained from it. Our work focuses on a two-step approach to validate a DRAM cache implementation. In the first step, we use a technique based on it Feedback-Directed Random Testing to reverse engineer the state models from the execution traces. This process helps us to match the implementation with the state machines associated with the formal model and to verify some of the state-based properties. In the second step, we instrument the implementation with monitors and validate the liveness and safety properties (during run-time) which have been proved earlier in the formal model.