Formal verification of high-level synthesis

High-level synthesis (HLS), which refers to the automatic compilation of software into hardware, is rapidly gaining popularity. In a world increasingly reliant on application-specific hardware accelerators, HLS promises hardware designs of comparable performance and energy efficiency to those coded by hand in a hardware description language such as Verilog, while maintaining the convenience and the rich ecosystem of software development. However, current HLS tools cannot always guarantee that the hardware designs they produce are equivalent to the software they were given, thus undermining any reasoning conducted at the software level. Furthermore, there is mounting evidence that existing HLS tools are quite unreliable, sometimes generating wrong hardware or crashing when given valid inputs. To address this problem, we present the first HLS tool that is mechanically verified to preserve the behaviour of its input software. Our tool, called Vericert, extends the CompCert verified C compiler with a new hardware-oriented intermediate language and a Verilog back end, and has been proven correct in Coq. Vericert supports most C constructs, including all integer operations, function calls, local arrays, structs, unions, and general control-flow statements. An evaluation on the PolyBench/C benchmark suite indicates that Vericert generates hardware that is around an order of magnitude slower (only around 2× slower in the absence of division) and about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.

Download Full-text

Buffer Placement and Sizing for High-Performance Dataflow Circuits

ACM Transactions on Reconfigurable Technology and Systems ◽

10.1145/3477053 ◽

2022 ◽

Vol 15 (1) ◽

pp. 1-32

Author(s):

Lana Josipović ◽

Shabnam Sheikhha ◽

Andrea Guerrieri ◽

Paolo Ienne ◽

Jordi Cortadella

Keyword(s):

Performance Optimization ◽

Optimization Model ◽

High Performance ◽

Control Flow ◽

High Level Synthesis ◽

Software Applications ◽

Marked Graphs ◽

Variable Latency ◽

High Level ◽

Strong Contrast

Commercial high-level synthesis tools typically produce statically scheduled circuits. Yet, effective C-to-circuit conversion of arbitrary software applications calls for dataflow circuits, as they can handle efficiently variable latencies (e.g., caches), unpredictable memory dependencies, and irregular control flow. Dataflow circuits exhibit an unconventional property: registers (usually referred to as “buffers”) can be placed anywhere in the circuit without changing its semantics, in strong contrast to what happens in traditional datapaths. Yet, although functionally irrelevant, this placement has a significant impact on the circuit’s timing and throughput. In this work, we show how to strategically place buffers into a dataflow circuit to optimize its performance. Our approach extracts a set of choice-free critical loops from arbitrary dataflow circuits and relies on the theory of marked graphs to optimize the buffer placement and sizing. Our performance optimization model supports important high-level synthesis features such as pipelined computational units, units with variable latency and throughput, and if-conversion. We demonstrate the performance benefits of our approach on a set of dataflow circuits obtained from imperative code.

Download Full-text

Efficient Implementation of Application-Aware Spinlock Control in MPSoCs

International Journal of Embedded and Real-Time Communication Systems ◽

10.4018/jertcs.2013010104 ◽

2013 ◽

Vol 4 (1) ◽

pp. 64-84 ◽

Cited By ~ 3

Author(s):

Diandian Zhang ◽

Li Lu ◽

Jeronimo Castrillon ◽

Torsten Kempf ◽

Gerd Ascheid ◽

...

Keyword(s):

High Efficiency ◽

A Priori ◽

Control Flow ◽

Specific Information ◽

Centralized Control ◽

Shared Resources ◽

Complete Control ◽

Application Aware ◽

High Level ◽

Application Specific

Spinlocks are a common technique in Multi-Processor Systems-on-Chip (MPSoCs) to protect shared resources and prevent data corruption. Without a priori application knowledge, the control of spinlocks is often highly random which can degrade the system performance significantly. To improve this, a centralized control mechanism for spinlocks is proposed in this paper, which utilizes application-specific information during spinlock control. The complete control flow is presented, which starts from integrating high-level user-defined information down to a low-level realization of the control. An Application-Specific Instruction-set Processor (ASIP) called OSIP, which was originally designed for task scheduling and mapping, is extended to support this mechanism. The case studies demonstrate the high efficiency of the proposed approach and at the same time highlight the efficiency and flexibility advantages of using an ASIP as the system controller in MPSoCs.

Download Full-text

A Prolog-based design environment for the high-level synthesis of application-specific architectures

Microprocessing and Microprogramming ◽

10.1016/0165-6074(91)90363-x ◽

1991 ◽

Vol 32 (1-5) ◽

pp. 307-313 ◽

Cited By ~ 4

Author(s):

P. Tsanakas ◽

G. Papakonstantinou ◽

S. Kaxiras

Keyword(s):

High Level Synthesis ◽

Design Environment ◽

High Level ◽

Application Specific

Download Full-text

High-level synthesis of low-power control-flow intensive circuits

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems ◽

10.1109/43.811321 ◽

1999 ◽

Vol 18 (12) ◽

pp. 1715-1729 ◽

Cited By ~ 19

Author(s):

K.S. Khouri ◽

G. Lakshminarayana ◽

N.K. Jha

Keyword(s):

Low Power ◽

Power Control ◽

Control Flow ◽

High Level Synthesis ◽

High Level

Download Full-text

Configuration and scheduling of the LHCb trigger application

EPJ Web of Conferences ◽

10.1051/epjconf/202024505004 ◽

2020 ◽

Vol 245 ◽

pp. 05004

Author(s):

Rosen Matev ◽

Niklas Nolte ◽

Alex Pearce

Keyword(s):

Hadron Collider ◽

Research Programme ◽

Control Flow ◽

Data Flow Graph ◽

Level Trigger ◽

Form Part ◽

Order Of Magnitude ◽

High Level ◽

User Friendly ◽

And Control

For Run 3 of the Large Hadron Collider, the final stage of the LHCb experiment’s high-level trigger must process 100 GB/s of input data. This corresponds to an input rate of 1 MHz, and is an order of magnitude larger compared to Run 2. The trigger is responsible for selecting all physics signals that form part of the experiment’s broad research programme, and as such defines thousands of analysis-specific selections that together comprise tens of thousands of algorithm instances. The configuration of such a system needs to be extremely flexible to be able to handle the large number of different studies it must accommodate. However, it must also be robust and easy to understand, allowing analysts to implement and understand their own selections without the possibility of error. A Python-based system for configuring the data and control flow of the Gaudi-based trigger application is presented. It is designed to be user-friendly by using functions for modularity and removing indirection layers employed previously in Run 2. Robustness is achieved by reducing global state and instead building the data flow graph in a functional manner, whilst keeping configurability of the full call stack.

Download Full-text