Verification of embedded memory systems using efficient memory modeling

Malay K. Ganai, Aarti Gupta, Pranav Ashar

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Scopus citations


We describe verification techniques for embedded memory systems using efficient memory modeling (EMM), without explicitly modeling each memory bit. We extend our previously proposed approach of EMM in Bounded Model Checking (BMC) for a single read/write port single memory system, to more commonly occurring systems with multiple memories, having multiple read and write ports. More importantly, we augment such EMM to providing correctness proofs, in addition to finding real bugs as before. The novelties of our verification approach are in a) combining EMM with proof-based abstraction that preserves the correctness of a property up to a certain analysis depth of SAT-based BMC, and b) modeling arbitrary initial memory state precisely and thereby, providing inductive proofs using SAT-based BMC for embedded memory systems. Similar to the previous approach, we construct a verification model by eliminating memory arrays, but retaining the memory interface signals with their control logic and adding constraints on those signals at every analysis depth to preserve the data forwarding semantics. The size of these EMM constraints depends quadratically on the number of memory accesses and the number of read and write ports; and linearly on the address and data widths and the number of memories. We show the effectiveness of our approach on several industry designs and software programs.

Original languageEnglish (US)
Title of host publicationProceedings - Design, Automation and Test in Europe, DATE '05
Number of pages6
StatePublished - 2005
EventDesign, Automation and Test in Europe, DATE '05 - Munich, Germany
Duration: Mar 7 2005Mar 11 2005

Publication series

NameProceedings -Design, Automation and Test in Europe, DATE '05
ISSN (Print)1530-1591


OtherDesign, Automation and Test in Europe, DATE '05

All Science Journal Classification (ASJC) codes

  • General Engineering


Dive into the research topics of 'Verification of embedded memory systems using efficient memory modeling'. Together they form a unique fingerprint.

Cite this