Microprocessor Specification in Hawk
John Matthews, John Launchbury, and Byron Cook

Modern microprocessors require an immense investment of time and effort to create and verify, from the high-level architectural design downwards. We are exploring ways to increase the productivity of design engineers by creating a domain-specific language for specif ying and simulating processor architectures. We believe that the structuring princ iples used in modern functional programming languages, such as static typing, para metric polymorphism, first-class functions, and lazy evaluation provide a good formalism for such a domain-specific language, and have made initial progress by creating a library on top of the functional language Haskell. We have specified the integer subset of an out-of-order, superscalar DLX microprocessor, with register-renaming, a reorder buffer, a global reservation station, multiple execution units, and speculative branch execution. Two key abstractions of this library are the signal abstract data type (ADT), which models the simulation history of a wire, and the transaction ADT, whi ch models the state of an entire instruction as it travels through the microprocessor.


Fri Aug 15 09:11:27 PDT 1997