A systematic incrementalization technique and its application to hardware design

Steven D. Johnson; Yanhong A. Liu; Yuchen Zhang

doi:10.1007/3-540-48153-2_28

A systematic incrementalization technique and its application to hardware design

Steven D. Johnson
, Yanhong A. Liu
, Yuchen Zhang

Computer Science

Indiana University Bloomington

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Correct Hardware Design and Verification Methods - 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME 1999, Proceedings
Editors	Laurence Pierre, Thomas Kropf
Publisher	Springer Verlag
Pages	334-337
Number of pages	4
ISBN (Print)	3540665595, 9783540665595
DOIs	https://doi.org/10.1007/3-540-48153-2_28
State	Published - 1999
Event	10th IFIP WG 10.5 Working Conference on Correct Hardware Design and Verification Methods, CHARME 1999 - Bad Herrenalb, Germany Duration: Sep 27 1999 → Sep 29 1999

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1703
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th IFIP WG 10.5 Working Conference on Correct Hardware Design and Verification Methods, CHARME 1999
Country/Territory	Germany
City	Bad Herrenalb
Period	09/27/99 → 09/29/99

Keywords

Design derivation
Floating point operations
Formal methods
Formal synthesis
Hardware verification
Transformational programming

Access to Document

10.1007/3-540-48153-2_28

Cite this

Johnson, S. D., Liu, Y. A., & Zhang, Y. (1999). A systematic incrementalization technique and its application to hardware design. In L. Pierre, & T. Kropf (Eds.), Correct Hardware Design and Verification Methods - 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME 1999, Proceedings (pp. 334-337). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1703). Springer Verlag. https://doi.org/10.1007/3-540-48153-2_28

Johnson, Steven D. ; Liu, Yanhong A. ; Zhang, Yuchen. / A systematic incrementalization technique and its application to hardware design. Correct Hardware Design and Verification Methods - 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME 1999, Proceedings. editor / Laurence Pierre ; Thomas Kropf. Springer Verlag, 1999. pp. 334-337 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{4423db71640a4c4b8d7187f0b3441205,

title = "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{\textquoteright}s hardware specifications. Incrementalization is illustrated by the derivation of a hardware-efficient nonrestoring square-root algorithm.",

keywords = "Design derivation, Floating point operations, Formal methods, Formal synthesis, Hardware verification, Transformational programming",

author = "Johnson, \{Steven D.\} and Liu, \{Yanhong A.\} and Yuchen Zhang",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1999.; 10th IFIP WG 10.5 Working Conference on Correct Hardware Design and Verification Methods, CHARME 1999 ; Conference date: 27-09-1999 Through 29-09-1999",

year = "1999",

doi = "10.1007/3-540-48153-2\_28",

language = "English",

isbn = "3540665595",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "334--337",

editor = "Laurence Pierre and Thomas Kropf",

booktitle = "Correct Hardware Design and Verification Methods - 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME 1999, Proceedings",

}

Johnson, SD, Liu, YA & Zhang, Y 1999, A systematic incrementalization technique and its application to hardware design. in L Pierre & T Kropf (eds), Correct Hardware Design and Verification Methods - 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME 1999, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1703, Springer Verlag, pp. 334-337, 10th IFIP WG 10.5 Working Conference on Correct Hardware Design and Verification Methods, CHARME 1999, Bad Herrenalb, Germany, 09/27/99. https://doi.org/10.1007/3-540-48153-2_28

A systematic incrementalization technique and its application to hardware design. / Johnson, Steven D.; Liu, Yanhong A.; Zhang, Yuchen.
Correct Hardware Design and Verification Methods - 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME 1999, Proceedings. ed. / Laurence Pierre; Thomas Kropf. Springer Verlag, 1999. p. 334-337 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1703).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A systematic incrementalization technique and its application to hardware design

AU - Johnson, Steven D.

AU - Liu, Yanhong A.

AU - Zhang, Yuchen

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1999.

PY - 1999

Y1 - 1999

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

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

KW - Design derivation

KW - Floating point operations

KW - Formal methods

KW - Formal synthesis

KW - Hardware verification

KW - Transformational programming

UR - https://www.scopus.com/pages/publications/84958681695

U2 - 10.1007/3-540-48153-2_28

DO - 10.1007/3-540-48153-2_28

M3 - Conference contribution

AN - SCOPUS:84958681695

SN - 3540665595

SN - 9783540665595

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 334

EP - 337

BT - Correct Hardware Design and Verification Methods - 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME 1999, Proceedings

A2 - Pierre, Laurence

A2 - Kropf, Thomas

PB - Springer Verlag

T2 - 10th IFIP WG 10.5 Working Conference on Correct Hardware Design and Verification Methods, CHARME 1999

Y2 - 27 September 1999 through 29 September 1999

ER -

Johnson SD, Liu YA, Zhang Y. A systematic incrementalization technique and its application to hardware design. In Pierre L, Kropf T, editors, Correct Hardware Design and Verification Methods - 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME 1999, Proceedings. Springer Verlag. 1999. p. 334-337. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-48153-2_28

A systematic incrementalization technique and its application to hardware design

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this