article

On the fundamental limitations of transformational design

Author:

Jeroen VoetenAuthors Info & Claims

ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 6, Issue 4

Pages 533 - 552

https://doi.org/10.1145/502175.502181

Published: 01 October 2001 Publication History

Abstract

The completeness of a collection of design transformations is an important aspect in transformational design. Completeness guarantees that any correct design can in principle be explored using the transformation system. In the field of transformational design the problem of incompleteness is not well understood and it is often believed that complete transformation systems can be constructed. In this article, we show, using a formal framework based on the theory of computation, that this is not the case if the transformation system is based on an expressive general-purpose design language such as VHDL. Only when restrictions are imposed on the design language and correctness relation, a transformation system can be made complete in theory, but this is expected to result in serious practical problems. It is shown that the incompleteness problem in transformational design is closely related to the syntactic variance problem in high-level synthesis and that this latter problem is not solvable in general either.

References

[1]

BOLOGNESI, T. 1992. Catalogue of LOTOS correctness-preserving transformations. Tech. Rep. Lo/WP1/T1.2/N0045/V03, LotoSphere Consortium, Univ. Twente, Twente, The Netherlands.

[2]

CAMPASANO, R. 1989. Behaviour-preserving transformations for high-level synthesis. In Proceedings of the Mathematical Sciences Institute Workshop (New York). Springer-Verlag, Berlin, Germany, pp. 106-128.

[3]

CHAIYAKUL, V., GAJSKI,D.,AND RAMACHANDRAN, L. 1993. High-level transformations for minimizing syntactic variances. In Proceedings of DAC'93 (Dallas, Texas). IEEE Computer Society Press, Los Alamitos, Calif., pp. 413-418.

[4]

CHERNIAVSKY, J. 1976. Simple programs realize exactly Presberger formulas. SIAM J. Comput. 5, 4, 666-677.

[5]

GAJSKI, D. 1994. Introduction to high-level synthesis. IEEE Des. Test Comput. (Winter), 44-54.

[6]

HILFINGER, P. 1985. A high-level language and silicon compiler for digital signal processing. In Proceedings of IEEE CICC Conference (Portland, Ore.). IEEE Computer Society Press, Piscat-away, N.J. pp. 213-216.

[7]

HOFSTADTER, D. 1979. G~del, Escher, Bach: An Eternal Golden Braid. Basic Books, New York.

[8]

HUIJS, C. 1996. A graph rewriting approach for transformational design of digital systems. In Proceedings of Euromicro'96 (Prague, Czech Republic). IEEE Computer Society Press, Los Alamitos, Calif., pp. 177-184.

[9]

JANSSEN, M., CATTHOOR,F.,AND DE MAN, H. 1994. A specification invariant technique for operation cost minimisation in flow-graphs. In Proceedings of the 7th International Symposium on High- Level Synthesis (Niagara-on-the-Lake, Ontario, Canada). IEEE Computer Society Press, Los Alamitos, Calif., pp. 146-151.

[10]

KROL,T.,VAN MEERBERGEN, J., NIESSEN, C., SMITS,W.,AND HUISKEN, J. 1992. The Sprite Input Language: an intermediate format for high level synthesis. In Proceedings of 3rd EDAC(Brussels, Belgium). IEEE Computer Society Press, Los Alamitos, Calif., pp. 186-192.

[11]

LEWIS, H., AND PAPADIMITRIOU, C. 1981. Elements of the Theory of Computation. Prentice-Hall, Engelwood Cliffs, N.J.

[12]

MEYER, A., AND RITCHIE, D. 1967. The complexity of loop programs. In Proceedings of 22nd National Conference of ACM (Washington D.C.). ACM, New York, pp. 465-469.

[13]

MIDDELHOEK, P. 1997. Transformational Design: An Architecture Independent Interactive Design Methodology for the Synthesis of Correct and Efficient Digital Systems. Ph.D. dissertation. Univ. Twente, The Netherlands.

[14]

MIDDELHOEK,P.,AND RAJAN, S. 1996. From VHDLto efficient and first-time-right designs: A formal approach. ACM Trans. Des. Automat. Elec. Syst. 1, 2, 205-250.

[15]

ODIFREDDI, P. 1989. Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers. North-Holland, Amsterdam, The Netherlands.

[16]

TSICHRITZIS, D. 1970. The equivalence problem of simple programs. J. ACM 17, 4 (Oct.), 729-738.

[17]

VAN MEERBERGEN, J., LIPPENS, P., VERHAEGH,W.,AND VAN DER WERF, A. 1995. PHIDEO: High-level synthesis for high throughput applications. J. VLSI Sig. Proc. 9, 89-104.

[18]

