% should be used if it is desired that the figures are to be displayed in
% draft mode.
%
-\documentclass[conference]{IEEEtran}
+\documentclass[conference,pdf,a4paper,10pt,final,twoside,twocolumn]{IEEEtran}
% Add the compsoc option for Computer Society conferences.
%
% If IEEEtran.cls has not been installed into the LaTeX system files,
% manually specify the path to it like:
% \documentclass[conference]{../sty/IEEEtran}
-
-
-
-
% Some very useful LaTeX packages include:
% (uncomment the ones you want to load)
-
% *** MISC UTILITY PACKAGES ***
%
%\usepackage{ifpdf}
% *** CITATION PACKAGES ***
%
-%\usepackage{cite}
+\usepackage{cite}
% cite.sty was written by Donald Arseneau
% V1.6 and later of IEEEtran pre-defines the format of the cite.sty package
% \cite{} output to follow that of IEEE. Loading the cite package will
% (Unless specifically asked to do so by the journal or conference you plan
% to submit to, of course. )
-
% correct bad hyphenation here
\hyphenation{op-tical net-works semi-conduc-tor}
% Macro for certain acronyms in small caps. Doesn't work with the
% default font, though (it contains no smallcaps it seems).
-\def\VHDL{\textsc{VHDL}}
-\def\GHC{\textsc{GHC}}
+\def\VHDL{\textsc{vhdl}}
+\def\GHC{\textsc{ghc}}
+\def\CLaSH{\textsc{C$\lambda$aSH}}
% Macro for pretty printing haskell snippets. Just monospaced for now, perhaps
% we'll get something more complex later on.
\def\hs#1{\texttt{#1}}
+\def\quote#1{``{#1}"}
\begin{document}
%
% paper title
% can use linebreaks \\ within to get better formatting as desired
-\title{Bare Demo of IEEEtran.cls for Conferences}
+\title{\CLaSH: Structural Descriptions \\ of Synchronous Hardware using Haskell}
% author names and affiliations
% use a multiple column layout for up to three different
% affiliations
-\author{\IEEEauthorblockN{Michael Shell}
-\IEEEauthorblockA{School of Electrical and\\Computer Engineering\\
-Georgia Institute of Technology\\
-Atlanta, Georgia 30332--0250\\
-Email: http://www.michaelshell.org/contact.html}
-\and
-\IEEEauthorblockN{Homer Simpson}
-\IEEEauthorblockA{Twentieth Century Fox\\
-Springfield, USA\\
-Email: homer@thesimpsons.com}
-\and
-\IEEEauthorblockN{James Kirk\\ and Montgomery Scott}
-\IEEEauthorblockA{Starfleet Academy\\
-San Francisco, California 96678-2391\\
-Telephone: (800) 555--1212\\
-Fax: (888) 555--1212}}
+\author{\IEEEauthorblockN{Christiaan P.R. Baaij, Matthijs Kooijman, Jan Kuper, Marco E.T. Gerards, Bert Molenkamp, Sabih H. Gerez}
+\IEEEauthorblockA{University of Twente, Department of EEMCS\\
+P.O. Box 217, 7500 AE, Enschede, The Netherlands\\
+c.p.r.baaij@utwente.nl, matthijs@stdin.nl}}
+% \and
+% \IEEEauthorblockN{Homer Simpson}
+% \IEEEauthorblockA{Twentieth Century Fox\\
+% Springfield, USA\\
+% Email: homer@thesimpsons.com}
+% \and
+% \IEEEauthorblockN{James Kirk\\ and Montgomery Scott}
+% \IEEEauthorblockA{Starfleet Academy\\
+% San Francisco, California 96678-2391\\
+% Telephone: (800) 555--1212\\
+% Fax: (888) 555--1212}}
% conference papers do not typically use \thanks and this command
% is locked out in conference mode. If really needed, such as for
\IEEEpeerreviewmaketitle
-
\section{Introduction}
-
-foo\par bar % Won't compile without at least two paragraphs.
-
+Hardware description languages has allowed the productivity of hardware
+engineers to keep pace with the development of chip technology. Standard
+Hardware description languages, like \VHDL\ and Verilog, allowed an engineer
+to describe circuits using a programming language. These standard languages
+are very good at describing detailed hardware properties such as timing
+behavior, but are generally cumbersome in expressing higher-level
+abstractions. These languages also tend to have a complex syntax and a lack of
+formal semantics. To overcome these complexities, and raise the abstraction
+level, a great number of approaches based on functional languages has been
+proposed \cite{T-Ruby,Hydra,HML2,Hawk1,Lava,ForSyDe1,Wired,reFLect}. The idea
+of using functional languages started in the early 1980s \cite{Cardelli1981,
+muFP,DAISY,FHDL}, a time which also saw the birth of the currently popular
+hardware description languages such as \VHDL.
+
+What gives functional languages as hardware description languages their merits
+is the fact that basic combinatorial circuits are equivalent to mathematical
+function, and that functional languages lend themselves very well to describe
+and compose these mathematical functions.
\section{Hardware description in Haskell}
- To translate Haskell to hardware, every Haskell construct needs a
- translation to \VHDL. There are often multiple valid translations
- possible. When faced with choices, the most obvious choice has been
- chosen wherever possible. In a lot of cases, when a programmer looks
- at a functional hardware description it is completely clear what
- hardware is described. We want our translator to generate exactly that
- hardware whenever possible, to make working with Cλash as intuitive as
- possible.
-
\subsection{Function application}
The basic syntactic elements of a functional program are functions
and function application. These have a single obvious \VHDL\
translation: each top level function becomes a hardware component,
where each argument is an input port and the result value is the
(single) output port. This output port can have a complex type (such
- as a tuple), so having just a single output port does not pose a
+ as a tuple), so having just a single output port does not create a
limitation.
Each function application in turn becomes component instantiation.
Here, the result of each argument expression is assigned to a
signal, which is mapped to the corresponding input port. The output
port of the function is also mapped to a signal, which is used as
- the result of the application.
+ the result of the application itself.
Since every top level function generates its own component, the
hierarchy of of function calls is reflected in the final \VHDL\
hardware. This separation in different components makes the
resulting \VHDL\ output easier to read and debug.
- \subsection{Choice}
- Although describing components and connections allows us to describe
- a lot of hardware designs already, there is an obvious thing
- missing: choice. We need some way to be able to choose between
- values based on another value. In Haskell, choice is achieved by
- \hs{case} expressions, \hs{if} expressions, pattern matching and
- guards.
-
- However, to be able to describe our hardware in a more convenient
- way, we also want to translate Haskell's choice mechanisms. The
- easiest of these are of course case expressions (and \hs{if}
+ Example that defines the \texttt{mac} function by applying the
+ \texttt{add} and \texttt{mul} functions to calculate $a * b + c$:
+
+\begin{verbatim}
+mac a b c = add (mul a b) c
+\end{verbatim}
+
+ TODO: Pretty picture
+
+ \subsection{Choices }
+ Although describing components and connections allows describing a
+ lot of hardware designs already, there is an obvious thing missing:
+ choice. We need some way to be able to choose between values based
+ on another value. In Haskell, choice is achieved by \hs{case}
+ expressions, \hs{if} expressions, pattern matching and guards.
+
+ The easiest of these are of course case expressions (and \hs{if}
expressions, which can be very directly translated to \hs{case}
expressions). A \hs{case} expression can in turn simply be
- translated to a conditional assignment, where the conditions use
- equality comparisons against the constructors in the \hs{case}
- expressions.
+ translated to a conditional assignment in \VHDL, where the
+ conditions use equality comparisons against the constructors in the
+ \hs{case} expressions.
A slightly more complex (but very powerful) form of choice is
pattern matching. A function can be defined in multiple clauses,
where each clause specifies a pattern. When the arguments match the
pattern, the corresponding clause will be used.
+ A pattern match (with optional guards) can also be implemented using
+ conditional assignments in \VHDL, where the condition is the logical
+ and of comparison results of each part of the pattern as well as the
+ guard.
+
+ Contrived example that sums two values when they are equal or
+ non-equal (depending on the predicate given) and returns 0
+ otherwise. This shows three implementations, one using and if
+ expression, one using only case expressions and one using pattern
+ matching and guards.
+
+\begin{verbatim}
+sumif pred a b = if pred == Eq && a == b || pred == Neq && a != b
+ then a + b
+ else 0
+\end{verbatim}
+
+\begin{verbatim}
+sumif pred a b = case pred of
+ Eq -> case a == b of
+ True -> a + b
+ False -> 0
+ Neq -> case a != b of
+ True -> a + b
+ False -> 0
+\end{verbatim}
+
+\begin{verbatim}
+sumif Eq a b | a == b = a + b
+sumif Neq a b | a != b = a + b
+sumif _ _ _ = 0
+\end{verbatim}
+
+ TODO: Pretty picture
+
\subsection{Types}
Translation of two most basic functional concepts has been
discussed: function application and choice. Before looking further
\subsection{Built-in types}
The language currently supports the following built-in types. Of these,
only the \hs{Bool} type is supported by Haskell out of the box (the
- others are defined by the Cλash package, so they are user-defined types
+ others are defined by the \CLaSH\ package, so they are user-defined types
from Haskell's point of view).
\begin{description}
structure. In fact, the built-in tuple types are just algebraic product
types (and are thus supported in exactly the same way).
- The ``product'' in its name refers to the collection of values belonging
- to this type. The collection for a product type is the Cartesian
- product of the collections for the types of its fields.
+ The \quote{product} in its name refers to the collection of values
+ belonging to this type. The collection for a product type is the
+ Cartesian product of the collections for the types of its fields.
These types are translated to \VHDL\ record types, with one field for
every field in the constructor. This translation applies to all single
for our purposes this distinction does not really make a
difference, so this distinction is note made.
- The ``sum'' in its name refers again to the collection of values
+ The \quote{sum} in its name refers again to the collection of values
belonging to this type. The collection for a sum type is the
union of the the collections for each of the constructors.
\end{description}
-\section{C$\lambda$ash prototype}
+\section{\CLaSH\ prototype}
foo\par bar
\section{Related work}
-Many functional hardware description languages have been developed over the years. Early work includes such languages as $\mu$FP~\cite{muFP}, an extension of Backus' FP language to synchronous streams, designed particularly for describing and reasoning about regular circuits. The Ruby~\cite{Ruby} language uses relations, instead of functions, to describe circuits, and has a particular focus on layout. HML~\cite{HML1} is a hardware modeling language based on the strict functional language ML, and has support for polymorphic types and higher-order functions. Published work suggests that there is no direct simulation support for HML, and that the translation to VHDL is only partial.
-
-Like this work, many functional hardware description languages have some sort of foundation in the functional programming language Haskell. Hawk~\cite{Hawk2} uses Haskell to describe system-level executable specifications used to model the behavior of superscalar microprocessors. Hawk specifications can be simulated, but there seems to be no support for automated circuit synthesis. The ForSyDe~\cite{ForSyDe} system uses Haskell to specify abstract system models, which can (manually) be transformed into an implementation model using semantic preserving transformations. ForSyDe has several simulation and synthesis backends, though synthesis is restricted to the synchronous subset of the ForSyDe language.
-
-Lava~\cite{Lava} is a hardware description language that focuses on the structural representation of hardware. Besides support for simulation and circuit synthesis, Lava descriptions can be interfaced with formal method tools for formal verification. Lava descriptions are actually circuit generators when viewed from a synthesis viewpoint, in that the language elements of Haskell, such as choice, can be used to guide the circuit generation. If a developer wants to insert a choice element inside an actual circuit he will have to specify this explicitly as a component. In this respect C$\lambda$aSH differs from Lava, in that all the choice elements, such as case-statements and patter matching, are synthesized to choice elements in the eventual circuit. As such, richer control structures can both be specified and synthesized in C$\lambda$aSH compared to any of the languages mentioned in this section.
-
-The merits of polymorphic typing, combined with higher-order functions, are now also recognized in the `main-stream' hardware description languages, exemplified by the new VHDL 2008 standard~\cite{VHDL2008}. VHDL-2008 has support to specify types as generics, thus allowing a developer to describe polymorphic components. Note that those types still require an explicit generic map, whereas type-inference and type-specialization are implicit in C$\lambda$aSH.
+Many functional hardware description languages have been developed over the
+years. Early work includes such languages as \textsc{$\mu$fp}~\cite{muFP}, an
+extension of Backus' \textsc{fp} language to synchronous streams, designed
+particularly for describing and reasoning about regular circuits. The
+Ruby~\cite{Ruby} language uses relations, instead of functions, to describe
+circuits, and has a particular focus on layout. \textsc{hml}~\cite{HML2} is a
+hardware modeling language based on the strict functional language
+\textsc{ml}, and has support for polymorphic types and higher-order functions.
+Published work suggests that there is no direct simulation support for
+\textsc{hml}, and that the translation to \VHDL\ is only partial.
+
+Like this work, many functional hardware description languages have some sort
+of foundation in the functional programming language Haskell.
+Hawk~\cite{Hawk1} uses Haskell to describe system-level executable
+specifications used to model the behavior of superscalar microprocessors. Hawk
+specifications can be simulated, but there seems to be no support for
+automated circuit synthesis. The ForSyDe~\cite{ForSyDe2} system uses Haskell
+to specify abstract system models, which can (manually) be transformed into an
+implementation model using semantic preserving transformations. ForSyDe has
+several simulation and synthesis backends, though synthesis is restricted to
+the synchronous subset of the ForSyDe language.
+
+Lava~\cite{Lava} is a hardware description language that focuses on the
+structural representation of hardware. Besides support for simulation and
+circuit synthesis, Lava descriptions can be interfaced with formal method
+tools for formal verification. Lava descriptions are actually circuit
+generators when viewed from a synthesis viewpoint, in that the language
+elements of Haskell, such as choice, can be used to guide the circuit
+generation. If a developer wants to insert a choice element inside an actual
+circuit he will have to specify this explicitly as a component. In this
+respect \CLaSH\ differs from Lava, in that all the choice elements, such as
+case-statements and patter matching, are synthesized to choice elements in the
+eventual circuit. As such, richer control structures can both be specified and
+synthesized in \CLaSH\ compared to any of the languages mentioned in this
+section.
+
+The merits of polymorphic typing, combined with higher-order functions, are
+now also recognized in the `main-stream' hardware description languages,
+exemplified by the new \VHDL\ 2008 standard~\cite{VHDL2008}. \VHDL-2008 has
+support to specify types as generics, thus allowing a developer to describe
+polymorphic components. Note that those types still require an explicit
+generic map, whereas type-inference and type-specialization are implicit in
+\CLaSH.
+
+Wired~\cite{Wired},, T-Ruby~\cite{T-Ruby}, Hydra~\cite{Hydra}.
+
+A functional language designed specifically for hardware design is
+$re{\mathit{FL}}^{ect}$~\cite{reFLect}, which draws experience from earlier
+language called \textsc{fl}~\cite{FL} to la
% An example of a floating figure using the graphicx package.
% Note that \label must occur AFTER (or within) \caption.
projects / matthijs / master-project / dsd-paper.git / blobdiff