Verification of Finite-State-Machine Refinements Using a Symbolic Methodology

  • Stefan Hendricx
  • Luc Claesen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


The top-down design of VLSI-systems typically features a step-wise refinement of intermediate solutions. Even though these refinements do usually not preserve time-scales, current formal verification approaches are largely based on the assumption that both specification and implementation utilize the same scales of time. In this paper, a symbolic methodology is presented to verify the step-wise refinement of finite state machines, allowing for possible differences in timing-granularity.


  1. 1.
    P. Camurati and P. Prinetto. Formal Verification of Hardware Correctness: Introduction and Survey of Current Research. IEEE Computer, 21(7):8–19, July 1988.Google Scholar
  2. 2.
    T. Coe, Mathisen, T., C. Moler, and V. Pratt. Computational Aspects of the Pentium Affair. IEEE Computational Science & Engineering, pages 18–31, spring 1995.Google Scholar
  3. 3.
    S. Hendricx and L. Claesen. Symbolic Multi-Level Verification of Refinement. In Nineth Great Lakes Symposium on VLSIAnn ArborMI 4-6 March 1999. IEEE Computer Society Press.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Stefan Hendricx
    • 1
  • Luc Claesen
    • 1
  1. 1.Imec vzw/Katholieke Universiteit LeuvenHeverleeBelgium

Personalised recommendations