Efficient distributed SAT and SAT-based distributed Bounded Model Checking

Malay K. Ganai, Aarti Gupta, Zijiang Yang, Pranav Ashar

Research output: Contribution to journalArticlepeer-review

8 Scopus citations


SAT-based Bounded Model Checking (BMC), though a robust and scalable verification approach, still is computationally intensive, requiring large memory and time. Even with the recent development of improved SAT solvers, the memory limitation of a single server rather than time can become a bottleneck for doing deeper BMC search for large designs. Distributing computing requirements of BMC over a network of workstations can overcome the memory limitation of a single server, albeit at increased communication cost. In this paper, we present (a) a method for distributed SAT over a network of workstations using a Master/ Client model where each Client workstation has an exclusive partition of the SAT problem and uses knowledge of partition topology to communicate with other Clients, (b) a method for distributing SAT-based BMC using the distributed SAT. For the sake of scalability, at no point in the BMC computation does a single workstation have all the information. We experimented on a network of heterogeneous workstations interconnected with a standard Ethernet LAN. To illustrate, on an industrial design with ∼13 K FFs and ∼0.5 million gates, the non-distributed BMC on a single workstation (with 4 GB memory) ran out of memory after reaching a depth of 120; on the other hand, our SAT-based distributed BMC over 5 similar workstations was able to go up to 323 steps with a communication overhead of only 30%.

Original languageEnglish (US)
Pages (from-to)387-396
Number of pages10
JournalInternational Journal on Software Tools for Technology Transfer
Issue number4-5
StatePublished - Aug 2006

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems


  • BMC; SAT
  • Distributed-SAT
  • Formal verification
  • Model checking
  • Parallel SAT


Dive into the research topics of 'Efficient distributed SAT and SAT-based distributed Bounded Model Checking'. Together they form a unique fingerprint.

Cite this