Generation of Compiler Backends from Formal Models of Hardware

TL;DR

This paper proposes automatically generating compiler backends from formal hardware models, enhancing optimization, correctness, and development efficiency, demonstrated through case studies on machine learning accelerators and FPGA mapping.

Contribution

It introduces a novel approach of deriving compiler backends from formal hardware models using automated reasoning, which improves performance and correctness.

Findings

Increased optimization capabilities for hardware accelerators.

Stronger correctness guarantees for generated compiler backends.

Reduced development time for hardware-specific compiler components.

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.