Functional Programming for Hardware Design
For decades I’ve pursued a simple yet powerful idea: that functional programming can revolutionize how we design, verify, and optimize digital hardware. This talk chronicles that journey from early PAL/PLA fuse-based chips used for glue logic, to modern machine learning inference accelerators running on FPGAs and custom silicon chips, and highlights the ways in which functional approaches outperform conventional hardware design methods. Along the way I will describe some of the hardware that was designed and verified using the Bluespec language and DSLs written in Haskell e.g. high speed sorters and machine learning inference chips.
Looking forward, I’ll discuss how proof assistants like Agda might enable an old paradigm in a new context: refining circuit implementations directly from formal specifications using equational reasoning, following the vision of Richard Bird and Lambert Meertens. Recent breakthroughs in machine learning for proof automation make this approach increasingly practical, handling tedious algebraic transformations while allowing hardware designers to focus on high-level architectural decisions.
Satnam Singh was a Fellow at Groq where he applied the power of functional programming languages to the design of machine learning chips and their programming models. Satnam Singh previously worked at Google (machine learning chips, cluster management), Facebook (Android optimization), Microsoft (parallel and concurrent programming) and Xilinx (Lava DSL for hardware design, formal verification of hardware). He started his career as an academic at the University of Glasgow (FPGA-based application acceleration and functional programming, software-defined radio).
His research interests include functional programming in Haskell, high level techniques for hardware design (Lava, Bluespec, DSLs in Haskell, Coq, Agda and C#), formal methods (SAT-solvers, model checkers, theorem provers), formally verified hardware/software co-design, FPGAs, and concurrent and parallel programming.
He is a Senior Member of the ACM and IEEE and a Fellow of the IET. He is also an elected member of IFIP WG2.8 (functional programming) and IFIP WG2.11 (program generation). He previously served as an elected member of ACM SIGPLAN. He has held part-time or honorary positions at The University of Birmingham, Imperial College London, the University of Washington, and the University of Santa Cruz (UCSC).