Verification of Embedded Memory Systems using Efficient Memory Modeling

Details Verification of Embedded Memory Systems using Efficient Memory Modeling Verification of Embedded Memory Systems using Efficient Memory Modeling

2007-10-25

arxiv.org/abs/0710.4666v1

Dans Design, Automation and Test in Europe - DATE'05, Munich : Allemagne (2005)

Computer Science

Logic in Computer Science

Submitted on behalf of EDAA (http://www.edaa.com/)

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Verification of Embedded Memory Systems using Efficient Memory Modeling does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Verification of Embedded Memory Systems using Efficient Memory Modeling, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verification of Embedded Memory Systems using Efficient Memory Modeling will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-431706