面向硬件加速器高层次综合的关系 Hoare 逻辑
编程语言
2026-01-26 v2 硬件体系结构
摘要
高层次综合（HLS）是开发高效硬件加速器的强大工具，这些加速器依赖专用存储系统来实现足够的片上数据重用和片外带宽利用率。然而，即使使用 HLS，设计此类系统仍需仔细的手动调优，因为现有工具提供的自动优化对编程风格高度敏感，且往往缺乏透明度。为了解决这些问题，我们提出了一个基于关系 Hoare 逻辑的形式化转换框架，可实现稳健且透明的转换。我们的方法能够识别朴素 HLS 程序中复杂的存储访问模式，并通过插入片上缓冲区以强制对片外存储进行线性访问，以及用流处理替换非顺序处理，来自动转换这些模式，同时保持程序语义。使用我们的原型转换器，结合现成的 HLS 编译器和真实的 FPGA 板进行的实验表明，性能得到了显著提升。
引用
@article{arxiv.2601.09217,
title = {Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators},
author = {Izumi Tanaka and Ken Sakayori and Shinya Takamaeda-Yamazaki and Naoki Kobayashi},
journal= {arXiv preprint arXiv:2601.09217},
year = {2026}
}
备注
An extended version of the paper to appear in Proceedings of ESOP 2026