Efficient Memory Modeling in BMC
Designs with large embedded memories are quite common and have wide application. However, these embedded memories add further complexity to formal verification tasks due to an exponential increase in state space with each additional memory bit. In typical BMC approaches [45, 66, 109, 178], the search space increases with each time-frame unrolling of a design. With explicit modeling of large embedded memories, the search space frequently becomes prohibitively large to analyze beyond a small depth. In order to make BMC more useful, it is important to have some abstraction of these memories. However, for finding real bugs, it is sufficient that the abstraction techniques capture the memory semantics  without explicitly modeling each memory bit.
KeywordsClock Cycle Memory Modeling Memory Module Read Data Data Width
Unable to display preview. Download preview PDF.