State enumeration with abstract descriptions of state machines

  • F. Corella
  • M. Langevin
  • E. Cerny
  • Z. Zhou
  • X. Song
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)


We propose a theory of abstract descriptions of state machines in a many-sorted first-order logic with abstract and concrete sorts. State variables containing data values have abstract sorts while control state variables have concrete sorts. Data operations are represented by uninterpreted function symbols. The theory provides a foundation for automated state enumeration methods whose complexity is independent of the width of the datapath, and in particular for methods based on Multiway Decision Grahps (MDGs).


State Machine Theorem Prover Function Symbol Reachable State Disjunctive Normal Form 
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.


  1. 1.
    Bartsch, A., Eveking, H., Faerber, H.-J., Keletatchew, M., Pinder, J., Schellin, U.: LOVERT — A logic verifier of register-transfer level description. In L. Claesen, ed., Proc. of Int. Work. on Applied Formal Methods for Correct VLSI Design, North-Holland, 1989.Google Scholar
  2. 2.
    Borrione, D., Camurati, P., Prinetto, P., Paillet, J.-L.: Functional approaches applied to microprogrammed architectures. Int. Journal of Computer Aided VLSI Design, 2(4):339–358, 1990.Google Scholar
  3. 3.
    Bronstein, A.: MLP: String-Functional Semantics and Boyer-Moore Mechanization for the Formal Verification of Synchronous Circuits. PhD thesis, Stanford University, Department of Computer Science, 1989.Google Scholar
  4. 4.
    Bryant, R. E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. on Comp., 35(8):677–691, 1986.Google Scholar
  5. 5.
    Burch, J. R., Clarke, E. M., Long, D. E., McMillan, K. L., Dill, D. L.: Symbolic model checking for sequential circuit verification. IEEE Trans. on CAD, 13(4):401–424, 1994.Google Scholar
  6. 6.
    Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In Proc. of Work. on Computer-Aided Verification, 1994.Google Scholar
  7. 7.
    Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In Proc. of Symp. on Principles of Programming Languages, 1992.Google Scholar
  8. 8.
    Cho, H., Hachtel, G.D., Jeong, S.-W., Plessier, B., Schwarz, E., Somenzi, F.: ATPG Aspects of FSM Verification. In Proc. of ICCAD, pp. 134–137, 1990.Google Scholar
  9. 9.
    Corella, F.: Automated high-level verification against clocked algorithmic specifications. In D. Agnew, et al., ed., Proc. of CHDL, North-Holland, 1993.Google Scholar
  10. 10.
    Corella, F.: Automated verification of behavioral equivalence for microprocessors. IEEE Trans. on Comp., 43(1):115–117, 1994.Google Scholar
  11. 11.
    Corella, F., Zhou, Z., Song, X., Langevin, M., Cerny, E.: Multiway decision graphs for automated hardware verification. Technical Report RC19676, IBM T. J. Watson Research Center, July 1994.Google Scholar
  12. 12.
    Coudert, O., Madre, J. C.: A Unified Framework for the Formal Verification of Sequential Circuits. In Proc. of ICCAD, 1990.Google Scholar
  13. 13.
    Cyrluk, D., Rajan, S., Shankar, N., Srivar, M.K.: Effective theorem proving for hardware verification. In Int. Conf. on Theorem Provers in Circuit Design, 1994.Google Scholar
  14. 14.
    Filkorn, T., Payer, M., Warkentin, P.: Symbolic verification of high-level synthesis results from CALLAS. In Proc. of High-level Synthesis Workshop, 1993.Google Scholar
  15. 15.
    Gordon, M.J.C., Melham, T.F.: An Introduction to HOL. Cambridge University Press, 1993.Google Scholar
  16. 16.
    Gupta, A.: Formal Hardware Verification Methods: A Survey. Formal Methods in System Designs, 1:151–238, 1992.Google Scholar
  17. 17.
    Joyce, J.J.: Multi-level verification of microprocessor-based systems. PhD thesis, University of Cambridge, Computer Laboratory, May 1990.Google Scholar
  18. 18.
    Kumar, R., Schneider, K., Kropf, T.: Structuring and automating hardware proofs in a higher-order theorem-proving environment. Formal Methods in System Design, 2(2):165–223, 1993.Google Scholar
  19. 19.
    Langevin, M., Cerny, E.: Verification of processor-like circuits. In P. Prinetto and P. Camurati, ed., Proc. of Work. on Correct Hardware Design Methodologies, North-Holland, 1991.Google Scholar
  20. 20.
    Langevin, M., Cerny, E.: Comparing generic state machines. In K. Larsen and A. Skou, ed., Proc. of Work. on Computer-Aided Verification, Springer-Verlag, 1991.Google Scholar
  21. 21.
    Langevin, M., Cerny, E.: An extended OBDD representation for extended FSMs. In Proc. of EDAC-ETC-EUROASIC, 1994.Google Scholar
  22. 22.
    Loewenstein, P.N., Dill, D.L.: Verification of a multiprocessor cache protocol using simulation relations and higher-order logic. Formal Methods in System Design, 1:355–383, 1992.Google Scholar
  23. 23.
    Pierre, L.: The formal proof of sequential circuits described in CASCADE using the Boyer-Moore theorem prover. In L. Claesen, ed., Proc. of Int. Work. on Applied Formal Methods for Correct VLSI Design, North-Holland, 1989.Google Scholar
  24. 24.
    Staunstrup, J., Garland, S.J., Guttag, J.V.: Mechanized verification of circuit descriptions using the Larch Prover. In V. Stavridou, et al., ed., Proc. of Int. Conf. on Theorem Provers in Circuit Design: Theory, Practice and Experience, North-Holland, pp. 277–299, 1992.Google Scholar
  25. 25.
    Touati, H.J., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.: Implicit State Enumeration of Finite State Machines Using BDDs. In Proc. of ICCAD, pp. 130–133, 1990.Google Scholar
  26. 26.
    Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In Proc. of the Symp. on Principles of Programming Languages, 1986.Google Scholar
  27. 27.
    Zhou, Z., Song, X., Corella, F., Cerny, E., Langevin, M.: Partitioning transition relation automatically and efficiently. In Proc. of Great Lakes Symp. on VLSI, 1995.Google Scholar
  28. 28.
    Zhou, Z., Song, X., Corella, F., Cerny, E., Langevin, M., Description and verification of RTL designs using multiway decision graphs. In Proc. of CHDL, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • F. Corella
    • 1
  • M. Langevin
    • 2
  • E. Cerny
    • 3
  • Z. Zhou
    • 3
  • X. Song
    • 3
  1. 1.IBM ResearchUSA
  2. 2.GMD-SETGermany
  3. 3.Univ. de MontréalCanada

Personalised recommendations