Per Bjesse
Abstract
Lava is a tool to assist circuit designers in specifying, designing, verifying and implementing hardware. It is a collection of Haskell modules. The system design exploits functional programming language features, such as monads and type classes, to provide multiple interpretations of circuit descriptions. These interpretations implement standard circuit analyses such as simulation, formal verification and the generation of code for the production of real circuits.Lava also uses polymorphism and higher order functions to provide more abstract and general descriptions than are possible in traditional hardware description languages. Two Fast Fourier Transform circuit examples illustrate this.
- Bje97 Per Bjesse. Specification of signal processing programs in a pure functional language and compilation to distributed architectures. Master's thesis, Chalmers University of Technology, 1997.]]Google Scholar
- CLM98 Byron Cook, John Launchbury, and John Matthews. Specifying superscalar microprocessors in Hawk. In Formal Techniques for Hardware and Hardware-like Systems. Marstrand, Sweden, 1998.]]Google Scholar
- Cyr96 David Cyrluk. inverting the abstraction mapping: A methodology for hardware verification. In Formal Methods for Computer Aided Design of Electronic Circuits (FMCAD), number 1166 in Lecture Notes In Computer Science. Springer-Verlag, 1996.]] Google ScholarDigital Library
- Gam98 Ruben Gamboa. Mechanically verifying the correctness of the Fast Fourier Transform in ACL2. In Third International Workshop on Formal Methods for Parallel Programming: Theory and Applications, 1998.]]Google ScholarCross Ref
- HD92 Keith Hanna and Nell Daeche. Dependent types and formal synthesis. Phil. Trans. R. Soc. Lond. A, (339), X992.]]Google Scholar
- He95 Shousheng He. Concurrent VLSI Architectures for DFT Computing and Algorithms for Multi-output Logic Decomposition. PhD thesis, Lund Institute of Technology, 1995.]]Google Scholar
- Jon90 Geraint Jones, A fast flutter by the Fourier transform. In Proceedings IVth Banff Workshop on Higher Order. Springer Workshops in Computing, 1990.]]Google Scholar
- JS90 Geraint Jones and Mary Sheeran. The study of butterflies. In Proceedings IVth Banff Workshop on Higher Order. Springer Workshops in Computing, 1990.]]Google Scholar
- LL95 Yanbing Li and Miriam Leeser. HML: An innovative hardware design language and its translation to VHDL. In Computer Hardware Description Languages (CHDL '95), 1995.]]Google Scholar
- MW97 William W. McCune and L. Wos. Otter: The CADE-13 competition incarnations. Journal of Automated Reasoning, 18(2):211-220, 1997.]] Google ScholarDigital Library
- O'D96 John O'Donnell. From transistors to computer architecture: Teaching functional circuit specification in Hydra. In Functional Programming Languagues in Education, volume 1125 of Lecture Notes In Computer Science, pages 221-234. Springer Verlag, 1996.]] Google ScholarDigital Library
- PM92 John Proakis and Dimitris Manolakis. Digital Signal Processing. Macmillan, 1992.]] Google ScholarDigital Library
- SB98 Mary Sheeran and Arne Bor~ilv. How to prove properties of recursively defined circuits using Stfilmarck's method. In Formal Techniques for Hardware and Hardware-like Systems. Marstrand, Sweden, 1998.]]Google Scholar
- She85 Mary Sheeran. Designing regular array architectures using higher order functions, in Int. Conf. on Functional Programming Languages and Computer Architecture, (Jouannaud ed.), volume 201 of Lecture Notes In Computer Science. Springer Verlag, 1985.]] Google ScholarDigital Library
- Sin91 Satnam Singh. Analysis of Hardware Description Languages. PhD thesis, Computing Science Dept., Glasgow University, 1991.]]Google Scholar
- SR93 Robin Sharp and Ole Rasmussen. Transformational rewriting with Ruby. In Computer Hardware Description Languages (CHDL '93). Elsevier Science Publishers, 1993.]] Google ScholarDigital Library
- Stå89 Gunnar Stf~Imarck. A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula, 1989. Swedish Patent No. 467 076 (approved 1992), U.S. Patent No. 5 276 897 (1994), European Patent No. 0403 454 (1995).]]Google Scholar
- Tam97 Tanel Tammet. Gandalf. Journal of Automated Reasoning, 18(2):199-204, 1997.]] Google ScholarDigital Library
- Wad92 Philip Wadler. Monads for Functional Programming. In Lecture notes for Marktoberdorf Summer School on Program Design Calculi, NATO ASI Series F: Computer and systems sciences. Springer Verlag, August 1992.]]Google Scholar
Index Terms
- Lava: hardware design in Haskell
Recommendations
Lava: hardware design in Haskell
ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programmingLava is a tool to assist circuit designers in specifying, designing, verifying and implementing hardware. It is a collection of Haskell modules. The system design exploits functional programming language features, such as monads and type classes, to ...
Introducing Kansas lava
IFL'09: Proceedings of the 21st international conference on Implementation and application of functional languagesKansas Lava is a domain specific language for hardware description. Though there have been a number of previous implementations of Lava, we have found the design space rich, with unexplored choices. We use a direct (Chalmers style) specification of ...
What's the matter with Kansas Lava?
TFP'10: Proceedings of the 11th international conference on Trends in functional programmingKansas Lava is a functional hardware description language implemented in Haskell. In the course of attempting to generate ever larger circuits, we have found the need to effectively test and debug the internals of Kansas Lava. This includes confirming ...
Reviews
Josep Silva
Hardware design languages have been continuously increasing their abstraction levels over the last 20 years, and languages such as very high speed integrated circuit hardware description language (VHDL) and Verilog have become standards in the field. These languages lack a formal basis, however, which is needed, for instance, to formally verify designed circuits. Nowadays, Haskell (see http://www.haskell.org) is the most important pure functional language. Its strong mathematical foundation (it is based on lambda calculus) makes it a very convenient language to perform formal verification of programs. In this work, the authors describe the hardware design language, Lava, that has been embedded into Haskell. The authors describe how Lava takes advantage of many features of Haskell, such as monads or type classes, to completely describe hardware circuits, and how many existing tools, such as theorem provers (which allow users to perform formal verification of circuits), can be used with Lava. The paper is well written, and clearly explains the advantages and properties of Lava using many examples. Although some related work is described, the authors only mention a short comment about Hawk [1], another language embedded in Haskell, which uses a very similar approach to hardware specification. A more detailed comparison between them would have been very interesting. Finally, Lava has become the core of Claessen's Ph.D. thesis [2], so I refer the interested reader to this document for a more detailed explanation about Lava. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments