Article

A methodology for generating verified combinatorial circuits

Authors:

Kedar N. Swadi,

Walid TahaAuthors Info & Claims

EMSOFT '04: Proceedings of the 4th ACM international conference on Embedded software

Pages 249 - 258

https://doi.org/10.1145/1017753.1017794

Published: 27 September 2004 Publication History

Abstract

High-level programming languages offer significant expressivity but provide little or no guarantees about resource use. Resource-bounded languages --- such as hardware-description languages --- provide strong guarantees about the runtime behavior of computations but often lack mechanisms that allow programmers to write more structured, modular, and reusable programs. To overcome this basic tension in language design, recent work advocated the use of Resource-aware Programming (RAP) languages, which take into account the natural distinction between the development platform and the deployment platform for resource-constrained software.This paper investigates the use of RAP languages for the generation of combinatorial circuits. The key challenge that we encounter is that the RAP approach does not safely admit a mechanism to express a posteriori (post-generation) optimizations. The paper proposes and studies the use of abstract interpretation to overcome this problem. The approach is illustrated using an in-depth analysis of the Fast Fourier Transform (FFT). The generated computations are comparable to those generated by FFTW.

References

[1]

H. Abelson, G.J. Sussman, and J. Sussman. Structure and Interpretation of Computer Programs. The MIT Press (Cambridge, MA) and McGraw-Hill Book Company (New York, NY), 1996. Available online from http://mitpress.mit.edu/sicp/full-text/book/book.html.]]

Digital Library

[2]

Per Bjesse, Koen Claessen, and Mary Sheeran. Lava: Hardware design in Haskell. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP '98), pages 174--184, 1998.]]

Digital Library

[3]

W. Boehm, J. Hammes, B. Draper, M. Chawathe, C. Ross, R. Rinker, and W. Najjar. Mapping a single assignment programming language to reconfigurable systems. In Supercomputing, number 21, pages 117--130, 2002.]]

Digital Library

[4]

Cristiano Calcagno, Walid Taha, Liwen Huang, and Xavier Leroy. Implementing multi-stage languages using ASTs, gensym, and reflection. In Krzysztof Czarnecki, Frank Pfenning, and Yannis Smaragdakis, editors, Generative Programming and Component Engineering (GPCE), Lecture Notes in Computer Science. Springer-Verlag, 2003.]]

Digital Library

[5]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages, pages 238--252. ACM, 1977.]]

Digital Library

[6]

A.H. DeHon. The density advantage of configurable computing. In IEEE Computer, pages 41--49, Apr 2000.]]

Digital Library

[7]

Jason Eckhardt, Roumen Kaiabachev, Oleg Kiselyov, Kedar N. Swadi, and Walid Taha. Monadic multi-stage programming. In preparation, July 2004.]]

[8]

Matteo Frigo. A Fast Fourier Transform compiler. In Proceedings of the Conference on Programming Language Design and Implementation, pages 169--180, 1999.]]

Digital Library

[9]

Jim Grundy, Tom Melham, and John O'Leary. A reflective functional language for hardware design and theorem proving. In Fifth International Workshop on Designing Correct Circuits, March 2004.]]

[10]

Martin Hofmann. A type system for bounded space and functional in-place update. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer-Verlag, 2000.]]

Digital Library

[11]

C. S. Burrus I. W. Selesnick. Automatic generation of prime length FFT programs. In IEEE Transactions on Signal Processing, pages 14--24, Jan 1996.]]

Digital Library

[12]

Geraint Jones and Mary Sheeran. Designing arithmetic circuits by refinement in ruby. In C. C. Morgan R. S. Bird and J. C. P. Woodcock, editors, Mathematics of Program Construction, Lecture Notes in Computer Science. Springer Verlag, 1993.]]

Digital Library

[13]

D. Ku and G.D. Micheli. HardwareC - a language for hardware design (version 2.0). Technical Report CSL-TR-90-419, Stanford University, April 1990.]]

Digital Library

[14]

John Launchbury, Jeffrey R. Lewis, and Byron Cook. On embedding a microarchitectural design language within Haskell. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP '99), Paris, France, September 1999.]]

Digital Library

[15]

