Simple Dependent Types in Architecture Specification Languages
Alastair Reid - 10th January 2024
Speaker's Website: https://alastairreid.github.io/
Alastair Reid is a Senior Principal Research Engineer at Intel Strategic CAD Labs. He has previously worked at companies such as Google, where he lead research into the verification of Rust programs, and Arm, where he focused on specifications, developing a language for formally specifying the Arm architecture and a methodology to verify CPUs against this specification. Alastair has a PhD from the University of Glasgow and has sat on the Haskell Design Committee, as well as having over 30 publications and 20 patents.
Over the last 15 years or so, the notation used to specify the behaviour of CPUs has been evolving from being nothing more than a documentation convention to proper programming languages with a well defined syntax, a type system, a semantics. Uses have expanded from just documentation to include formal verification of hardware, test generation, measuring test coverage, generating simulators, and more. To support these uses, tool support has evolved from just vim/emacs to include interpreters, compilers, Verilog generation, bounded model checkers and more.
This talk will look at one small part of the toolchain: the typesystems of two hardware specification languages. These typesystems are a simple form of dependent type system with influences from “Liquid Types”. I will look at the goals of the typesystems, the design choices and their implementation. My hope is to explain why you might want this form of typesystem in these languages but also to help you understand whether you want this form of typesystem in the languages that you will design yourselves.
This talk will look at one small part of the toolchain: the typesystems of two hardware specification languages. These typesystems are a simple form of dependent type system with influences from “Liquid Types”. I will look at the goals of the typesystems, the design choices and their implementation. My hope is to explain why you might want this form of typesystem in these languages but also to help you understand whether you want this form of typesystem in the languages that you will design yourselves.