Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915749274058752 |
|---|---|
| author | Tanaka, Izumi Sakayori, Ken Takamaeda-Yamazaki, Shinya Kobayashi, Naoki |
| author_facet | Tanaka, Izumi Sakayori, Ken Takamaeda-Yamazaki, Shinya Kobayashi, Naoki |
| contents | High-level synthesis (HLS) is a powerful tool for developing efficient hardware accelerators that rely on specialized memory systems to achieve sufficient on-chip data reuse and off-chip bandwidth utilization. However, even with HLS, designing such systems still requires careful manual tuning, as automatic optimizations provided by existing tools are highly sensitive to programming style and often lack transparency. To address these issues, we present a formal translation framework based on relational Hoare logic, which enables robust and transparent transformations. Our method recognizes complex memory access patterns in naïve HLS programs and automatically transforms them by inserting on-chip buffers to enforce linear access to off-chip memory, and by replacing non-sequential processing with stream processing, while preserving program semantics. Experiments using our prototype translator, combined with an off-the-shelf HLS compiler and a real FPGA board, have demonstrated significant performance improvements. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_09217 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators Tanaka, Izumi Sakayori, Ken Takamaeda-Yamazaki, Shinya Kobayashi, Naoki Programming Languages Hardware Architecture High-level synthesis (HLS) is a powerful tool for developing efficient hardware accelerators that rely on specialized memory systems to achieve sufficient on-chip data reuse and off-chip bandwidth utilization. However, even with HLS, designing such systems still requires careful manual tuning, as automatic optimizations provided by existing tools are highly sensitive to programming style and often lack transparency. To address these issues, we present a formal translation framework based on relational Hoare logic, which enables robust and transparent transformations. Our method recognizes complex memory access patterns in naïve HLS programs and automatically transforms them by inserting on-chip buffers to enforce linear access to off-chip memory, and by replacing non-sequential processing with stream processing, while preserving program semantics. Experiments using our prototype translator, combined with an off-the-shelf HLS compiler and a real FPGA board, have demonstrated significant performance improvements. |
| title | Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators |
| topic | Programming Languages Hardware Architecture |
| url | https://arxiv.org/abs/2601.09217 |