SAT-MapIt: A SAT-based Modulo Scheduling Mapper for Coarse Grain Reconfigurable Architectures

TL;DR

This work tackles the challenge of mapping loop kernels onto coarse-grain reconfigurable arrays (CGRAs) by introducing SAT-MapIt, a SAT-based modulo scheduling mapper. It defines a novel Kernel Mobility Schedule (KMS) to encode the scheduling space and uses a CNF formulation to capture data dependencies, architectural constraints, and stage folding, solving with a SAT solver and iteratively increasing the iteration interval $II$ when needed. Experimental results show SAT-MapIt outperforms state-of-the-art heuristic methods in 47.72% of benchmarks across varied CGRA sizes, and even finds feasible mappings where previous tools fail, demonstrating the method’s effectiveness and scalability. The approach offers a principled, exact exploration of the scheduling space for CGRA mapping, with practical impact on achieving lower latency and higher performance for loop-intensive workloads, albeit with current limitations in routing strategies.

Abstract

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.

Figures (6)

• Figure 1: Example $3\times 3$ CGRA. Processing elements are connected in a 2D mesh with near-neighbour topology.
• Figure 2: a) Example Data Flow graph of a loop. b) Modulo scheduling of the DFG on the left, highlighting the division among Prolog, Kernel, and Epilog. The loop is unrolled once; the first iteration is in blue, and the second, shifted by $II$, is in green. c) Mapping example on a $2\times 2$ CGRA
• Figure 3: SAT-MapIt searches for mappings for a given $II$, iteratively increasing $II$ in case the SAT solver returns UNSAT, or register allocation fails to colour the model returned by the solver.
• Figure 4: ASAP, ALAP, and Mobility Schedule
• Figure 5: Kernel Mobility Schedule creation. In blue iteration 0, in green iteration 1