Algebraic specification and verification of processor microarchitectures

The Hawk 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 microarchitecture algebra. 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 Isabelle, a higher order logic theorem prover. The laws are used t o 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.