Correctness and Verification of Hardware Systems Using Maude
N. A. Harman · 2000
We consider models of hardware systems, within a welldeveloped set of mathematical tools based on an equational, algebraic model. We implement these tools using Maude, an equational, algebraic language with strong meta-language tools and an efficient term rewriting implementation. Maude has the same mathematical basis as the existing formal tools and it is fast. We consider the process of verification, and apply it to a simple illustrative pipeline. Microprocessors, and related systems, are modelled as iterated maps. Initialisation functions act as an invariant when applying one-step theorems to reduce formal verification to state exploration.