Content area
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. Chip design requires reasoning between different layers of abstraction, however these tools do not provide mechanisms to connect specifications with implementations to ensure correctness. Programming languages for chip design rely on technology-specific components, but lack helpful abstractions needed to support common deployment platforms, making it difficult to adapt and compose designs. And further, the design ecosystem is fragmented between systems and tool chains without the ability to interoperate.
This thesis presents my research on improving chip design tools with automated reasoning techniques. I use program synthesis techniques to bridge the gap between an architectural specification and a low-level hardware implementation, developing a new technique called control logic synthesis. I establish a new field called hardware decompilation, which is about lifting common hardware artifacts to high-level source code, enabling design transpilation and automating the effort of re-targeting designs to different technologies. And finally, to address challenges with technology constraints, I developed a memory design language that uses equational reasoning techniques to automatically target multiple memory technologies from a single interface. Through the application of these automated reasoning techniques, I opened two wholly new areas in the chip design space enabling novel design processes that were not possible before, improving developer agility and design verifiability.