TY  - GEN
AB  - 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.
AD  - Oregon Graduate Institute of Science and Technology
AU  - Matthews, John
DA  - 2000
DO  - 10.6083/M45718Z1
DO  - DOI
ED  - Launchbury,  John
ED  - Advisor
ID  - 107
KW  - Microcomputers
KW  - design
KW  - microprocessors
KW  - functional programming languages
KW  - computer hardware description languages
L1  - https://digitalcollections.ohsu.edu/record/107/files/107_etd.pdf
L2  - https://digitalcollections.ohsu.edu/record/107/files/107_etd.pdf
L4  - https://digitalcollections.ohsu.edu/record/107/files/107_etd.pdf
LK  - https://digitalcollections.ohsu.edu/record/107/files/107_etd.pdf
N2  - 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.
PB  - Oregon Graduate Institute of Science and Technology
PY  - 2000
T1  - Algebraic specification and verification of processor microarchitectures
TI  - Algebraic specification and verification of processor microarchitectures
UR  - https://digitalcollections.ohsu.edu/record/107/files/107_etd.pdf
Y1  - 2000
ER  -