Meta-Functional Languages for Hardware Design


Project Description

The high demand for Hardware Description Languages (HDLs) to create larger and complex micro-electronic circuits has been increasing, especially since circuits are being implemented in a wide variety of systems. This has been pushing the industry and academic researchers to produce a more feasible methodology for the development of circuits than the ones offered by standardised languages like VHDL and Verilog. As circuits are becoming even more complex, the process to design, test, debug and implement such hardware is highly effecting the overall costs due to an increase of obscured areas exposed for errors that affect the compilation process, even that of a correct high abstract description.

Hardware can be described using textual descriptions that define either the behavioural, or the structural composition of the circuit. Designing hardware using structural descriptions can be rather tedious and time consuming, since the designer has to indicate what components are used and how these are connected to each other. A traditional proposal to such a situation is to use a higher conceptual level of description, thus giving a behavioural description of the circuit. These behavioural descriptions could then be compiled down to the equivalent structural description of the circuit. Both VHDL and Verilog offer mechanisms to allow both structural and behavioural descriptions, however these do not allow higher-order reasoning to be performed on the textual descriptions, limiting the ability to describe generic and parametrised circuits, which are extremely useful for the generation of large regular-shaped circuit structures.


Embedded Hardware Description Languages

A more practical way to describe circuits at an acceptable level of abstraction is demonstrated in modern HDLs, that have been developed as embedded languages within a general purpose functional language. Functional languages offer ideal grounds for the embedding of such languages, and this is clearly demonstrated in a number of examples, Lava, Hydra, Hawk, and others. These HDLs define the functional aspect of the circuits in terms of high level programs within the host language. These programs or descriptions act as the circuit generators. An instance of these generators creates the described circuits as data objects that can be modified and analysed within the host language. The analogy of a two-level approach can be used to outline the framework. The bottom level would be the host language level, while in the above level lies the HDL, thus the host language has access to the generated circuits. Larger circuits can also be generated using a higher-order logic over the smaller definitions, in particular regular-shaped circuits.

Lava is a structural HDL embedded in the generic functional language Haskell, therefore it permits to write Haskell programs describing generic and parametrised circuits. In this setting, Lava is the meta-language for the hardware being described, but not for the hardware descriptions themselves. One of the successful features of Lava is the ability to interact with external tools such as model checkers. Model checkers offer a technique to verify finite state concurrent systems, which is considered to be a superior technique than simulation, testing and deductive reasoning.

The circuits generated by embedded HDLs are always of a finite size, thus these could easily be model checked directly. However, in practice, circuit generators are mostly of an infinite state when considering their realistic composition. Therefore these circuit generators cannot be model checked automatically. Nonetheless, Pace and Claessen describe a technique how regular descriptions do allow generic reasoning over the produced circuit. This work was achieved through the use of Lava, and showed how certain properties of the compilation process could in fact be verified using finite state model checkers. The problem in using model checking for infinite state circuit generators was avoided through the use of structural induction, which enabled to verify more complex properties.


Using Meta-Programming for Hardware Description Languages

The use of a Meta-Language for hardware descriptions is more recent, yet a number of positive enhancements can already be perceived. Meta-programming was initially introduced by C++ as templates. Templates enabled the compiler to execute code specified in the source program, thus manipulating the compilation process resulting in a manipulated program. Lately, extensions with similar functionality have been introduced to functional languages, where the function definitions could now be treated as data objects without disrupting most of the type-safety constraints.

Meta-programming in a functional setting allows the reasoning and manipulation of the circuit generators themselves and not just the resulting circuits. Meta-ML is an extension to Standard ML offering the meta-programming concept in a function language. The central intention of Meta-ML is to generate programs by defining meta-programs that manipulate object-programs within the meta-language. Experimental work on HDLs, embedded in Meta-ML have reported numerous advantages.

reFLect is another functional language offering built-in meta-programming features. reFLect is a strongly typed functional language similar to ML, developed by Intel aimed at hardware design and verification. The meta-language features in reFLect allow the data structure of the abstact syntax tree of the language itself, to be used by the programmer as a data type. This gives the possibility to create, manipulate and inspect programs written in reFLect, and using the reFLect language itself. Such a setting provides an alternative approach for the embedding of an HDL. Recently an HDL based on Lava, and embedded in the language reFLect has been developed. Nonetheless, the interaction between the hardware generators and this kind of embedding is still an open research.


