Circuits generated through dynamically-scheduled high-level synthesis (also known as elastic circuits) are highly performant, as circuit execution can adjust at runtime to variable control flow or memory dependencies. While there are many promising opportunities for further optimization, the resulting circuits can be difficult to analyze—the challenge of maintaining circuit correctness forms a major obstacle to the optimization process. Seeking to increase performance, we introduce for the first time eager execution—speculatively executing both sides of a conditional branch in parallel, with results committed based on the branch condition—to elastic circuits. We build on recent work to present eager execution as a set of formally verified circuit rewrite patterns, localized transformations which we prove preserve correctness. This allows us to pursue high performance, while simultaneously guaranteeing that global circuit correctness is maintained at every stage. Our eager execution strongly increases performance using only slight alterations to the control path of the circuit: unlike the prohibitive resource cost of processor eager execution, elastic-circuit eager execution can be effectively enabled without additional computational units. On a set of selected kernels, we achieve an average speed-up of 3.2x, at an average increase of 1.2x in LUTs and 1.3x in FFs, compared to standard elastic circuits. Excitingly, elastic eager execution opens up a new design space of high-performance circuits, generated through correct-by-construction approaches, which we have only just begun to explore. EagerlyElastic is open-sourced under 10.5281/zenodo.17703725.

While High-Level Synthesis (HLS) enables circuit generation directly from languages like C/C++ and OpenCL, optimal implementations require additional design specification through compiler directives. Automated optimization of these directives requires evaluation of candidate designs, but is bottlenecked by the high computational cost. Graph Neural Networks (GNNs) have recently emerged as the state-of-the-art for estimating the required Quality of Results (QoR) directly from high-level source code, but they come with associated challenges: the difficulty of information propagation, the complexity of software-oriented graph representations, and high levels of extraneous computation increase both error and computational cost. We present Balor, an HLS source code evaluator, which consists of a graph compiler and a GNN-based QoR estimator. The modular graph compiler is tailor-made for HLS QoR estimation, producing smaller graphs that contain only HLS-specific information. Balor analytically propagates important information across the graph, allowing us to pivot to small, local GNNs, while outperforming more expensive networks. Additionally, we make use of the natural hierarchy of an HLS kernel, and cluster the graph by basic block, to further propagate and process information---without the need for additional datasets. Combined, our contributions simultaneously reduce estimation error by 41%, and computational cost by 82%. Balor is open-sourced at github.com/emmet-murphy/balor

Recent HLS efforts explore the generation of dynamically scheduled, dataflow circuits from high-level code; their ability to adapt the schedule at runtime to particular data and control outcomes promises superior performance to standard, statically scheduled HLS solutions. However, dataflow circuits are notoriously resource-expensive: their distributed handshake mechanism brings performance benefits in some cases, but causes an unneeded resource overhead when general dynamism is not required. In this work, we present a verification framework based on model checking to systematically reduce the hardware complexity of dataflow circuits. We devise a series of formal proofs that identify the absence of particular behavioral scenarios and use this information to replace the generic dataflow logic with simpler and cheaper control structures. On a set of benchmarks obtained from high-level code, we demonstrate that our technique significantly reduces the resource requirements of dataflow circuits (i.e., it results in LUT and FF reductions of up to 51% and 53%, respectively), while still reaping all performance benefits of dynamic scheduling.