Distributed SAT-Based BMC

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.