Optimal Software Pipelining using an SMT-Solver

TL;DR

This paper introduces an optimal software pipelining method for VLIW processors using an SMT solver, outperforming heuristics and aiding programmers and designers in schedule feasibility analysis.

Contribution

It presents a novel SMT-based approach for optimal software pipelining, providing better performance and insightful feedback compared to traditional heuristics.

Findings

Outperforms heuristic algorithms and hand-optimized schedules

Provides feedback on schedule feasibility to programmers and designers

Significantly improves instruction-level parallelism in loop optimization

Abstract

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.