Abstract
BDD-based implicit state enumeration usually fails for systems with wide numeric datapaths. It may be possible to take advantage of higher level structure in designs to improve efficiency. By treating the integer variables as atomic types, rather than breaking them into individual bits, one can perform implicit state enumeration using Presburger arithmetic decision procedures; the complexity of this approach is independent of the width of the datapath. Since BDDs grow with the width of the datapath, we know that at some width BDDs will become less efficient than Presburger techniques. However, we establish that for widths of practical interest, the BDD approach is still more efficient.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
D. A. Basin and N. Klarlund. Hardware verification using monadic second-order logic. In P. Wolper, editor, Proc. Computer Aided Verification, volume 939 of LNCS, pages 31–41. Springer-Verlag, July 1995.
A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In H. Kirchner, editor, Trees and Algebra in Programming-CAAP, volume 1059 of LNCS, pages 30–43. Springer-Verlag, 1996.
R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa. VIS: A system for verification and synthesis. In R. Alur and T. A. Henzinger, editors, Proceedings of the Conference on Computer-Aided Verification, volume 1102 of LNCS, pages 428–432, New Brunswick NJ, July 1996. Springer-Verlag.
J. R. Büchi. On a decision method in restricted second order arithmetic. In Proc. Int. Congress Logic, Methodology, and Philosophy of Science, pages 1–11, Berkeley CA, 1960. Stanford University Press.
T. Bultan, R. Geber, and W. Pugh. Symbolic model checking of infinite state programs using Presburger arithmetic. In O. Grumberg, editor, Proc. Computer Aided Verification, volume 1254 of LNCS, pages 400–411, Haifa, June 1997. Springer-Verlag.
K.-T. Cheng and A. Krishnakumar. Automatic functional test generation using the extended finite state machine model. In Proc. 30th Design Automat. Conf., pages 86–91, June 1993.
E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. in Proc. Principles of Programming Language, Jan. 1992
O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 365–373. Springer-Verlag, June 1989.
D. Cyrluk and P. Narendran. Ground temporal logic: A logic for hardware verification. In D. L. Dill, editor, Proc. Computer Aided Verification, volume 818 of LNCS, pages 247–259, Stanford, CA, June 1994. Springer-Verlag.
P. Godefroid and D. E. Long. Symbolic protocol verification with queue BDDs. In Proc. Logic in Computer Science, pages 198–206, July 1996.
A. Gupta. Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction. PhD thesis, Carnegie Mellon University, 1994. Memorandum No. CMU-CS-94-208.
J. G. Henriksen, J. Jensen, M. JØrgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS’ 95, volume 1019 of LNCS, pages 89–110. Springer-Verlag, May 1995.
R. Hojati and R. K. Brayton. Automatic datapath abstraction in hardware systems. In P. Wolper, editor, Proc. Computer Aided Verification, volume 939 of LNCS, pages 98–113. Springer-Verlag, July 1995.
P. Kelb, T. Margaria, M. Mendler, and C. Gsottberger. MOSEL: A flexible toolset for monadic second-order logic. In TACAS’ 97: Int’l Workshop on Tools and Algorithms for the Construction and Analysis of Systems, volume 1217 of LNCS, pages 183–202. Springer-Verlag, Apr. 1997.
W. Kelly, V. Maslov, W. Pugh, E. Rosser, T. Shpeisman, and D. Wonnacott. The Omega library (Version 1.1.0) interface guide. http://www.cs.umd.edu/projects/omega, Nov. 1996.
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In O. Grumberg, editor, Proc. Computer Aided Verification, volume 1254 of LNCS, pages 424–435. Springer-Verlag, June 1997.
N. Klarlund. An nlogn algorithm for online BDD refinement. In O. Grumberg, editor, Proc. Computer Aided Verification, volume 1254 of LNCS, pages 107–118. Springer-Verlag, June 1997.
A. Krishnakumar and K.-T. Cheng. On the computation of the set of reachable states of hybrid models. In Proc. 31st Design Automat. Conf., pages 615–621, June 1994.
R. P. Kurshan. Analysis of discrete event coordination. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshiop on Stepwise Refinement of Distribute Systems, Models, Formalisms, Correctness, volume 430 of LNCS, pages 414–453. Springer-Verlag, 1989.
R. P. Kurshan and K. L. McMillan. A structural induction theorem for processes. In Proc. Eighth Symp. Princ. of Distributed Computing, pages 239–247, 1989.
H. R. Lewis and C. H. Papadimitriou. Elements of the Theory of Computation. Prentice Hall Englewood Cliffs, New Jersey, 1981.
W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102–114, Aug. 1992.
T. R. Shiple, J. H. Kukula, and R. K. Ranjan. A comparison of Presburger engines for EFSM reachability. In A. Hu and M. Vardi, editors, Proc. Computer Aided Verification, LNCS Vancouver, June 1998. Springer-Verlag.
P. Wolper and B. Boigelot. An automata-theoretic approach to Presburger arithmetic constraints. In Proc. of Static Analysis Symposium, volume 983 of LNCS, pages 21–32. Springer-Verlag, Sept. 1995.
Z. Zhou, X. Song, S. Tahar, E. Cemy, F. Corella, and M. Langevin. Formal verification of the island tunnel controller using multiway decision graphs. In M. Srivas and A. Camilleri, editors, Proc. Formal Methods in Computer-Aided Desigh, volume 1166 of LNCS, pages 233–247. Sringer-Verlag, Nov. 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kukula, J.H., Shiple, T.R., Aziz, A. (1998). Techniques for Implicit State Enumeration of EFSMs. In: Gopalakrishnan, G., Windley, P. (eds) Formal Methods in Computer-Aided Design. FMCAD 1998. Lecture Notes in Computer Science, vol 1522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49519-3_30
Download citation
DOI: https://doi.org/10.1007/3-540-49519-3_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65191-8
Online ISBN: 978-3-540-49519-2
eBook Packages: Springer Book Archive