Mechanical Certification of Loop Pipelining
Transformations: A Preview
K. Hao, and F. Xie
In R. Gamboa
and G. Klein editors,
International Conference on Interactive Theorem Proving
(ITP 2014), Vienna, Austria, July
2014, volume 8558 of LNCS,
© 2014 Springer.
We describe our ongoing effort using theorem proving to
certify loop pipelining, a critical and complex
transformation employed by behavioral synthesis. Our
approach is mechanized in the ACL2 theorem prover. We
discuss some formalization and proof challenges and our
early attempts at addressing them.