Advertisement

Automatic Generation of Hints for Symbolic Traversal

  • David Ward
  • Fabio Somenzi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

Abstract

Recent work in avoiding the state explosion problem in hardware verification during breath-first symbolic traversal (BFST) based on Binary Decision Diagrams (BDDs) applies hints to constrain the transition relation of the circuit being verified [14]. Hints are expressed as constraints on the primary inputs and states of a circuit modeled as a finite transition system and can often be found with the help of simple heuristics by someone who understands the circuit well enough to devise simulation stimuli or verification properties for it. However, finding good hints requires one to constrain the transition system so that small intermediate BDDs arise during image computations that produce large numbers of reachable states. Thus, the ease of finding good hints is limited by the user’s ability to predict their usefulness. In this paper we present a method to statically and automatically determine good hints. Working on the control flow graph(s) of a behavioral model of the circuit being analyzed, our algorithm extracts sets of related execution paths. Each set has a corresponding enabling predicate which is a candidate hint. Program slicing is employed to identify execution paths. Abstract interpretation and model checking are used to ascertain properties along these paths. Hints generated automatically using our technique result in orders-of-magnitude reductions in time and space requirements during state space exploration compared to BFST and are usually as good as those produced by someone who understands the circuit.

Keywords

Model Check Abstract Interpretation Reachable State Execution Path Binary Decision Diagram 
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

  1. 1.
    Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science 82(2), 253–284 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Brayton, R.K., et al.: VIS. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 248–256. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  3. 3.
    Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)zbMATHCrossRefGoogle Scholar
  4. 4.
    Cormen, T.H., Leiserson, C.E., Rivest, R.L.: An Introduction to Algorithms. McGraw-Hill, New York (1990)Google Scholar
  5. 5.
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by constructions or approximation of fixpoints. In: Proceedings of the ACM Symposium on the Principles of Programming Languages, pp. 238–250 (1977)Google Scholar
  6. 6.
    Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Transactions on Programming Languages and Systems (TOPLAS) 9(3), 319–349 (1987)zbMATHCrossRefGoogle Scholar
  7. 7.
    Gustafsson, J., Lisper, B., Kirner, R., Puschner, P.: Input-dependency analysis for hard real-time software. In: International Workshop on Object-Oriented Real-Time Dependable System (October 2004)Google Scholar
  8. 8.
    Horwitz, S., Reps, T.: The use of program dependence graphs in software engineering. In: Fourteenth International Conference on Software Engineering (1992)Google Scholar
  9. 9.
  10. 10.
    Johnson, D.B.: Finding all the elementary circuits of a directed graph. SIAM Journal on Computing 4, 77–84 (1975)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)Google Scholar
  12. 12.
    McMillan, K.L.: Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 110–121. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  13. 13.
    Ottenstein, K.J., Ottenstein, L.M.: The program dependence graph in a software development environment. In: Symposium on Practical Software Development Environments, New York, NY, pp. 177–184 (1984)Google Scholar
  14. 14.
    Ravi, K., Somenzi, F.: Hints to accelerate symbolic traversal. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 250–264. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  15. 15.
    Weiser, M.: Program slicing. IEEE Transactions on Software Engineering 10(4), 352–357 (1984)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • David Ward
    • 1
  • Fabio Somenzi
    • 2
  1. 1.IBM Printing Systems Division 
  2. 2.University of Colorado at Boulder 

Personalised recommendations