Abstract
In this paper, we explore a parallelization of BMC based on state space partitioning. The parallelization is accomplished by executing multiple instances of BMC independently from di.erent seed states. These seed states are deep states, selected from the reachable states in different partitions. In this scheme, all processors work independently of each other, thus it is suitable for scaling verification to a grid-like network. Our experimental results demonstrate improvement over existing approaches, and show that the method can scale to a large network.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Asato, A., Kadooka, Y.: Grid Middleware for Effectively Utilizing Computing Resources: CyberGRIP. Fujitsu Scientific and Technical Journal 40, 261–268 (2004)
Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19(1), 7–34 (2001)
Ho, P.-H., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J.: Smart Simulation Using Collaborative Formal and Simulation Engines. In: Proc. of the IEEE/ACM International Conference on Computer-Aided Design, November 2000, pp. 120–126 (2000)
Iyer, S., Jain, J., Prasad, M., Sahoo, D., Sidle, T.: Error Detection using BMC in a Parallel Environment. Technical Report, Department of Computer Sciences, University of Texas at Austin (2005)
Sahoo, D., Iyer, S., Jain, J., Stangier, C., Narayan, A., Dill, D.L., Allen Emerson, E.: A Partitioning Methodology for BDD-based Verification. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 399–413. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Iyer, S.K., Jain, J., Prasad, M.R., Sahoo, D., Sidle, T. (2005). Error Detection Using BMC in a Parallel Environment. In: Borrione, D., Paul, W. (eds) Correct Hardware Design and Verification Methods. CHARME 2005. Lecture Notes in Computer Science, vol 3725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560548_30
Download citation
DOI: https://doi.org/10.1007/11560548_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29105-3
Online ISBN: 978-3-540-32030-2
eBook Packages: Computer ScienceComputer Science (R0)