Improving Boolean Satisfiability-Based Modulo Scheduling

Modulo scheduling is a highly effective approach for maximizing throughput in loops with static memory dependencies, interleaving computations across consecutive loop iterations. Despite substantial advancements in scheduling procedures, it remains the most computationally intensive phase for high-level synthesis flows. A recent approach encodes the modulo scheduling problem as a series of Boolean satisfiability (SAT) instances, capitalizing on the efficiency of modern SAT solvers. This approach significantly reduces solving time and increases the availability of throughput-optimal solutions compared to integer linear programming-based algorithms. This work introduces two enhancements for SAT-based modulo scheduling: (i) an algorithm to rapidly calculate a lower bound for the schedule length, improving the identification of latency-optimal schedules; and (ii) a streamlined SAT formulation with fewer clauses, facilitating quicker solver decisions. Extensive experimental evaluations show that these improvements lead to an increased number of throughput-optimal and latency-optimal solutions.