Verification of Finite-State-Machine Refinements Using a Symbolic Methodology
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.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.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.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