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.
This work was supported in part by SRC contract 2003-TJ-920.
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
Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science 82(2), 253–284 (1991)
Brayton, R.K., et al.: VIS. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 248–256. Springer, Heidelberg (1996)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
Cormen, T.H., Leiserson, C.E., Rivest, R.L.: An Introduction to Algorithms. McGraw-Hill, New York (1990)
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)
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)
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)
Horwitz, S., Reps, T.: The use of program dependence graphs in software engineering. In: Fourteenth International Conference on Software Engineering (1992)
ITC 1999 benchmark home page, http://www.cerc.utexas.edu/itc99-benchmarks/bench.html
Johnson, D.B.: Finding all the elementary circuits of a directed graph. SIAM Journal on Computing 4, 77–84 (1975)
Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)
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)
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)
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)
Weiser, M.: Program slicing. IEEE Transactions on Software Engineering 10(4), 352–357 (1984)
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
Ward, D., Somenzi, F. (2005). Automatic Generation of Hints for Symbolic Traversal. 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_17
Download citation
DOI: https://doi.org/10.1007/11560548_17
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)