Verification of Embedded Memory Systems using Efficient Memory Modeling

TL;DR

This paper presents an efficient verification method for embedded memory systems that combines memory modeling with proof-based abstraction, enabling bug detection and correctness proofs in complex multi-memory systems.

Contribution

It extends previous EMM techniques to multi-memory systems with multiple ports and integrates proof-based abstraction for correctness verification.

Findings

Effective verification on industry designs

Able to find real bugs in embedded memory systems

Provides inductive correctness proofs using SAT-based BMC

Abstract

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.