UC Santa Barbara

Despite all the effort spent in testing, analyzing, and formally verifying software, a program is ultimately only as correct as the underlying hardware on which it runs. As processors become more performant, their microarchitectures become increasingly complex; this complexity often manifests in instruction set architectures (ISAs) that are bloated, imprecise, and therefore unamenable to formal verification. The ISA itself is realized as a hardware implementation written in a hardware description language (HDL). Unfortunately, modern HDLs lack the expressive, composable programming abstractions we’ve come to expect of traditional high-level programming languages, hampering innovation and correct-by-construction hardware design. Furthermore, the unique characteristics of emerging technologies like superconductor electronics (SCE) require us to rethink the HDLs we use and retool the entire design, simulation, and verification stack.

This thesis shows how various programming language techniques, applied to the realm of computer architecture and hardware design, help address these issues. I show that abstraction, formal semantics, and type theory can be used to create an ISA that is precise, concise, and amenable to formal reasoning by both human and machine. I also show how HDLs can better support composability via formalized notions of intermodular communication and dependency. Finally, I show that we can improve SCE behavioral modeling and system design using a new automata-based pulse-transfer level language.