The <i>Hawk</i> language is a domain-specific extension
of the pure functional language Haskell, and is used to specify and
reason about processor microarchitectures at a high level of
abstraction. We apply functional language technology and reasoning
principles to concisely specify pipelined microarchitectures in Hawk
and verify them through a domain-specific <i>microarchitecture algebra</i>.
We develop a remarkably simple set of local equational laws
governing processor components such as register files, bypass logic,
and execution units. Many of these laws are verified in <i>Isabell</i>e, a
higher order logic theorem prover. The laws are used to incrementally
simplify a complex pipelined microarchitecture, removing pipeline
stages and simplifying control logic, while retaining cycle-accurate
behavior with respect to the original pipelined design.

<p>Proving these laws requires defining mutually recursive functions over
coinductively defined streams. Such definitions are not directly
supported in current theorem provers. We develop a generalization of
well-founded recursion, called <i>Converging Equivalence Relations</i>,
that allows these definitions to be added conservatively in a
straightforward and modular fashion.</p>