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板进行的实验已展现出显著的性能提升。