Coarse-Grain Reconfigurable Arrays (CGRAs) are emerging low-power architectures aimed at accelerating compute-intensive application loops. The acceleration that a CGRA can ultimately provide, however, heavily depends on the quality of the mapping, i.e. on how effectively the loop is compiled onto the given platform. State of the Art compilation techniques achieve mapping through modulo scheduling, a strategy which attempts to minimize the II (Iteration Interval) needed to execute a loop, and they do so usually through well known graph algorithms, such as Max-Clique Enumeration. We address the mapping problem through a SAT formulation, instead, and thus explore the solution space more effectively than current SoA tools. To formulate the SAT problem, we introduce an ad-hoc schedule called the \textit{kernel mobility schedule} (KMS), which we use in conjunction with the data-flow graph and the architectural information of the CGRA in order to create a set of boolean statements that describe all constraints to be obeyed by the mapping for a given II. We then let the SAT solver efficiently navigate this complex space. As in other SoA techniques, the process is iterative: if a valid mapping does not exist for the given II, the II is increased and a new KMS and set of constraints is generated and solved. Our experimental results show that SAT-MapIt obtains better results compared to SoA alternatives in $47.72\%$ of the benchmarks explored: sometimes finding a lower II, and others even finding a valid mapping when none could previously be found.

翻译：粗粒度可重构阵列（CGRAs）是一种新兴的低功耗架构，旨在加速计算密集型应用循环。然而，CGRA最终能提供的加速效果在很大程度上取决于映射质量，即循环如何有效地编译到给定平台上。现有最先进的编译技术通过模调度实现映射，该策略试图最小化执行循环所需的迭代间隔（II），通常通过已知的图算法（如最大团枚举）来实现。相反，我们通过SAT（可满足性）公式化方法解决映射问题，从而比当前最先进工具更有效地探索解空间。为构建SAT问题，我们引入了一种称为“内核移动性调度”（KMS）的专用调度方案，结合数据流图和CGRA的架构信息，生成一组布尔语句，描述给定II下映射必须遵守的所有约束条件。随后，我们利用SAT求解器高效遍历这一复杂空间。与其他最先进技术类似，该过程是迭代的：如果给定II下不存在有效映射，则增加II，生成新的KMS和约束集并求解。实验结果表明，在探索的基准测试中，SAT-MapIt在47.72%的情况下优于现有最先进方案：有时找到更低的II，有时甚至能在先前无法找到有效映射的情况下成功实现映射。