VEMURI, R. 1990. How to prove the completeness of a set of register level design transformations. In Proceedings of DAC'90 (Orlando, Fla.). IEEE Computer Society Press, Los Alamitos, Calif., pp. 207-212.

[19]

VOETEN,J.,VAN DER PUTTEN,P.,AND STEVENS, M. 1996. Behaviour-preserving transformations in SHE : A formal approach to architecture design. In Proceedings of EUROMICRO'96 (Prague, Czech Republic). IEEE Computer Society Press, Los Alamitos, Calif., pp. 19-27.

Cited By

Sander IJantsch AAttarzadeh-Niaki S(2017)ForSyDe: System Design Using a Functional Language and Models of ComputationHandbook of Hardware/Software Codesign10.1007/978-94-017-7358-4_5-1(1-42)Online publication date: 12-Apr-2017
https://doi.org/10.1007/978-94-017-7358-4_5-1
Sander IJantsch AAttarzadeh-Niaki S(2017)ForSyDe: System Design Using a Functional Language and Models of ComputationHandbook of Hardware/Software Codesign10.1007/978-94-017-7267-9_5(99-140)Online publication date: 27-Sep-2017
https://doi.org/10.1007/978-94-017-7267-9_5
Gerdes AHeeren BJeuring Jvan Binsbergen L(2016)Ask-Elle: an Adaptable Programming Tutor for Haskell Giving Automated FeedbackInternational Journal of Artificial Intelligence in Education10.1007/s40593-015-0080-x27:1(65-100)Online publication date: 5-Feb-2016
https://doi.org/10.1007/s40593-015-0080-x
Show More Cited By

Index Terms

On the fundamental limitations of transformational design
1. Applied computing
  1. Arts and humanities
    1. Architecture (buildings)
      1. Computer-aided design
  2. Physical sciences and engineering
    1. Engineering
      1. Computer-aided design
2. Theory of computation
  1. Computational complexity and cryptography
    1. Complexity classes
  2. Design and analysis of algorithms

Recommendations

A Henkin-Style Completeness Proof for the Modal Logic S5
Logic and Argumentation
Abstract
This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of Hughes and Cresswell [8], but the system, based on a ...
Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
A reification calculus for model-oriented software specification
Abstract
This paper presents a transformational approach to the derivation of implementations from model-oriented specifications of abstract data types.
The purpose of this research is to reduce the number of formal proofs required in model refinement, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Design Automation of Electronic Systems

ACM Transactions on Design Automation of Electronic Systems Volume 6, Issue 4

October 2001

198 pages

ISSN:1084-4309

EISSN:1557-7309

DOI:10.1145/502175

Issue’s Table of Contents

Copyright © 2001 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 01 October 2001

Published in TODAES Volume 6, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
400
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)1

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Sander IJantsch AAttarzadeh-Niaki S(2017)ForSyDe: System Design Using a Functional Language and Models of ComputationHandbook of Hardware/Software Codesign10.1007/978-94-017-7358-4_5-1(1-42)Online publication date: 12-Apr-2017
https://doi.org/10.1007/978-94-017-7358-4_5-1
Sander IJantsch AAttarzadeh-Niaki S(2017)ForSyDe: System Design Using a Functional Language and Models of ComputationHandbook of Hardware/Software Codesign10.1007/978-94-017-7267-9_5(99-140)Online publication date: 27-Sep-2017
https://doi.org/10.1007/978-94-017-7267-9_5
Gerdes AHeeren BJeuring Jvan Binsbergen L(2016)Ask-Elle: an Adaptable Programming Tutor for Haskell Giving Automated FeedbackInternational Journal of Artificial Intelligence in Education10.1007/s40593-015-0080-x27:1(65-100)Online publication date: 5-Feb-2016
https://doi.org/10.1007/s40593-015-0080-x
Jeuring Jvan Binsbergen LGerdes AHeeren B(2014)Model solutions and properties for diagnosing student programs in Ask-ElleProceedings of the Computer Science Education Research Conference10.1145/2691352.2691355(31-40)Online publication date: 5-Nov-2014
https://dl.acm.org/doi/10.1145/2691352.2691355
Martinez AKuchcinski K(2007)Graph Matching Constraints for Synthesis with Complex Components10th Euromicro Conference on Digital System Design Architectures, Methods and Tools (DSD 2007)10.1109/DSD.2007.4341482(288-295)Online publication date: Aug-2007
https://doi.org/10.1109/DSD.2007.4341482
Sander IJantsch ALu Z(2003)Development and application of design transformations in ForSyDeIEE Proceedings - Computers and Digital Techniques10.1049/ip-cdt:20030836150:5(313)Online publication date: 2003
https://doi.org/10.1049/ip-cdt:20030836

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents