A Mechanized Refinement Framework for Analysis of Custom Memories

We present a framework for formal verification of embedded custom memories. Memory verification is complicated ifficulty 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 ing 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.

• Type: Conference
• Year: 2007
• Where: FMCAD
• Authors: Sandip Ray, Jayanta Bhadra
• Keywords: Embedded Custom Memories, FMCAD 2007, Formal Methods, Memory Verification, State Machines