Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators

TL;DR

The paper presents a formal framework for transforming naïve HLS programs into hardware-friendly equivalents using relational Hoare logic, enabling automatic insertion of on-chip buffers and replacement of non-sequential memory accesses with stream processing while preserving semantics. By modeling a minimal source language with arrays and a target language with streams, and by defining a translation relation with pre/post-conditions, the approach achieves robust, style-independent optimizations that standard HLS tools often miss. The authors implement a prototype translator that automates buffer insertion and stream conversion, and validate it on an FPGA-based workflow with Vitis HLS and Vivado, reporting significant performance improvements and up to 38.5x speedups on several benchmarks. They also discuss limitations, formal correctness guarantees, and directions for extending the framework to richer data structures, scheduling, and tiling, highlighting the potential for using relational Hoare logics to guide hardware-aware optimizations.

Abstract

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.

Figures (3)

• Figure 1: Pitfall of Vitis HLS: The first (top) uses burst transfers, whereas the second (bottom) fails to do so.
• Figure 2: Naïve filtering program without burst transfers (top) vs. translated program with burst transfers (bottom).
• Figure 3: High-level synthesis toolchain with our tool.