Generation of Compiler Backends from Formal Models of Hardware

TL;DR

This work argues for automatically generating compiler backends from explicit formal models of hardware using automated reasoning, aiming to improve optimization, correctness, and development time. It presents two concrete efforts: Glenside, a pure tensor IR enabling equality-saturation driven accelerator mapping integrated into 3LA for ML workloads; and Lakeroad, a sketch-guided program-synthesis-based FPGA mapper that imports vendor HDL semantics to produce correct, complete DSP mappings. Together, these case studies demonstrate that explicit hardware models paired with adaptable algorithms yield more accelerator mappings, stronger correctness guarantees, and easier extension to new targets, while enabling end-to-end hardware validation and faster development cycles. The work also outlines Churchroad as a path to scale these ideas to larger hardware designs, arguing that tooling built on explicit models and solver-based optimization can transform hardware/software co-design and technology mapping. Overall, the approach represents a practical blueprint for generating robust, extensible compiler backends by bridging formal hardware models with modern reasoning tools.

Abstract

Compilers convert between representations -- usually, from higher-level, human writable code to lower-level, machine-readable code. A compiler backend is the portion of the compiler containing optimizations and code generation routines for a specific hardware target. In this dissertation, I advocate for a specific way of building compiler backends: namely, by automatically generating them from explicit, formal models of hardware using automated reasoning algorithms. I describe how automatically generating compilers from formal models of hardware leads to increased optimization ability, stronger correctness guarantees, and reduced development time for compiler backends. As evidence, I present two case studies: first, Glenside, which uses equality saturation to increase the 3LA compiler's ability to offload operations to machine learning accelerators, and second, Lakeroad, a technology mapper for FPGAs which uses program synthesis and semantics extracted from Verilog to map hardware designs to complex, programmable hardware primitives.

Figures (23)

• Figure 1: clang compiling high-level C code to target-specific x86 assembly.
• Figure 2: Tensorizing a 2D convolution to VTA moreau2018vta accelerator calls.
• Figure 3: Technology mapping a high-level hardware design to an instantiation of a specific hardware primitive.
• Figure 4: Declaration of x86's imul instruction in LLVM's x86 backend llvmx86tablegen.
• Figure 5: Snippet of code from Yosys's pmgen framework yosysxilinxpmgen attempting to map hardware designs to specific FPGA hardware primitives.

Theorems & Definitions (2)

• Lemma 7.1
• Proof 7.1: Proof of Lemma \ref{['lemma:interp-is-primitive-recursive']}