Scaling Program Synthesis Based Technology Mapping with Equality Saturation
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910705171562496 |
|---|---|
| author | Smith, Gus Henry Knizek, Colin Petrisko, Daniel Tatlock, Zachary Balkind, Jonathan Bernstein, Gilbert Louis Ni, Haobin Nandi, Chandrakana |
| author_facet | Smith, Gus Henry Knizek, Colin Petrisko, Daniel Tatlock, Zachary Balkind, Jonathan Bernstein, Gilbert Louis Ni, Haobin Nandi, Chandrakana |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_11036 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Scaling Program Synthesis Based Technology Mapping with Equality Saturation Smith, Gus Henry Knizek, Colin Petrisko, Daniel Tatlock, Zachary Balkind, Jonathan Bernstein, Gilbert Louis Ni, Haobin Nandi, Chandrakana Programming Languages Hardware Architecture 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. |
| title | Scaling Program Synthesis Based Technology Mapping with Equality Saturation |
| topic | Programming Languages Hardware Architecture |
| url | https://arxiv.org/abs/2411.11036 |