Speaker: Satnam Singh, Google AI

This talk is an experience report about a recent exercise using ideas from the world of functional programming to design and implement hardware accelerators and their associated development and programming toolchain in an integrated manner. In particular, having a single Haskell-based representation provided unusually high levels of agility for exploring the design space by rapidly refactoring architectural decisions with confidence in preserving correctness and automatically keeping development tooling in sync. Looking to the future, the ability to derive an implementation from a formal specification opens up the possibility of deriving a correct circuit from a specification by successively applying correctness preserving transformations in an interactive theorem prover. Each of these transformations injects architecture implementation that refines the specification. Finally, this path opens up the possibility of developing machine learning algorithms that can drive a theorem prover to automatically produce an efficient circuit implementation from a human written formal specification.

Speaker bio: Satnam Singh is a software engineer at Google AI working on the design and implementation of hardware using functional programming techniques. He has worked on compiler technology and CAD tools in industry (Xilinx, Microsoft, Google, Facebook, X) and academia (The University of Glasgow).