Scaling Program Synthesis Based Technology Mapping with Equality Saturation

TL;DR

This paper introduces Churchroad, a new FPGA hardware mapping tool that combines equality saturation with program synthesis, eliminating the need for user sketches and improving handling of complex designs.

Contribution

It presents a novel approach integrating equality saturation with program synthesis to enhance FPGA design mapping without requiring user-provided sketches.

Findings

Handles larger and more complex designs than previous tools

Eliminates the need for user sketches in the mapping process

Improves efficiency of hardware mapping for FPGA designs

Abstract

State-of-the-art hardware compilers for FPGAs often fail to find efficient mappings of high-level designs to low-level primitives, especially complex programmable primitives like digital signal processors (DSPs). New approaches apply sketch-guided program synthesis to more optimally map designs. However, this approach has two primary drawbacks. First, sketch-guided program synthesis requires the user to provide sketches, which are challenging to write and require domain expertise. Second, the open-source SMT solvers which power sketch-guided program synthesis struggle with the sorts of operations common in hardware -- namely multiplication. In this paper, we address both of these challenges using an equality saturation (eqsat) framework. By combining eqsat and an existing state-of-the-art program-synthesis-based tool, we produce Churchroad, a technology mapper which handles larger and more complex designs than the program-synthesis-based tool alone, while eliminating the need for a user to provide sketches.