Reproducing Synchronization Bugs with Model Checking
In this paper we describe our experience in reproducing synchronization bugs using a model checker. We demonstrate how model checking technology can be utilized for more than just model checking. Synchronization bugs are caused by physical phenomena which cause the actual behavior of a chip to be different than predicted according to the functional model. Traditionally, verification methods such as dynamic simulation and model checking use a synchronous model, whereas the actual behavior is according to an asynchronous model. Because of this, synchronization bugs are very hard to trace. Using a model checker we were able to create a model closer to the actual behavior, and retrace many synchronization bugs. Because model checking allows us to introduce non-determinism when checking a VLSI design, and because of its ability to produce counter examples for specifications that fail, we find that model checking is the ideal tool for reproducing synchronization bugs.
- 1.L. Glasser and D. Dopperpuhl. The design and analysis of VLSI circuits. Addison-Wesley, 1985.Google Scholar
- 2.K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.Google Scholar
- 3.The RuleBase homepage at IBM: http://www.haifa.il.ibm.com/projects/verification/RB_homepage/.