A functional approach to formal hardware verification: the MTI experience

The authors present the application of formal verification techniques to the MTI (Microprocesseur a test integre) microprocessor. The device is described and verified using a functional model. The authors note that the application is a real, rather than a verification-oriented microprocessor, whose description was available to them under the form of schematic and timing diagrams and as output of CAD (computer-aided design) tools. The effort is two-fold: (1) the authors verify the MTI microprocessor, finding some subtle bugs which had escaped the designers´ attention, and (2) they develop a methodology whose applicability ranges beyond the particular case it has been demonstrated on