Modeling and Verification of Industrial Flash Memories

Sandip Ray1,  Jayanta Bhadra2,  Thomas Portlock3,  Ronald Syzdek3
1University of Texas at Austin, 2Freescale Semiconductor Inc., 3Freescale Semiconductor Inc


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.