Abstract
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).
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
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.
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.
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.
Bryant, R. E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. on Comp., 35(8):677–691, 1986.
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.
Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In Proc. of Work. on Computer-Aided Verification, 1994.
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In Proc. of Symp. on Principles of Programming Languages, 1992.
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.
Corella, F.: Automated high-level verification against clocked algorithmic specifications. In D. Agnew, et al., ed., Proc. of CHDL, North-Holland, 1993.
Corella, F.: Automated verification of behavioral equivalence for microprocessors. IEEE Trans. on Comp., 43(1):115–117, 1994.
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.
Coudert, O., Madre, J. C.: A Unified Framework for the Formal Verification of Sequential Circuits. In Proc. of ICCAD, 1990.
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.
Filkorn, T., Payer, M., Warkentin, P.: Symbolic verification of high-level synthesis results from CALLAS. In Proc. of High-level Synthesis Workshop, 1993.
Gordon, M.J.C., Melham, T.F.: An Introduction to HOL. Cambridge University Press, 1993.
Gupta, A.: Formal Hardware Verification Methods: A Survey. Formal Methods in System Designs, 1:151–238, 1992.
Joyce, J.J.: Multi-level verification of microprocessor-based systems. PhD thesis, University of Cambridge, Computer Laboratory, May 1990.
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.
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.
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.
Langevin, M., Cerny, E.: An extended OBDD representation for extended FSMs. In Proc. of EDAC-ETC-EUROASIC, 1994.
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.
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.
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.
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.
Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In Proc. of the Symp. on Principles of Programming Languages, 1986.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Corella, F., Langevin, M., Cerny, E., Zhou, Z., Song, X. (1995). State enumeration with abstract descriptions of state machines. In: Camurati, P.E., Eveking, H. (eds) Correct Hardware Design and Verification Methods. CHARME 1995. Lecture Notes in Computer Science, vol 987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60385-9_9
Download citation
DOI: https://doi.org/10.1007/3-540-60385-9_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60385-6
Online ISBN: 978-3-540-45516-5
eBook Packages: Springer Book Archive