Skip to main content

2017 | Buch

Separation Logic for High-level Synthesis

insite
SUCHEN

Über dieses Buch

This book presents novel compiler techniques, which combine a rigorous mathematical framework, novel program analyses and digital hardware design to advance current high-level synthesis tools and extend their scope beyond the industrial ‘state of the art’. Implementing computation on customised digital hardware plays an increasingly important role in the quest for energy-efficient high-performance computing. Field-programmable gate arrays (FPGAs) gain efficiency by encoding the computing task into the chip’s physical circuitry and are gaining rapidly increasing importance in the processor market, especially after recent announcements of large-scale deployments in the data centre. This is driving, more than ever, the demand for higher design entry abstraction levels, such as the automatic circuit synthesis from high-level languages (high-level synthesis). The techniques in this book apply formal reasoning to high-level synthesis in the context of demonstrably practical applications.<

Inhaltsverzeichnis

Frontmatter
Chapter 1. Introduction
Abstract
With the increasing demand for performance and efficiency of computing devices, custom computing is a growing area in digital computation today, which represents a class of processing devices that are dedicated to an application. This chapter introduces custom computing using FPGAs and high-level synthesis. It discusses the challenges in state-of-the-art high-level synthesis flows and introduces the research contributions made in this thesis.
Felix Winterstein
Chapter 2. High-Level Synthesis of Dynamic Data Structures
Abstract
High-level synthesis promises significant shortening of the design cycle compared to a design entry at RTL. However, many high-level synthesis implementations require extensive code alterations to ensure synthesisability and to achieve a quality of results comparable to handwritten RTL designs. These are especially important for programs with ‘irregular control flow’ and ‘complicated data dependencies’. In this chapter, we describe these terms in detail and elaborate on their implications for efficient high-level synthesis within the scope of a case study.
Felix Winterstein
Chapter 3. Background
Abstract
Besides the basic high-level synthesis steps, resource allocation, scheduling, binding and the generation of control circuits, a high-level synthesis tool usually performs several optimisation steps and transformations of the input code. This chapter discusses a literature review of existing techniques for parallelisation and memory system optimisations related to high-level synthesis flows. It also introduces separation logic, the theoretical framework leveraged in this thesis.
Felix Winterstein
Chapter 4. Heap Partitioning and Parallelisation
Abstract
Automatic parallelisation in high-level synthesis compilers requires a memory access and dependence analysis so as to detect parallelisation opportunities and partition the memory space accordingly. This chapter describes a static program analysis and automated code transformations that enable automatic parallelisation and distribution of data over separate blocks of FPGA memory.
Felix Winterstein
Chapter 5. Custom Multi-cache Architectures
Abstract
FPGAs allow the implementor to tailor the interface to off-chip memory and the on-chip/off-chip memory hierarchy according to the requirements of the application. This chapter presents a high-level synthesis design aid that leverages a memory access analysis of the application to automatically synthesise an application-specific high-performance memory hierarchy.
Felix Winterstein
Chapter 6. Conclusion
Abstract
This thesis extends the scope of high-level synthesis to efficient hardware implementations from heap-manipulating programs. This research direction is motivated by the fact that hardware synthesis and design optimisations for heap-manipulating code are beyond the scope of state-of-the-art tools to date. This chapter summarises the research contributions of the thesis and presents an outlook of challenges ahead.
Felix Winterstein
Backmatter
Metadaten
Titel
Separation Logic for High-level Synthesis
verfasst von
Felix Winterstein
Copyright-Jahr
2017
Electronic ISBN
978-3-319-53222-6
Print ISBN
978-3-319-53221-9
DOI
https://doi.org/10.1007/978-3-319-53222-6

Neuer Inhalt