|||Sabine Glesner, Rubino Gei√ü, Boris Boesler, Verified Code Generation for Embedded Systems, In Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), Electronic Notes in Theoretical Computer Science (ENTCS), 5th European Conferences on Theory and Practice of Software (ETAPS 2002),, April 13 2002.
Leider nur in Englisch verf√ľgbar.
Digital signal processors provide specialized SIMD (single instruction multiple data)
operations designed to dramatically increase performance in embedded systems.
While these operations are simple to understand, their unusual functions and their
parallelism make it dicult for automatic code generation algorithms to use them
eectively. In this paper, we present a new optimizing code generation method that
can deploy these operations successfully while also verifying that the generated code
is a correct translation of the input program.