Mechanical Certification of Loop Pipelining Transformations: A Preview

D. Puri, S. Ray, K. Hao, and F. Xie

In R. Gamboa and G. Klein editors, Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP 2014), Vienna, Austria, July 2014, volume 8558 of LNCS, pages 549-554. Springer.

© 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.

Relevant files