Shade - A Structural HDL embedded in reFLect

Embedded Hardware Description Languages
General functional languages, like Haskell, have been used as host languages for the embedding of modern Hardware Description Languages. This field has been widely explored, and improvements where made for the description of circuit generators at higher levels of abstraction, while maintaining the possibility to manipulate or reason about the generated circuits. Nevertheless, a fair amount of uncertainty is still present on how to describe, or infer, non-functional aspects of hardware systems, such as component placement and power consumption, while preserving the abstraction level that has already been established. More recent research has successfully shown how Meta-Programming mechanisms can be included in the functional programming paradigm. The Meta-Functional Programming Language reFLect is a modern example of a strongly-typed functional language with built-in meta-programming features. The meta-functional programming capabilities of reFLect, allow the development of circuit description that are able to manipulate and reason about the circuit generators themselves, thus introducing, or inferring, additional information necessary for the non-functional properties of the circuits being generated.

Shade
Shade is a hardware description language embedded within the meta-functional language reFLect. It uses code quotations and antiquotations to achieve a deep embedding of the described circuits, providing the possibility to describe circuit generators and access the generated circuits as object programs, whilst concealing the meta-programming constructs from the user. Through the use of meta-language constructs Shade offers additional features to enable circuit descriptions to be enhanced with hierarchical block markings of sub-circuits, and optional placement annotations. Furthermore, code quotations are used at a higher level of abstraction, allowing Shade to access the circuit generators themselves, thus providing the possibility to reason about the generators and apply transformations. Shade uses this approach to provide the automatic extraction of verification models reducing user intervention, and consequently reducing user errors.


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

The Toolkit

Overview:
Shade is a structural hardware description language embedded within the meta-functional language reFLect. The tool is not available as a stand-alone application, but as reFLect script files interpreted by Intel's Forte3 tool, which is only available for a Unix or Linux operating system.

Requirements:
Shade is available only as a source distribution. To use the script files you require to install Forte3 available from Intel. Additional information about the Forte3 formal verification system can be found at Tom Melham's web site. The SMV model checker is also required for the verification features provided by Shade.

How to compile:
No compilation is needed to use Shade since this is available as a collection of script files interpreted by the Forte3 tool. After installing the Forte3 tool and the SMV model checker, simply use the command 'load "shade.fl";' either at the Forte3 interpreter or at the beginning of your script file. Additionally modify the script file "run_smv" such that this points to your SMV installation, hence you are required to set execution permissions for this file.

Input syntax:
The input syntax that is used is that of the reFLect language.

Downloads:


Contact details
Gordon J. Pace
Department of Computer Science,
Faculty of Science,
University of Malta,
Msida MSD 06,
MALTA

Tel: (+356) 2340 2504
Fax: (+356) 2132 0539
E-mail: Gordon.Pace@um.edu.mt
Christian Tabone
Department of Computer Science,
Faculty of Science,
University of Malta,
Msida MSD 06,
MALTA

Tel: (+356) 2340 2249
E-mail: christian.tabone@um.edu.mt