Xavier Leroy. Objective Caml, 2000. Available from http://caml.inria.fr/ocaml/.]]

[16]

R. Lipsett, E. Marschner, and M. Shaded. VHDL - The Language. In IEEE Design and Test of Computers, pages 28--41, April 1986.]]

Digital Library

[17]

W.H. Mangione-Smith. Seeking solutions in configurable computing. In IEEE Computer, pages 38--43, Dec 1997.]]

Digital Library

[18]

Andrew K. Martin. HML: A language for high-level design of high-frequency circuits. In Fifth International Workshop on Designing Correct Circuits, March 2004.]]

[19]

Nicholas McKay and Satnam Singh. Dynamic specialisation of XC6200 FPGAs by partial evaluation. In Field-Programmable Logic and Applications. From FPGAs to Computing Paradigm: 8th International Workshop, FPL '98, Tallinn, Estonia, August 1998.]]

Digital Library

[20]

MetaOCaml: A compiled, type-safe multi-stage programming language. Available online from http://www.metaocaml.org/, 2003.]]

[21]

Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1), 1991.]]

Digital Library

[22]

Walid A. Najjar, Wim Boehm, Bruce A. Draper, Jeff Hammes, Robert Rinker, J. Ross Beveridge, Monica Chawathe, and Charles Ross. High-level language abstraction for reconfigurable computing. In IEEE Computer, pages 63--69, August 2003.]]

Digital Library

[23]

John O'Donnell. Integrating formal methods with digital circuit design in Hydra. In Fifth International Workshop on Designing Correct Circuits, March 2004.]]

[24]

Oregon Graduate Institute Technical Reports. P.O. Box 91000, Portland, OR 97291-1000,USA. Available online from ftp://cse.ogi.edu/pub/tech-reports/README.html.]]

[25]

Emir PašaliĆ, Walid Taha, and Tim Sheard. Tagless staged interpreters for typed languages. In the International Conference on Functional Programming (ICFP '02), Pittsburgh, USA, October 2002. ACM.]]

Digital Library

[26]

R. Sharp and A. Mycroft. A higher-level language for hardware synthesis. In Proceedings of the 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 2001.]]

Digital Library

[27]

Walid Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, 1999. Available from {24}.]]

Digital Library

[28]

Walid Taha. A sound reduction semantics for untyped CBN multi-stage computation. Or, the theory of MetaML is non-trivial. In Proceedings of the Workshop on Partial Evaluation and Semantics-Based Program Maniplation (PEPM), Boston, 2000. ACM Press.]]

Digital Library

[29]

Walid Taha. A gentle introduction to multi-stage programming. In Don Batory, Charles Consel, Christian Lengauer, and Martin Odersky, editors, Domain-specific Program Generation, Lecture Notes in Computer Science. Springer-Verlag, 2004.]]

[30]

Walid Taha, Stephan Ellner, and Hongwei Xi. Generating Imperative, Heap-Bounded Programs in a Functional Setting. In Proceedings of the Third International Conference on Embedded Software, Philadelphia, PA, October 2003.]]

[31]

Walid Taha and Michael Florentin Nielsen. Environment classifiers. In The Symposium on Principles of Programming Languages (POPL '03), New Orleans, 2003.]]

Digital Library

[32]

Donald E. Thomas and Philip R. Moorby. The Verilog Hardware Description Language. Kluwer Academic Publishers, 3rd edition, 1996.]]

Digital Library

[33]

Philip Wadler. Comprehending monads. In Proceedings of Symposium on Lisp and Functional Programming, pages 61--78, Nice, France, June 1990. ACM.]]

Digital Library

Cited By

Kovács A(2024)Closure-Free Functional Programming in a Two-Level Type TheoryProceedings of the ACM on Programming Languages10.1145/36746488:ICFP(659-692)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674648
Masuda MKameyama Y(2024)Program generation meets program verificationScience of Computer Programming10.1016/j.scico.2023.103035232:COnline publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1016/j.scico.2023.103035
Kiselyov O(2024)MetaOCaml: Ten Years LaterFunctional and Logic Programming10.1007/978-981-97-2300-3_12(219-236)Online publication date: 2024
https://doi.org/10.1007/978-981-97-2300-3_12
Show More Cited By

Index Terms

