The paper presents a method for translation validation of a specific optimization, software pipelining optimization, used to increase the instruction level parallelism in EPIC type of architectures. Using a methodology as in "Validation of optimizing compilers / Zuck,Pnueli and Leviathan" to establish simulation relation between source and target based on computational induction, we describe an algorithm that automatically produces a set of decidable proof obligations. The paper also describes SPV, a prototype translation validator that automatically produces verification conditions for software pipelining optimizations of the SGI Pro-64 compiler. These verification conditions are further checked automatically by the CVC checker.
International Conference on Compilers, Architecture, and Synthesis for Embedded Systems