Verified Agile Hardware

Speaker: Jackson Melchert, PhD Student, Stanford University
Date: February 8, 2023

The agile hardware project (AHA) aims to make designing hardware more like designing software, with high automation, fast design cycles, and support for fast and interactive debugging. To achieve hardware-compiler co-design, the AHA flow uses a domain-specific language to specify each accelerator component (processing element, memory element, and interconnect), and from these specifications generates both the hardware description and the compiler collateral for the component. While the current AHA flow can generate a programmable hardware accelerator and its compiler with low design effort, largely missing so far has been an integrated security and verification story. Much as we were able to automate other aspects of the AHA flow, we expect that security and verification can also be automated and integrated in many cases. In this project we will take the first steps towards that vision by automating formal equivalence checking across transformations performed by the compiler. In particular, we aim to show that transformations introduced during mapping, place and route, and bitstream generation preserve functional equivalence. This talk will outline a plan for the project and present the results of our first completed task: formally verifying the compute mapping stage of the compiler.