Efficient distributed SAT and SAT-based distributed Bounded Model Checking |
| |
Authors: | Malay K Ganai Aarti Gupta Zijiang Yang Pranav Ashar |
| |
Affiliation: | (1) NEC Laboratories America, Princeton, NJ 08540, USA |
| |
Abstract: | 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%. |
| |
Keywords: | BMC SAT Distributed-SAT Parallel SAT Formal Verification Model Checking |
本文献已被 SpringerLink 等数据库收录! |
|