Validation with guided search of the state space

ABSTRACT

In practice, model checkers are most useful when they find bugs, not when they prove a property. However, because large portions of the state space of the design actually satisfy the specification, model checkers devote much effort verifying correct portions of the design. In this paper, we enhance the bug-finding capability of a model checker by using heuristics to search the states that are most likely to lead to an error, first. Reductions of 1 to 3 orders of magnitude in the number of states needed to find bugs in industrial designs have been observed. Consequently, these heuristics can extend the capability of model checkers to find bugs in designs.

REFERENCES

• 1: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 2: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 3: David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
• 4: R. W. Hamming. Error Detecting and Error Correcting Codes. Bell System Tech Journal, 9: 147-160, April 1950.
• 5: Richard C. Ho , C. Han Yang , Mark A. Horowitz , David L. Dill, Architecture validation for processors, Proceedings of the 22nd annual international symposium on Computer architecture, p.404-413, June 22-24, 1995, S. Margherita Ligure, Italy
• 6: J. Kuskin , D. Ofelt , M. Heinrich , J. Heinlein , R. Simoni , K. Gharachorloo , J. Chapin , D. Nakahira , J. Baxter , M. Horowitz , A. Gupta , M. Rosenblum , J. Hennessy, The Stanford FLASH multiprocessor, Proceedings of the 21ST annual international symposium on Computer architecture, p.302-313, April 18-21, 1994, Chicago, Illinois, United States
• 7: F. Maruyama, M. Fujita, Hardware Verification, Computer, vol. 18, no. 2, pp 22-32, Feb 1985.
• 8: K. L. McMillan, Symbolic Model Checking. Ph.D. thesis, School of Computer Science, Carnegie Mellon University, May 1992.
• 9: Andreas G. Nowatzyk , Michael C. Browne , Edmund J. Kelly , Michael Parkin, S-connect: from networks of workstations to supercomputer performance, Proceedings of the 22nd annual international symposium on Computer architecture, p.71-82, June 22-24, 1995, S. Margherita Ligure, Italy
• 10: Andrew S. Tanenbaum, Computer Networks, Prentice Hall PTR, Upper Saddle River, NJ, 1985
• 11: C.H. Yang, D. L. Dill, SpotLight: Best-First Search of FSM State Space. IEEE International High Level Design Validation and Test Workshop, presented on November 16, 1996,_http:/!verifv.stanford.edulhvan}~/hldvtSlides.m
• 12: Jun Yuan , Jian Shen , Jacob A. Abraham , Adnan Aziz, On Combining Formal and Informal Verification, Proceedings of the 9th International Conference on Computer Aided Verification, p.376-387, June 22-25, 1997

INDEX TERMS

Primary Classification:
  B. Hardware
  B.8 Performance and Reliability

Additional Classification:
  C. Computer Systems Organization

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.8 Problem Solving, Control Methods, and Search
          Subjects: Heuristic methods

  J. Computer Applications

General Terms:
Algorithms, Design, Experimentation, Measurement, Performance, Theory

Keywords:
guided search, model checking, verification