Sciweavers

FMCAD
2007
Springer

A Mechanized Refinement Framework for Analysis of Custom Memories

14 years 1 months ago
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.
Sandip Ray, Jayanta Bhadra
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2007
Where FMCAD
Authors Sandip Ray, Jayanta Bhadra
Comments (0)