Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators

TL;DR

This paper introduces a formal translation framework using relational Hoare logic to automatically optimize high-level hardware synthesis code, improving performance and transparency in hardware accelerator design.

Contribution

It presents a novel formal method for transforming HLS programs to enhance memory access patterns and processing, addressing manual tuning challenges.

Findings

Significant performance improvements demonstrated on FPGA implementations.

Automatic transformations preserve program semantics and improve memory efficiency.

Framework effectively recognizes complex memory access patterns in HLS code.

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\"ive 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.