Microprocessor Verification in Maude

Neal Harman

(Swansea University)

Basic methods for algebraically representing microprocessors, and their correctness will be introduced. The resulting proof obligations can be substantially simplified if some easily-checked conditions hold. Example verifications of an abstract pipeline, and of a simple pipelined microprocessor have been undertaken using the equational language Maude, based on these simplifications. Maude will be introduced, and ongoing work on these and larger examples, and on reducing the level of manual direction required in proofs, will be discussed.
Thursday 9th December 1999, 15:00
Seminar Room 322
Department of Computer Science