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.

翻译：高层次综合（HLS）是开发高效硬件加速器的强大工具，这些加速器依赖专用存储系统以实现足够的片上数据重用和片外带宽利用。然而，即使采用HLS，设计此类系统仍需要细致的手动调优，因为现有工具提供的自动优化对编程风格高度敏感，且通常缺乏透明度。为解决这些问题，我们提出一个基于关系霍尔逻辑的形式化翻译框架，该框架支持鲁棒且透明的转换。我们的方法能够识别朴素HLS程序中的复杂访存模式，并通过插入片上缓冲区以强制对片外存储器的线性访问，以及通过用流处理替换非顺序处理来自动转换这些模式，同时保持程序语义不变。使用我们的原型翻译器结合商用HLS编译器和真实FPGA板进行的实验已展现出显著的性能提升。