Join us for a Computer Science Seminar at 12:45–1:45 p.m. on Thursday, February 20, 2025, at the Stuart Building, 113. Speaker Zachary Sisco will give a talk titled “Verifiable Hardware Design With Solver-Aided Programming Languages.”

Abstract

Modern chip design embodies enormous complexity, from general-purpose processors to specialized hardware accelerators. With the trend towards specialization, chip designers need techniques that let them quickly iterate over a design while fitting into familiar programming languages and tools. However, designing a chip with speed and robustness remains a challenge, particularly for smaller teams who are increasingly entering the field. As a result, industry studies show roughly half of chip development time is spent on verification.

This talk presents my research on improving hardware design tools with solver-aided programming techniques. By integrating formal methods into language-driven design tools, I show how chip developers overcome design challenges through rich language abstractions and automated verification and synthesis techniques. My work opens two entirely new areas in the chip design space and enables novel design processes based around increasing developer productivity with correctness guarantees. I will give an overview of these new areas, as well as future directions opened up through these solver-aided techniques. Given the high cost of chip development, the new design processes enabled by my research will reduce the cost and effort required to deliver new, specialized computing systems with high assurances. In the era of $500-billion data center projects, the availability of cheaper and more reliable chips can bring enormous value. However, we can only realize this vision if we improve the languages and tools that chip designers use through the dimensions of agility and verifiability.

Biography

Zachary Sisco is a PhD candidate at the University of California, Santa Barbara, advised by Jonathan Balkind and Ben Hardekopf. He conducts research at the intersection of programming languages and computer architecture, integrating formal methods into open-source languages for chip design to increase developer agility with correctness guarantees. His work is published in top-tier venues such as PLDI and ASPLOS and was awarded silver in the ACM Student Research Competition at PLDI. To learn more about his work, please visit zsisco.net.