Verification of Pipelined Microprocessors Using Invariants

Mustapha Bourahla

Computer Science Departement, University of Biskra

BP. 145, Biskra, Algeria, 07000

e-mail: mbourahla@hotmail.com

Mohamed Benmohamed

Computer Science Departement, University of Constantine

Constantine, Algeria, 25000

e-mail: ibnm@yahoo.fr

Abstract: This paper presents a new approach for the verification of a pipelined microprocessor which is based on the definition of invariants to characterize the reachable states of the pipelined machine. To express many machine-relevant properties, we have modeled the stream of instructions with the system Maude which is based on Rewriting Logic. It is also used to run and debug the pipelined machine specification. The meta-level module ITP (Inductive Theorem Prover) is used to verify the pipelined machine properties, presented as its object level specification, and eventually to verify a complete pipelined machine design, whose correctness is defined using the idea of pipeline flushing.

Keywords: Formal Verification, Rewriting Logic, Formal Specification, Pipelined Microprocessors.