Dataset for EASY: Efficient Arbiter SYnthesis from Multi-threaded Code

High-level synthesis (HLS) is an increasingly popular method for generating hardware from a description written in a software language like C/C++. Traditionally, HLS tools have operated on sequential code, however in recent years there has been a drive to synthesise multi-threaded code. In this context, a major challenge facing HLS tools is how to automatically partition memory among parallel threads to fully exploit the bandwidth available on an FPGA device and minimise memory contention. Existing partitioning approaches require inefficient arbitration circuitry to serialise accesses to each bank because they make conservative assumptions about which threads might access which memory banks. In this work, we design a static analysis that can prove certain memory banks are only accessed by certain threads and use this analysis to simplify or even remove the arbiters while preserving correctness. We show how this analysis can be implemented using the Microsoft Boogie verifier, a tool named EASY for automatic formal verification using an SMT solver. Our work supports arbitrary input code with any irregular memory access patterns and indirect array addressing forms. We implement our approach in LLVM, integrate it with the LegUp HLS tool, and show that for a set of typical application benchmarks we can achieve up to 87% (avg. 61%) area savings and up to 39% (avg. 23%) improvement in execution time, with little additional compilation time relative to a long time in hardware synthesis. This repository includes all the measured results for this work