A methodology for generating verified combinatorial circuits

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: Harold Abelson , Gerald J. Sussman, Structure and Interpretation of Computer Programs, MIT Press, Cambridge, MA, 1996
• 2: Per Bjesse , Koen Claessen , Mary Sheeran , Satnam Singh, Lava: hardware design in Haskell, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.174-184, September 26-29, 1998, Baltimore, Maryland, United States
• 3: W. Böhm , J. Hammes , B. Draper , M. Chawathe , C. Ross , R. Rinker , W. Najjar, Mapping a Single Assignment Programming Language to Reconfigurable Systems, The Journal of Supercomputing, v.21 n.2, p.117-130, February 2002 [doi>10.1023/A:1013623303037]
• 4: Cristiano Calcagno , Walid Taha , Liwen Huang , Xavier Leroy, Implementing multi-stage languages using ASTs, Gensym, and reflection, Proceedings of the second international conference on Generative programming and component engineering, p.57-76, September 22-25, 2003, Erfurt, Germany
• 5: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 6: André DeHon, The Density Advantage of Configurable Computing, Computer, v.33 n.4, p.41-49, April 2000 [doi>10.1109/2.839320]
• 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, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.169-180, May 01-04, 1999, Atlanta, Georgia, United States
• 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--Extended Abstract, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.165-179, April 02, 2000
• 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.
• 12: Geraint Jones , Mary Sheeran, Designing Arithmetic Circuits by Refinement in Ruby, Proceedings of the Second International Conference on Mathematics of Program Construction, p.208-232, June 29-July 03, 1992
• 13: David Ku , Giovanni DeMicheli, HardwareC -- A Language for Hardware Design (Version 2.0), Stanford University, Stanford, CA, 1990
• 14: John Launchbury , Jeffrey R. Lewis , Byron Cook, On embedding a microarchitectural design language within Haskell, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.60-69, September 27-29, 1999, Paris, France
• 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.
• 17: William H. Mangione-Smith , Brad Hutchings , David Andrews , André DeHon , Carl Ebeling , Reiner Hartenstein , Oskar Mencer , John Morris , Krishna Palem , Viktor K. Prasanna , Henk A. E. Spaanenburg, Seeking Solutions in Configurable Computing, Computer, v.30 n.12, p.38-43, December 1997 [doi>10.1109/2.642810]
• 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 , Satnam Singh, Dynamic Specialisation of XC6200 FPGAs by Parial Evaluation, Proceedings of the 8th International Workshop on Field-Programmable Logic and Applications, From FPGAs to Computing Paradigm, p.298-307, August 31-September 03, 1998
• 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, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 22: Walid A. Najjar , Wim Böhm , Bruce A. Draper , Jeff Hammes , Robert Rinker , J. Ross Beveridge , Monica Chawathe , Charles Ross, High-Level Language Abstraction for Reconfigurable Computing, Computer, v.36 n.8, p.63-69, August 2003 [doi>10.1109/MC.2003.1220583]
• 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 , Tim Sheard, Tagless staged interpreters for typed languages, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.218-229, October 04-06, 2002, Pittsburgh, PA, USA
• 26: Richard Sharp , Alan Mycroft, A Higher-Level Language for Hardware Synthesis, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.228-243, September 04-07, 2001
• 27: Walid Mohamed Taha , Tim Sheard, Multistage programming: its theory and applications, 1999
• 28: Walid Taha, A sound reduction semantics for untyped CBN mutli-stage computation. Or, the theory of MetaML is non-trival (extended abstract), Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.34-43, January 22-23, 2000, Boston, Massachusetts, United States
• 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 , Michael Florentin Nielsen, Environment classifiers, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.26-37, January 15-17, 2003, New Orleans, Louisiana, USA
• 32: Donald E. Thomas , Philip R. Moorby, The VERILOG Hardware Description Language, Kluwer Academic Publishers, Norwell, MA, 1996
• 33: Philip Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming, p.61-78, June 27-29, 1990, Nice, France [doi>10.1145/91556.91592]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Automatic synthesis

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

General Terms:
Design, Languages, Performance

Keywords:
abstract interpretation, multi-stage programming