Modeling and Verification of Industrial Flash Memories
S. Ray, J. Bhadra, T. Portlock, and
R. Syzdek
In P. Chatterjee and K. Gadepally, editors, Proceedings of the 11th International Symposium on Quality
Electronic Design (ISQED 2010), San Jose, CA, March 2010, pages
705-712. IEEE.
© 2009 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 method to abstract, formalize, and verify industrial
flash memory implementations. Flash memories contain specialized
transistors, e.g., floating gate and split gate devices, which
preclude the use of traditional switch-level abstractions for their
verification. We circumvent this problem through behavioral
abstractions, which allow formalization of the behaviors of the design
as interacting state machines. Behavioral abstractions are agnostic
to transistor type, making them suitable for formalizing flash
memories. We have verified industrial flash memory implementations
based on both floating gate and split gate technologies. Our work
provides the first formal functional verification results for
industrial flash memories.
Relevant files