Project Research

This project is focused to experiment with the usage of meta-programming features on embedded HDLs, using the language reFLect. Embedded HDLs like Lava, can automatically generate circuits, and these can also be manipulated and reasoned about using such a high-level functional language. However, the reasoning about hardware generators themselves has not yet been tackled within the host language itself. The project aims at using the meta-programming features of reFLect to explore how properties of these circuit generators, in particular hardware compilers, can be verified using model checking techniques. This is made possible in the meta-programming setting of reFLect, since the circuit descriptions are made available as data objects within the language itself.

Another issue that is being tackled is the reasoning of the non-functional aspects of the circuits being generated. These properties would include component placement, power consumption, timing and component reuse. Such non-functional properties are usually difficult to define or infer, especially at a high level of abstraction like the functional behaviour of circuits. Additional motivation for this issue is contributed by Wired. Wired is an extension to Lava, where the even placement of wires can be specified within the language. Wired acts as an additional level on top of Lava (as a meta-language), where the connections and placement of components can be specified separately from the functional behaviour of the circuits.

The proposed work is to make use of the meta-programming features of reFLect to develop circuit descriptions that are able to manipulate and reason about the hardware generators themselves. This should provide the possibility to introduce, or implicitly infer, additional information necessary for the non-functional properties of the circuits that are finally generated. Such an approach should be particularly useful for the placement of components. The meta-programming characteristics of reFLect should allow to independently handle the functional and non-functional properties of circuits, within the same host language. These features can then enable to access the circuit generators, and apply model checking techniques related to certain properties of the generators and applying optimisations accordingly.


References
  • Emil Axelsson, Koen Claessen, and Mary Sheeran. Wired: Wire-aware circuit design. In Proc. of Conference on Correct Hardware Design and Verification Methods (CHARME), Springer Verlag.
  • Per Bjesse, Koen Claessen, Mary Sheeran, and Satnam Singh. Lava: Hardware design in Haskell. In Proc. of International Conference on Functional Programming (ICFP). ACM SIGPLAN, 1998.
  • Jim Grundy, Tom Melham, and John O'Leary. A reflective functional language for hardware design and theorem proving. Journal of Functional Programming, 2006.
  • John Launchbury, Jeffrey~R. Lewis, and Byron Cook. On embedding a microarchitectural design language within haskell. SIGPLAN Not., 1999.
  • Roger Lipsett, Erich Marchner, and Moe Shahdad. VHDL - the language. IEEE Design and Test, 1986.
  • Tom Melham and John O'Leary. A functional HDL in reFLect. In Sixth International Workshop on Designing Correct Circuits: Vienna, Participants' Proceedings. A Satellite Event of the ETAPS 2006 group of conferences.
  • John O'Donnell. Overview of hydra: a concurrent language for synchronous digital circuit design. International Journal of Information, 2006.
  • Gordon J. Pace and Koen Claessen. Verifying hardware compilers. In Computer Science Annual Workshop 2005 (CSAW'05). University of Malta, 2005.
  • Walid Taha. Two-level languages and circuit design and synthesis. In Designing Correct Circuits, 2006.

Publications
  • Gordon J. Pace and Christian Tabone, Meta-Functional Languages for Hardware Design and Verification, WICT 2008, Department of Computer Science, University of Malta, 2008. (PDF)
  • Gordon J. Pace and Christian Tabone, Multi-Stage Languages in Hardware Design, Department of Computer Science, University of Malta. Technical Report CSAI2008-01, 2008. (PDF) (BiBTeX)
  • Gordon J. Pace and Christian Tabone, Accessing Circuit Generators in Embedded HDLs, in Proceedings of Designing Correct Circuits 2008 (DCC'08), Budapest, Hungary, 2008. (PDF) (slides)
  • Gordon J. Pace and Christian Tabone, Embedding a Hardware Description Language in a Functional Meta-Programming Language, Computer Science Annual Workshop 2007, Department of Computer Science and AI, University of Malta, 2007. (PDF)

Tools