Modeling and verification of industrial flash memories

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 tradiwitch-level abstractions for their verification. We nt this problem through behavioral abstractions, which allow formalization of the behaviors of the design acting 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. Keywords--equivalence checking, formal analysis, simulation, spice, theorem proving

• Type: Conference
• Year: 2010
• Where: ISQED
• Authors: Sandip Ray, Jayanta Bhadra, Thomas Portlock, Ronald Syzdek
• Keywords: Flash Memories, Flash Memory Implementations, Hardware, Industrial Flash Memory, ISQED 2010