Abstract
A transformation method based on incrementalization and value caching, generalizes a broad family of loop refinement techniques. This method and CACHET, an interactive tool supporting it, are presented. Though highly structured and automatable, better results are obtained with intelligent interaction, which provides insight and proofs involving term equality. Significant performance improvements are obtained in many representative program classes, including iterative schemes that characterize Today’s hardware specifications. Incrementalization is illustrated by the derivation of a hardware-efficient nonrestoring square-root algorithm.
Supported, in part, by the National Science Foundation under grant MIP-9601358.
Supported, in part, by the National Science Foundation under grant CCR-9711253
Chapter PDF
Similar content being viewed by others
Keywords and Phrases
References
Steven D. Johnson, Yanhong A. Liu, and Yuchen Zhang. A systematic incrementalization technique and its application to hardware design. Computer Science Department Technical Report 524, Indiana University, June 1999.
Yanhong A. Liu. CACHET: An interactive, incremental-attribution-based program transformation system for deriving incremental programs. In Proceedings of the 10th Knowledge-Based Software Engineering Conference, pages 19–26, Boston, Massachusetts, November 1995. IEEE CS Press, Los Alamitos, Calif.
Yanhong A. Liu. Principled strength reduction. In Richard Bird and Lambert Meertens, editors, Algorithmic Languages and Calculi, pages 357–381. Chapman & Hall, London, U. K., 1997.
Yanhong A. Liu, Scott D. Stoller, and Tim Teitelbaum. Static caching for incremental computation. ACM Trans. Program. Lang. and Syst., 20(2):1–40, March 1998.
Yanhong A. Liu and Tim Teitelbaum. Systematic derivation of incremental programs. Sci. Comput. Program., 24(1):1–39, February 1995.
Yanhong Annie Liu. Incremental Computation: A Semantics-Based Systematic Transformational Approach. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, January 1996.
John O’Leary, Miriam Leeser, Jason Hickey, and Mark Aagaard. Nonrestoring integer square root: A case study in design by principled optimization. In Ramayya Kumar and Thomas Kropf, editors, Proceedings of the 2nd International Conference on Theorem Provers in Circuit Design: Theory, Practice, and Experience, volume 901 of Lecture Notes in Computer Science, pages 52–71, Bad Herrenalb (Black Forest), Germany, September 1994. Springer-Verlag, Berlin.
Phillip Windley, Mark Aagard, and Miriam Leeser. Towards a super duper hardware tactic. In Jeffery J. Joyce and Carl Seger, editors, Higher-Order Logic Theorem Proving and its Applications, volume 780 of Lecture Notes in Computer Science Springer-Verlag, August 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Johnson, S.D., Liu, Y.A., Zhang, Y. (1999). A Systematic Incrementalization Technique and Its Application to Hardware Design. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_28
Download citation
DOI: https://doi.org/10.1007/3-540-48153-2_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66559-5
Online ISBN: 978-3-540-48153-9
eBook Packages: Springer Book Archive