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 [179] without explicitly modeling each memory bit.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Rights and permissions
Copyright information
© 2007 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
(2007). Efficient Memory Modeling in BMC. In: SAT-Based Scalable Formal Verification Solutions. Series on Integrated Circuits and Systems. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-69167-1_7
Download citation
DOI: https://doi.org/10.1007/978-0-387-69167-1_7
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-69166-4
Online ISBN: 978-0-387-69167-1
eBook Packages: Computer ScienceComputer Science (R0)