Proving the Correctness of a Complete Microprocessor
DanielKroening ChristianJacobi · 2000
Thispaperpresentsstatusresultsofamicroprocessorverificationproject. Theauthorsverifyacomplete32-bitRISCmicroprocessorincludingthefloating pointunitandthecontrollogicofthepipeline.Thepaperdescribesaformaldef initionofacorrectmicroprocessor. Thiscorrectnesscriterionisprovenforan implementation using formal methods. All proofs are verifiedmechanically by meansofthetheoremprovingsystemPVS.