Abstracting and Verifying Flash Memories

S. Ray and J. Bhadra

In K. Campbell, editor, Proceedings of the 9th Non-Volatile Memory Technology Symposium (NVMTS 2008), Pacific Grove, CA, November 2008, pages 100-104. IEEE.

© 2008 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

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.

Relevant files


BibTex

@Inproceedings{ray-abstracting,
  author    = "S. Ray and J. Bhadra",
  title     = "{Abstracting and Verifying Flash Memories}",
  editor    = "K. Campbell",
  booktitle = "{Proceedings of the $9$th Non-Volatile Memory 
                Technology Symposium (NVMTS 2008)}",
  address   = "{Pacific Grove, CA}",
  month     = nov,
  pages     = "100-104",
  year      = 2008,
  publisher = "IEEE"
}