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.