000000107 001__ 107 000000107 005__ 20251007004804.0 000000107 0247_ $$2DOI$$a10.6083/M45718Z1 000000107 037__ $$aETD 000000107 245__ $$aAlgebraic specification and verification of processor microarchitectures 000000107 260__ $$bOregon Graduate Institute of Science and Technology 000000107 269__ $$a2000 000000107 336__ $$aDissertation 000000107 502__ $$bPh.D. 000000107 520__ $$aThe 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. 000000107 542__ $$fIn copyright - single owner 000000107 650__ $$aMicrocomputers$$022268 000000107 6531_ $$adesign 000000107 6531_ $$amicroprocessors 000000107 6531_ $$afunctional programming languages 000000107 6531_ $$acomputer hardware description languages 000000107 692__ $$aOGI Department of Computer Science and Engineering$$041405 000000107 7001_ $$aMatthews, John$$uOregon Graduate Institute of Science and Technology$$041352 000000107 7201_ $$aLaunchbury, John$$uOregon Graduate Institute of Science and Technology$$041352$$7Personal$$eAdvisor 000000107 8564_ $$9f052edac-d3e8-419a-ac83-1934e681aff3$$s7588301$$uhttps://digitalcollections.ohsu.edu/record/107/files/107_etd.pdf$$ePublic$$2ca1af982e4ae74d4f1e179a429f382ee$$31 000000107 905__ $$a/rest/prod/12/57/9s/24/12579s24j 000000107 909CO $$ooai:digitalcollections.ohsu.edu:107$$pstudent-work 000000107 980__ $$aTheses and Dissertations