Verification of Pipelined Microprocessors Using Invariants
Mustapha Bourahla, Mohamed Benmohamed · 2003
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 modelled 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.