A methodology for generating verified combinatorial circuits
1. Hardware
  1. Electronic design automation
    1. High-level and register-transfer level synthesis
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages

Recommendations

General purpose languages should be metalanguages
PEPM '10: Proceedings of the 2010 ACM SIGPLAN workshop on Partial evaluation and program manipulation

In his paper, The Next 700 Programming Languages, the late Landin writes that "most programming languages are partly a way of expressing things in terms of other things and partly a basic set of given things." Landin tries to separate the general ...
A verified staged interpreter is a verified compiler
GPCE '06: Proceedings of the 5th international conference on Generative programming and component engineering

Dependent types and multi-stage programming have both been used, separately, in programming language design and implementation. Each technique has its own advantages --- with dependent types, we can verify aspects of interpreters and compilers such as ...
Forge: generating a high performance DSL implementation from a declarative specification
GPCE '13: Proceedings of the 12th international conference on Generative programming: concepts & experiences

Domain-specific languages provide a promising path to automatically compile high-level code to parallel, heterogeneous, and distributed hardware. However, in practice high performance DSLs still require considerable software expertise to develop and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

EMSOFT '04: Proceedings of the 4th ACM international conference on Embedded software

September 2004

316 pages

ISBN:1581138601

DOI:10.1145/1017753

General Chair:
Giorgio Buttazzo
University of Pavia, Italy

Copyright © 2004 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 September 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

EMSOFT04

Sponsor:

SIGBED

EMSOFT04: Fourth ACM International Conference on Embedded Software 2004

September 27 - 29, 2004

Pisa, Italy

Acceptance Rates

Overall Acceptance Rate 60 of 203 submissions, 30%

Upcoming Conference

ESWEEK '24

Sponsor:
sigbed
sigbed
sigbed

Twentieth Embedded Systems Week

September 29 - October 4, 2024

Raleigh , NC , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

42
Total Citations
View Citations
352
Total Downloads

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

Reflects downloads up to 21 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kovács A(2024)Closure-Free Functional Programming in a Two-Level Type TheoryProceedings of the ACM on Programming Languages10.1145/36746488:ICFP(659-692)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674648
Masuda MKameyama Y(2024)Program generation meets program verificationScience of Computer Programming10.1016/j.scico.2023.103035232:COnline publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1016/j.scico.2023.103035
Kiselyov O(2024)MetaOCaml: Ten Years LaterFunctional and Logic Programming10.1007/978-981-97-2300-3_12(219-236)Online publication date: 2024
https://doi.org/10.1007/978-981-97-2300-3_12
Reynolds THarrison WChadha RAllwein GMcKinna JOmar C(2020)Strongly bounded termination with applications to security and hardware synthesisProceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3406089.3409029(1-10)Online publication date: 23-Aug-2020
https://dl.acm.org/doi/10.1145/3406089.3409029
Kiselyov O(2018)Reconciling Abstraction with High PerformanceFoundations and Trends in Programming Languages10.1561/25000000385:1(1-101)Online publication date: 4-Jun-2018
https://dl.acm.org/doi/10.1561/2500000038
Yallop Jvon Glehn TKammar O(2018)Partially-static data as free extension of algebrasProceedings of the ACM on Programming Languages10.1145/32367952:ICFP(1-30)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236795
Mainland GJohnson J(2017)A Haskell compiler for signal transformsACM SIGPLAN Notices10.1145/3170492.313605652:12(219-232)Online publication date: 23-Oct-2017
https://dl.acm.org/doi/10.1145/3170492.3136056
Amin NRompf T(2017)Collapsing towers of interpretersProceedings of the ACM on Programming Languages10.1145/31581402:POPL(1-33)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158140
Mainland GJohnson JFlatt MErdweg S(2017)A Haskell compiler for signal transformsProceedings of the 16th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3136040.3136056(219-232)Online publication date: 23-Oct-2017
https://dl.acm.org/doi/10.1145/3136040.3136056
Yallop J(2017)Staged generic programmingProceedings of the ACM on Programming Languages10.1145/31102731:ICFP(1-29)Online publication date: 29-Aug-2017
https://dl.acm.org/doi/10.1145/3110273
Show More Cited By

View Options

Get Access

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents