Scaling Program Synthesis Based Technology Mapping with Equality Saturation

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. How...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2024-11
Main Authors: Smith, Gus Henry, Knizek, Colin, Petrisko, Daniel, Tatlock, Zachary, Balkind, Jonathan, Bernstein, Gilbert Louis, Ni, Haobin, Nandi, Chandrakana
Format: Article
Language:English
Subjects:
Digital mapping
Hardware
Sketches
Synthesis
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422