Abstract
This paper gives an account of the use of model checking in a large-scale microprocessor development project. It describes the tools, methods and techniques used, the way the work was organized, and some of the problems encountered, as well as the results achieved. The verification of a bus arbiter is presented as a case study illustrating the abstraction techniques required in order to achieve results for large designs.
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
Geoff Barrett. Modelling nondeterminism with transition functions. Technical report, ST Internal Report, SHD AX 0.0, 1996.
Ilan Beer, Shoham Ben-David, Cindy Eisner, and Avner Landver. RuleBase: An industry-oriented formal verification tool. In Proceedings of the 33rd Design Automation Conference, Las Vegas, pages 655–660, 1996.
Ilan Beer, Shoham Ben-David, Daniel Geist, Raanan Gewirtzman, and Michael Yoeli. Methodology and system for practical formal verification of reactive hardware. In D.Dill, editor, CAV'94, Lecture Notes in Computer Science 818, pages 182–193, 1994.
Jörg Bormann, Jörg Lohse, Michael Payer, and Gerd Venzl. Model checking in industrial hardware design. In Proceedings of the 32nd Design Automation Conference, San Francisco, pages 298–303, 1995.
Françoise Casaubieilh, Anthony Mclsaac, Mike Benjamin, et al. Functional verification methodology of Chameleon processor. In Proceedings of the 33rd Design Automation Conference, Las Vegas, pages 421–426, 1996.
E.M. Clarke, E. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986.
E.M. Clarke, O. Grumberg, and D.E.Long. Model checking and abstraction. In Proceedings of the 19th Annual ACM Symposium on Principles of Programming Languages, pages 343–354, 1992.
O. Coudert, C. Berthet, and J.C. Madre. Verification of sequential machines using boolean functional vectors. In Proceedings of the Workshop on Applied Formal Methods for Correct VLSI Design, Houlathen, Belgium, November 1989, in Formal VLSI Correctness Verification vol. II. North-Holland, 1990.
A.T. Eiriksson and K.L. McMillan. Using formal verification/analysis methods on the critical path in system design: A case study. In P.Wolper, editor, CAV'95, Lecture Notes in Computer Science 939, pages 367–380. Springer Verlag, 1995.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barrett, G., McIsaac, A. (1997). Model checking in a microprocessor design project. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_22
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive