Abstract
SAT-based Bounded Model Checking (BMC), though a robust and scalable verification approach, still is computationally intensive, requiring large memory and time. Interestingly, with the recent development of improved SAT solvers, it is frequently the memory limitation of a single server rather than time that becomes a bottleneck for doing deeper BMC search. 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 worsktation 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 heterogenous workstations interconnected with a standard Ethernet LAN. To illustrate, on an industrial design with 13K FFs and 0.5M gates, the non-disributed BMC on a single workstation (with 4 Gb memory) ran out of memroy after reaching a depth of 120; on the otherhand, our SAT-based distributed BMC over 5 similar workstations was able to go upto 323 steps with a communication overhead of only 30%.
Chapter PDF
Similar content being viewed by others
References
Silburt, A., Evans, A., Vrckovik, G., Diufrensne, M., Brown, T.: Functional Verification of ASICs in Silicon Intensive Systems. Presented at DesignCon 1998 On-Chip System Design Conference (1998)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the Design Automation Conference, pp. 317–320 (1999)
Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Proceedings of Conference on Formal Methods in Computer-Aided Design (2000)
Ganai, M., Aziz, A.: Improved SAT-based Bounded Reachability Analysis. In: Proceedings of VLSI Design Conference (2002)
Abdulla, P.A., Bjesse, P., Een, N.: Symbolic Reachability Analysis based on {SAT}- Solvers. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, p. 411. Springer, Heidelberg (2000)
Marques-Silva, J.P., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers 48, 506–521 (1999)
Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol. 1249, pp. 272–275. Springer, Heidelberg (1997)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of Design Automation Conference (2001)
Ganai, M., Zhang, L., Ashar, P., Gupta, A.: Combining Strengths of Circuit-based and CNF-based Algorithms for a High Performance SAT Solver. In: Proceedings of the Design Automation Conference (2002)
Kuehlmann, A., Ganai, M., Paruthi, V.: Circuit-based Boolean Reasoning. In: Proceedings of Design Automation Conference (2001)
Wah, B.W., Li, G.-J., Yu, C.F.: Multiprocessing of Combinational Search Problems. IEEE computer, 93–108 (1985)
Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems. Journal of Symbolic Computation (1996)
Zhao, Y.: Accelerating Boolean Satisfiability through Application Specific Processing, Ph.D. Thesis. Princeton (2001)
Powley, C., Fergusion, C., Korf, R.: Parallel Heuristic Search: Two Approaches. In: Kumar, V., Gopalakrishnan, P.S., Kanal, L.N. (eds.) Parallel Algorithms for Machine Intelligence and Vision, Springer, New York (1990)
Jurkowiak, B., Li, C.M., Utard, G.: Parallelizing Satz Using Dynamic Workload Balancing. Presented at Workshop on Theory and Applications of Satisfiability Testing (2001)
Boehm, M., Speckenmeyer, E.: A Fast Parallel SAT-solver – Efficient Workload Balancing. Presented at Third International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida (1994)
Stern, U., Dill, D.L.: Parallelizing the Murphi Verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)
Heyman, T., Geist, D., Grumberg, O., Schuster, A.: Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)
Narayan, A., Isles, A., Jain, J., Brayton, R., Sangiovanni-Vincentelli, A.L.: Reachability Analysis using Partitioned-ROBDDs. Presented at International Conference on Computer-Aided Design (1997)
Yadgar, A.: Parallel SAT Solving for Model Checking (2002), http://www.cs.technion.ac.il/~adgar/Research/research.pdf
Davis, M., Longeman, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the ACM 5, 394–397 (1962)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)
Sheeran, M., Singh, S., Stalmarck, G.: Checking Safety Properties using Induction and a SAT Solver. In: Proceedings of Conference on Formal Methods in Computer-Aided Design (2000)
Hasegawa, A., Matsuoka, H., Nakanishi, K.: Clustering Software for Linux-Based HPC. NEC Research & Development 44(1), 60–63 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ganai, M.K., Gupta, A., Yang, Z., Ashar, P. (2003). Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive