Verifying a Simple Pipelined Microprocessor Using Maude

Abstract. We consider the verification of a simple pipelined microprocessor in Maude, by implementing an equational theoretical model of systems. Maude is an equationally-based language, with an efficient term rewriting implementation, and effective meta-level tools. Microprocessors and other systems are modelled as iterated maps operating in time e state-set, and are related by means of data and abstraction maps, and correctness is reduced to state exploration by the choice of an appropriate initialisation function, ensuring/enforcing consistency of the initial state.

• Type: Conference
• Year: 2001
• Where: WADT
• Authors: Neal A. Harman
• Keywords: Equational Theoretical Model, Simple Pipelined Microprocessor, Software Engineering, Term Rewriting Implementation, WADT 2001