Distributed SAT-Based BMC

Part of the Series on Integrated Circuits and Systems book series (ICIR)

SAT-based Bounded Model Checking (BMC), though a robust and scalable verification approach, is still computationally intensive, requiring large memory and time. Even with the many enhancements discussed in Chapter 5, sometimes the memory limitation of a single server, rather than time, can become a bottleneck for doing deeper BMC search on large designs. The main limitation of a standard BMC application is that it can perform search up to a maximum depth allowed by the physical memory on a single server. This limitation stems from the fact that as the search bound k becomes large, the memory requirement due to unrolling of the design also increases. Especially for memory-bound designs, a single server can quickly become a bottleneck in doing deeper search for bugs.


Communication Overhead Single Server Bound Model Check Large Design Quick Sort 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media, LLC 2007

Personalised recommendations