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）求解器的最优软件流水线生成方法。实验表明，该方法在性能上显著优于启发式算法与手工优化方案。此外，我们展示了如何利用求解器为程序员和处理器设计者提供反馈，解释为何特定启动间隔的软件流水线调度方案不可行。