Model checking in a microprocessor design project

  • Geoff Barrett
  • Anthony McIsaac
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


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.


Model Check Finite State Machine Formal Verification Visible Transition Register Transfer Level 
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.


  1. 1.
    Geoff Barrett. Modelling nondeterminism with transition functions. Technical report, ST Internal Report, SHD AX 0.0, 1996.Google Scholar
  2. 2.
    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.Google Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    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.Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Geoff Barrett
    • 1
  • Anthony McIsaac
    • 1
  1. 1.SGS-Thomson Microelectronics LimitedAlmondsburyUK

Personalised recommendations