A Scalable Approach to Exact Resource-Constrained Scheduling Based on a Joint SDC and SAT Formulation
A Scalable Approach to Exact Resource-Constrained Scheduling Based on a Joint SDC and SAT Formulation
复制标题
DOI：
10.1145/3174243.3174268
复制
发表时间：
2018-02
期刊：
影响因子：
--
通讯作者：
Steve Dai;Gai Liu;Zhiru Zhang
中科院分区：
文献类型：
--
作者：
Steve Dai;Gai Liu;Zhiru Zhang
尽管高级合成（HLS）的设计生产力优势越来越高，但在实现高质量的较高质量中的成功通常受到普通HLS优化的不精确性的阻碍。特别是，尽管计划构成了HLS技术的算法核心，但当前的日程安排算法很大程度上依赖于从根本上进行不精确的启发式方法，这些启发式方法可以做出临时的本地决策，并且无法准确和全球优化一系列约束。为了应对这一挑战，我们提出了基于整数差异限制系统（SDC）和Boolean Excelability（SAT）的调度公式，以精确处理各种调度限制。我们开发了一个基于冲突驱动的学习和特定问题知识的专业调度程序，以最佳有效地解决资源约束的调度问题。通过利用SDC算法的效率和现代SAT求解器的可扩展性，我们的调度技术能够平均能够超过100倍的运行时提高整数线性编程（ILP）方法，同时达到最佳延迟。通过将我们的调度公式集成到最先进的开源HLS工具中，我们进一步证明了我们的调度技术的适用性，并使用针对FPGA的一套代表性基准。
Despite increasing adoption of high-level synthesis (HLS) for its design productivity advantage, success in achieving high quality-of-results out-of-the-box is often hindered by the inexactness of the common HLS optimizations. In particular, while scheduling forms the algorithmic core to HLS technology, current scheduling algorithms rely heavily on fundamentally inexact heuristics that make ad hoc local decisions and cannot accurately and globally optimize over a rich set of constraints. To tackle this challenge, we propose a scheduling formulation based on system of integer difference constraints (SDC) and Boolean satisfiability (SAT) to exactly handle a variety of scheduling constraints. We develop a specialized scheduler based on conflict-driven learning and problem-specific knowledge to optimally and efficiently solve the resource-constrained scheduling problem. By leveraging the efficiency of SDC algorithms and scalability of modern SAT solvers, our scheduling technique is able to achieve on average over 100x improvement in runtime over the integer linear programming (ILP) approach while attaining optimal latency. By integrating our scheduling formulation into a state-of-the-art open-source HLS tool, we further demonstrate the applicability of our scheduling technique with a suite of representative benchmarks targeting FPGAs.