Error Detection Using BMC in a Parallel Environment
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.
KeywordsError Detection Reachable State Deep State Bound Model Check Seed State
- 1.Asato, A., Kadooka, Y.: Grid Middleware for Effectively Utilizing Computing Resources: CyberGRIP. Fujitsu Scientific and Technical Journal 40, 261–268 (2004)Google Scholar
- 3.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)Google Scholar
- 4.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)Google Scholar