A Mechanized Refinement Framework for Analysis of Custom Memories

We present a framework for formal verification of embedded custom memories. Memory verification is complicated by the difficulty in abstracting design parameters induced by the inherently analog nature of transistor-level designs. We develop behavioral formal models that specify a memory as a system of interacting state machines, and relate such models with an abstract read/write view of the memory via refinements. The operating constraints on the individual state machines can be validated by readily available data from analog simulations. The framework handles both static RAM (SRAM) and flash memories, and we show initial results demonstrating its applicability.