Modeling and verification of industrial flash memories

Author

Ray, Sandip ; Bhadra, Jayanta ; Portlock, Thomas ; Syzdek, Ronald

Author_Institution

Dept. of Comput. Sci., Univ. of Texas at Austin, Austin, TX, USA

fYear

2010

fDate

22-24 March 2010

Firstpage

705

Lastpage

712

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.

Keywords

electronic engineering computing; formal verification; logic design; logic gates; transistors; behavioral abstraction; floating gate; formal functional verification; industrial flash memories; split gate device; switch-level abstraction; transistor; Abstracts; Computer industry; Computer science; Electronic mail; Flash memory; Microprocessors; Nonvolatile memory; Random access memory; Split gate flash memory cells; Switches; equivalence checking; formal analysis; simulation; spice; theorem proving;

fLanguage

English

Publisher

ieee

Conference_Titel

Quality Electronic Design (ISQED), 2010 11th International Symposium on

Conference_Location

San Jose, CA

ISSN

1948-3287

Print_ISBN

978-1-4244-6454-8

Type

conf

DOI

10.1109/ISQED.2010.5450498

Filename

5450498