The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Eliminating Excessive Dynamism of Dataflow Circuits Using Model Checking
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
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.
@misc{xu2023eliminating,
title = {Eliminating Excessive Dynamism of Dataflow Circuits Using Model Checking},
author = {Jiahui Xu and Emmet Murphy and Jordi Cortadella and Lana Josipović},
year = {2023},
journal = {ACM/SIGDA International Symposium on Field-Programmable Gate Arrays (FPGA)},
pages = {27--37},
doi = {10.1145/3543622.3573196},
}