Efficient memory arbitration in high-level synthesis from multi-threaded code
File(s)
Accepted version
Author(s)
Type
Journal Article
Abstract
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 article, 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 on top of satisfiability modulo theories (SMT) solver, and propose a tool named EASY using automatic formal verification. Our work supports arbitrary input code with any irregular memory access patterns and indirect array addressing forms. We implement our approach in LLVM and integrate it into the LegUp HLS tool. For a set of typical application benchmarks our results have shown that EASY can achieve 0.13×(avg. 0.43×) of area and 1.64×(avg. 1.28×) of performance compared to the baseline, with little additional compilation time relative to the long time in hardware synthesis.
Date Issued
2022-04-01
Date Acceptance
2021-02-28
Citation
IEEE Transactions on Computers, 2022, 71 (4), pp.933-946
ISSN
0018-9340
Publisher
Institute of Electrical and Electronics Engineers (IEEE)
Start Page
933
End Page
946
Journal / Book Title
IEEE Transactions on Computers
Volume
71
Issue
4
Copyright Statement
© 2021 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Identifier
https://ieeexplore.ieee.org/document/9380343
Grant Number
EP/P010040/1
Subjects
Science & Technology
Technology
Computer Science, Hardware & Architecture
Engineering, Electrical & Electronic
Computer Science
Engineering
Instruction sets
Tools
Hardware
Software
Memory management
Bandwidth
Scalability
High-level synthesis
HLS
formal methods
multi-threaded code
FPGA
Computer Hardware & Architecture
0803 Computer Software
0805 Distributed Computing
1006 Computer Hardware
Publication Status
Published
Date Publish Online
2021-03-17