Title :
Abstracting and verifying flash memories
Author :
Ray, Sandip ; Bhadra, Jayanta
Author_Institution :
Univ. of Texas at Austin, Austin, TX, USA
Abstract :
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.
Keywords :
NAND circuits; NOR circuits; SPICE; flash memories; formal verification; integrated circuit design; integrated circuit testing; logic testing; system-on-chip; transistor circuits; NAND flash memory core; NOR flash memory core; SPICE simulation; SoC design; analog simulation; capacitive coupling; flash memory design; floating gate; formal verification; switch-level abstraction; transistor network; Analytical models; Equations; Flash memory; Formal verification; Information retrieval; Logic arrays; Microprocessors; Nonvolatile memory; SPICE; Switches;
Conference_Titel :
Non-Volatile Memory Technology Symposium, 2008. NVMTS 2008. 9th Annual
Conference_Location :
Pacific Grove, CA
Print_ISBN :
978-1-4244-3659-0
Electronic_ISBN :
978-1-4244-2411-5
DOI :
10.1109/NVMT.2008.4731203