Software Pipelining is a classic and important loop-optimization for VLIW processors. It improves instruction-level parallelism by overlapping multiple iterations of a loop and executing them in parallel. Typically, it is implemented using heuristics. In this paper, we present an optimal software pipeliner based on a Satisfiability Modulo Theories (SMT) Solver. We show that our approach significantly outperforms heuristic algorithms and hand-optimization. Furthermore, we show how the solver can be used to give feedback to programmers and processor designers on why a software pipelined schedule of a certain initiation interval is not feasible.

翻译：软件流水线是VLIW处理器中经典且重要的循环优化技术。它通过重叠循环的多次迭代并并行执行这些迭代来提高指令级并行性。通常，该技术采用启发式方法实现。本文提出了一种基于可满足性模理论（SMT）求解器的最优软件流水线调度方法。实验表明，该方法在性能上显著优于启发式算法与人工优化方案。此外，我们还展示了如何利用求解器向程序员和处理器设计者反馈特定启动间隔的软件流水线调度方案不可行的原因。