Functional Hardware Design and Verification Revisited
Mary Sheeran · 2023
I have long been fascinated by the problem of how to describe and reason about regular algorithms, and especially those that are well suited to direct implementation as circuits. I use higher order functions to capture circuit structure, and I argue for the use of correctness preserving transformations. An important class of transformations enables trade-offs between space and time. I keep coming back to the problem of folding circuits or indeed programs so that they fit into less space or onto a given architecture. This problem seems to crop up all over the place, for example when colleagues at DeepMind fold huge programs implementing language models onto available hardware, or in Carl Seger's Thor system for hardware design by transformation, presented at NANDA last year. So I think it is time to tackle these transformations, and programming language support for them, again, since I am not satisfied with my earlier attempts. In this talk, I will concentrate on circuits, and will present first steps towards verified circuit folding. A key aim is to design transformations that allow as much as possible of the resulting verification to be done using combinational rather than sequential verification.