This paper presents status results of a microprocessor verification project.
The authors verify a complete 32-bit RISC microprocessor including the
floating point unit and the control logic of the pipeline. The paper
describes a formal definition of a ''correct'' microprocessor. This
correctness criterion is proven for an implementation using formal methods.
All proofs are verified mechanically by means of the theorem proving system
PVS.