Abstract
In this paper a solution for property verification of synchronous VHDL designs is introduced, and an efficient symbolic model checker is implemented. The model checker applies the feature of synchronous circuit design and the locality feature of property to reduce the size of the state space of the internal finite state machine (FSM) model, thus speeding up the reachability analysis and property checking of circuits. A counterexample generation mechanism is also implemented. We have used the implemented model checker to verify several benchmark circuits; the experimental results contrast with another well-known model checker and demonstrate that our solution is more practicable.
This work was supported by Chinese National Key Fundamental Research and Development Plan (973) under Grant No. G1998030404.
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.
Reference
J. R. Burch, E. M. Clarke, and D. E. Long, “Symbolic model checking with partitioned transition relations”, In Proc. International Conference of VLSI, Aug. 1991.
K. L. McMillan, “The SMV System”, Technical Report, School of Computer Science, CMU, 1992.
C. Delgado Kloos and P. Breuer, editors. Formal Semantics for VHDL, volume 307 of Series in Engineering and Computer Science. Kluwer Academic Publishers, 1995.
D. Deharbe and D. Borrione. Semantics of a verification-oriented subset of VHDL. In P.E. Camurati and H. Eveking, editors, CHARME’95: Correct Hardware Design and Verification Methods, volume 987 of Lecture Notes in Computer Science, Frankfurt, Germany, October 1995. Springer Verlag.
IEEE, “IEEE Standard VHDL Language Reference Manual”, Std 1076–1993, 1993.
J. R. Burch, E. M. Clarke, D. E. Long, et al, “Symbolic model checking for sequential circuit verification”, in IEEE Trans. On Computer-Aided Design of Integrated Circuits and Systems, Vol. 13, NO. 4, pp. 401–424, April 1994.
O. Caudate, C. Berthed, and J. C. Madder, “Verification of sequential machines using functional vectors”, In International Workshop on Applied Formal Methods for Correct VLSI Design, volume VLSI Design Methods-II, pages 179–196, 1990.
E. M. Clarke, O. Grumberg, K. L. McMillan, et al, “Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking”, 32nd Design Automatic Conference, 1995.
R. Lipsett, C. F. Schaefer, C. Ussery, “VHDL: Hardware Description and Design”, Kluwer Academic Publishers, 1989.
Jinsong Bei, Jinian Bian, Hongxi Xue et al. “FSM Modeling of Synchronous VHDL Design for Symbolic Model Checking”, In Proceedings of ASP-DAC’99, Hong Kong, 1999, 363–366.
R.P.Kurshan, Bell Laboratories, Murray Hill, “Formal Verification In a Commercial Setting”, In Proceedings of 34th ACM/IEEE Design Automation Conference, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer Science+Business Media New York
About this chapter
Cite this chapter
Fan, Y., Bei, J., Bian, J., Xue, H., Hong, X., Gu, J. (2001). VERIS: An Efficient Model Checker for Synchronous VHDL Designs. In: Ashenden, P.J., Mermet, J.P., Seepold, R. (eds) System-on-Chip Methodologies & Design Languages. Springer, Boston, MA. https://doi.org/10.1007/978-1-4757-3281-8_9
Download citation
DOI: https://doi.org/10.1007/978-1-4757-3281-8_9
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-4901-1
Online ISBN: 978-1-4757-3281-8
eBook Packages: Springer Book Archive