A Systematic Incrementalization Technique and Its Application to Hardware Design

  • Steven D. Johnson
  • Yanhong A. Liu
  • Yuchen Zhang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


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.

Keywords and Phrases

Formal methods hardware verification design derivation formal synthesis transformational programming floating point operations 


  1. 1.
    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.Google Scholar
  2. 2.
    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.CrossRefGoogle Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    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.zbMATHGoogle Scholar
  5. 5.
    Yanhong A. Liu and Tim Teitelbaum. Systematic derivation of incremental programs. Sci. Comput. Program., 24(1):1–39, February 1995.zbMATHCrossRefGoogle Scholar
  6. 6.
    Yanhong Annie Liu. Incremental Computation: A Semantics-Based Systematic Transformational Approach. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, January 1996.Google Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Steven D. Johnson
    • 1
  • Yanhong A. Liu
    • 2
  • Yuchen Zhang
    • 3
  1. 1.Computer Science DepartmentIndiana UniversityUSA
  2. 2.Indiana UniversityUSA
  3. 3.Indiana UniversityUSA

Personalised recommendations