Efficient modeling of embedded memories in bounded model checking

We describe a viable approach for memory abstraction that preserves memory semantics, thereby augmenting the capability of SAT-based BMC to handle designs with large embedded memory without explicitly modeling each memory bit. Our method does not require examining the design or changing the SAT-solver and is guaranteed not to generate false negatives. The proposed method is similar, but with key enhancements, to the previous abstract interpretation of memory that captures its forwarding semantics, i.e., a data read from a memory location is same as the most recent data written at the same location. In our method, we construct an abstract model for BMC by eliminating memory arrays, but retaining the memory interface signals and adding constraints on those signals at every analysis depth to preserve the memory semantics. The size of these memory-modeling constraints depends quadratically on the number of memory accesses and linearly on the bus widths of memory interface signals. Since the analysis depth of BMC bounds the number of memory accesses, these constraints are significantly smaller than the explicit memory model. The novelty of our memory-modeling constraints is that they capture the exclusivity of a read and write pair explicitly, i.e., when a SAT-solver decides on a valid read and write pair, other pairs are implied invalid immediately, thereby reducing the solve time. We have implemented these techniques in our SAT-based BMC framework where we demonstrate the effectiveness of such an abstraction on a number of hardware and software designs with large embedded memories. We show at least an order of magnitude improvement (both in time and space) using our method over explicit modeling of each memory bit. We also show that our method of adding constraints boosts the performance of the SAT solver (in BMC) significantly as opposed to the conventional way of modeling these constraints as nested if-then-else expressions.