A Formal Specification of Some User Mode Instructions for The Motorola 68020
Robert S. Boyer, Yuan Yu · 1992
. We present a formal specification of approximately 80% of the `user mode' instructions of the Motorola MC68020 microprocessor. The specification is given in the form of definitions in the logic of Nqthm, the Boyer-Moore system. The definitions are displayed in a conventional mathematical syntax. The specification has been used in the mechanical verification of several dozen machine code programs, whose binary was generated by `industrial strength' C and Ada compilers. 1 Introduction This report contains a formal specification of approximately 80% of the `user mode' instructions of the Motorola MC68020 microprocessor. An earlier report [3] describes how we have used this specification to prove mechanically the correctness of several dozen machine code programs, most of them generated by `industrial strength' compilers for C or Ada. Our specification is based upon the user's manual for the MC68020 [4]. The function definitions below are ordered so that a function is defined before it...