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.


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