Abstracting and verifying flash memories

We present a framework for formal verification of flash cores. Flash memories cannot be verified by traditional switch-level abstractions, due to capacitive coupling induced by the presence of floating gates. We discuss a new approach to abstracting transistor networks that is agnostic to the type of transistor used in the implementation. We show how to use this abstraction to model flash memory designs. The abstractions are used for functional verification of memory cores, and can be validated through analog simulation. We have used the approach in the verification of representative NOR and a NAND flash memory cores.