Model checking in a microprocessor design project

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.