A systematic incrementalization technique and its application to hardware design

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.