Include karel's comments
[matthijs/master-project/dsd-paper.git] / cλash.lhs
index c56eebca684bb9a0b8f7bcffc36d9e9f086832a1..b5653d81d64f4bada76d70bf821fe7eda8202208 100644 (file)
@@ -65,6 +65,7 @@
 %
 
 \documentclass[conference,pdf,a4paper,10pt,final,twoside,twocolumn]{IEEEtran}
+\IEEEoverridecommandlockouts
 % Add the compsoc option for Computer Society conferences.
 %
 % If IEEEtran.cls has not been installed into the LaTeX system files,
 
 % *** PDF, URL AND HYPERLINK PACKAGES ***
 %
-%\usepackage{url}
+\usepackage{url}
 % url.sty was written by Donald Arseneau. It provides better support for
 % handling and breaking URLs. url.sty is already installed on most LaTeX
 % systems. The latest version can be obtained at:
 % Macro for certain acronyms in small caps. Doesn't work with the
 % default font, though (it contains no smallcaps it seems).
 \def\acro#1{{\small{#1}}}
+\def\acrop#1{\acro{#1}s}
+\def\acrotiny#1{{\scriptsize{#1}}}
 \def\VHDL{\acro{VHDL}}
 \def\GHC{\acro{GHC}}
 \def\CLaSH{{\small{C}}$\lambda$a{\small{SH}}}
+\def\CLaSHtiny{{\scriptsize{C}}$\lambda$a{\scriptsize{SH}}}
 
 % Macro for pretty printing haskell snippets. Just monospaced for now, perhaps
 % we'll get something more complex later on.
 \newenvironment{xlist}[1][\rule{0em}{0em}]{%
   \begin{list}{}{%
     \settowidth{\labelwidth}{#1:}
-    \setlength{\labelsep}{0.5cm}
+    \setlength{\labelsep}{0.5em}
     \setlength{\leftmargin}{\labelwidth}
     \addtolength{\leftmargin}{\labelsep}
+    \addtolength{\leftmargin}{\parindent}
     \setlength{\rightmargin}{0pt}
     \setlength{\listparindent}{\parindent}
     \setlength{\itemsep}{0 ex plus 0.2ex}
 \newcommand{\fref}[1]{\cref{#1}} 
 \newcommand{\Fref}[1]{\Cref{#1}}
 
+\usepackage{epstopdf}
+
+\epstopdfDeclareGraphicsRule{.svg}{pdf}{.pdf}{rsvg-convert --format=pdf < #1 > \noexpand\OutputFile}
 
 %include polycode.fmt
 %include clash.fmt
 
+\newcounter{Codecount}
+\setcounter{Codecount}{0}
+
+\newenvironment{example}
+  {
+    \refstepcounter{equation}
+  }
+  {
+      \begin{flushright}
+      (\arabic{equation})
+      \end{flushright}
+  }
+
 \begin{document}
 %
 % paper title
 % author names and affiliations
 % use a multiple column layout for up to three different
 % affiliations
-\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\\
+\author{\IEEEauthorblockN{Christiaan P.R. Baaij, Matthijs Kooijman, Jan Kuper, Marco E.T. Gerards}%, Bert Molenkamp, Sabih H. Gerez}
+\IEEEauthorblockA{%Computer Architecture for Embedded Systems (CAES)\\ 
+Department of EEMCS, University of Twente\\
 P.O. Box 217, 7500 AE, Enschede, The Netherlands\\
-c.p.r.baaij@@utwente.nl, matthijs@@stdin.nl}}
+c.p.r.baaij@@utwente.nl, matthijs@@stdin.nl, j.kuper@@utwente.nl}
+\thanks{Supported through the FP7 project: S(o)OS (248465)}
+}
 % \and
 % \IEEEauthorblockN{Homer Simpson}
 % \IEEEauthorblockA{Twentieth Century Fox\\
@@ -438,10 +462,23 @@ c.p.r.baaij@@utwente.nl, matthijs@@stdin.nl}}
 % make the title area
 \maketitle
 
-
 \begin{abstract}
 %\boldmath
-The abstract goes here.
+\CLaSH\ is a functional hardware description language that borrows both its 
+syntax and semantics from the functional programming language Haskell. 
+Polymorphism and higher-order functions provide a level of abstraction and 
+generality that allow a circuit designer to describe circuits in a more 
+natural way than possible in a traditional hardware description language.
+
+Circuit descriptions can be translated to synthesizable VHDL using the 
+prototype \CLaSH\ compiler. As the circuit descriptions, simulation code, and 
+test input are also valid Haskell, complete simulations can be done by a 
+Haskell compiler allowing high-speed simulation and analysis.
+
+% \CLaSH\ supports stateful descriptions by explicitly making the current 
+% state an argument of the function, and the updated state part of the result. 
+% This makes \CLaSH\ descriptions in essence the combinational parts of a 
+% mealy machine.
 \end{abstract}
 % IEEEtran.cls defaults to using nonbold math in the Abstract.
 % This preserves the distinction between vectors and scalars. However,
@@ -465,176 +502,281 @@ The abstract goes here.
 % creates the second title. It will be ignored for other modes.
 \IEEEpeerreviewmaketitle
 
-
 \section{Introduction}
-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~\cite{VHDL2008} and 
-Verilog~\cite{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. In an attempt to raise the 
-abstraction level of the descriptions, 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 for hardware 
-descriptions 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. The merit of using a functional language to describe 
-hardware comes from the fact that basic combinatorial circuits are equivalent 
-to mathematical functions and that functional languages are very good at 
-describing and composing mathematical functions.
-
-In an attempt to decrease the amount of work involved with creating all the 
-required tooling, such as parsers and type-checkers, many functional hardware 
-description languages are embedded as a domain specific language inside the 
-functional language Haskell \cite{Hydra,Hawk1,Lava,ForSyDe1,Wired}. This 
-means that a developer is given a library of Haskell~\cite{Haskell} functions 
-and types that together form the language primitives of the domain specific 
-language. As a result of how the signals are modeled and abstracted, the 
-functions used to describe a circuit also build a large domain-specific 
-datatype (hidden from the designer) which can be further processed by an 
-embedded compiler. This compiler actually runs in the same environment as the 
-description; as a result compile-time and run-time become hard to define, as 
-the embedded compiler is usually compiled by the same Haskell compiler as the 
-circuit description itself.
-
-The approach taken in this research is not to make another domain specific 
-language embedded in Haskell, but to use (a subset of) the Haskell language 
-itself for the purpose of describing hardware. By taking this approach, we can 
-capture certain language constructs, such as Haskell's choice elements 
-(if-constructs, case-constructs, pattern matching, etc.), which are not 
-available in the functional hardware description languages that are embedded 
-in Haskell as a domain specific languages. As far as the authors know, such 
-extensive support for choice-elements is new in the domain of functional 
-hardware description language. As the hardware descriptions are plain Haskell 
-functions, these descriptions can be compiled for simulation using using the 
-optimizing Haskell compiler \GHC.
-
-Where descriptions in a conventional hardware description language have an 
-explicit clock for the purpose state and synchronicity, the clock is implied 
-in this research. The functions describe the behavior of the hardware between 
-clock cycles, as such, only synchronous systems can be described. Many 
-functional hardware description models signals as a stream of all values over 
-time; state is then modeled as a delay on this stream of values. The approach 
-taken in this research is to make the current state of a circuit part of the 
-input of the function and the updated state part of the output.
-
-Like the standard hardware description languages, descriptions made in a 
-functional hardware description language must eventually be converted into a 
-netlist. This research also features a prototype translator called \CLaSH\ 
-(pronounced: clash), which converts the Haskell code to equivalently behaving 
-synthesizable \VHDL\ code, ready to be converted to an actual netlist format 
-by an optimizing \VHDL\ synthesis tool.
+Hardware description languages (\acrop{HDL}) have not allowed the productivity 
+of hardware engineers to keep pace with the development of chip technology. 
+While traditional \acrop{HDL}, like \VHDL~\cite{VHDL2008} and 
+Verilog~\cite{Verilog}, are very good at describing detailed hardware 
+properties such as timing behavior, they are generally cumbersome in 
+expressing the higher-level abstractions needed for today's large and complex 
+circuit designs. In an attempt to raise the abstraction level of the 
+descriptions, a great number of approaches based on functional languages has 
+been proposed \cite{Cardelli1981,muFP,DAISY,T-Ruby,HML2,Hydra,Hawk1,Lava,
+Wired,ForSyDe1,reFLect}. The idea of using functional languages for hardware 
+descriptions started in the early 1980s \cite{Cardelli1981,muFP,DAISY}, a 
+time which also saw the birth of the currently popular \acrop{HDL}, such as 
+\VHDL. Functional languages are especially well suited to describe hardware 
+because combinational circuits can be directly modeled as mathematical 
+functions and functional languages are very good at describing and composing 
+these functions.
+
+In an attempt to ease the prototyping process of the language, such as 
+creating all the required tooling like parsers and type-checkers, many 
+functional \acrop{HDL} \cite{Hydra,Hawk1,Lava,Wired} are embedded as a domain 
+specific language (\acro{DSL}) within the functional language Haskell 
+\cite{Haskell}. This means that a developer is given a library of Haskell 
+functions and types that together form the language primitives of the 
+\acro{DSL}. The primitive functions used to describe a circuit do not actually 
+process any signals, they instead compose a large domain-specific graph 
+(which is usually hidden from the designer). This graph is then further 
+processed by an embedded circuit compiler which can perform e.g. simulation or 
+synthesis. As Haskell's choice elements (\hs{case}-expressions, 
+pattern-matching, etc.) are evaluated at the time the domain-specific graph is 
+being build, they are no longer visible to the embedded compiler that 
+processes the datatype. Consequently, it is impossible to capture Haskell's 
+choice elements within a circuit description when taking the embedded language 
+approach. This does not mean that circuits specified in an embedded language 
+can not contain choice, just that choice elements only exists as functions, 
+e.g. a multiplexer function, and not as syntactic elements of the language 
+itself.
+
+The approach taken in this research is to use (a subset of) the Haskell 
+language \emph{itself} for the purpose of describing hardware. By taking this 
+approach, this research \emph{can} capture certain language constructs, like 
+all of Haskell's choice elements, within circuit descriptions. The more 
+advanced features of Haskell, such as polymorphic typing and higher-order 
+functions, are also supported.
+
+% supporting polymorphism, higher-order functions and such an extensive array 
+% of choice-elements, combined with a very concise way of specifying circuits 
+% is new in the domain of (functional) \acrop{HDL}. 
+% As the hardware descriptions are plain Haskell 
+% functions, these descriptions can be compiled to an executable binary
+% for simulation using an optimizing Haskell compiler such as the Glasgow
+% Haskell Compiler (\GHC)~\cite{ghc}.
+
+Where descriptions in a conventional \acro{HDL} have an explicit clock for the 
+purposes state and synchronicity, the clock is implicit for the descriptions 
+and research presented in this paper. A circuit designer describes the 
+behavior of the hardware between clock cycles. Many functional \acrop{HDL} 
+model signals as a stream of all values over time; state is then modeled as a 
+delay on this stream of values. Descriptions presented in this research make 
+the current state an additional input and the updated state a part of their 
+output. This abstraction of state and time limits the descriptions to 
+synchronous hardware, there is however room within the language to eventually 
+add a different abstraction mechanism that will allow for the modeling of 
+asynchronous systems.
+
+Likewise as with the traditional \acrop{HDL}, descriptions made in a functional \acro{HDL} must eventually be converted into a netlist. This research also features a prototype compiler, which has the same name as the language: \CLaSH\footnote{\CLaSHtiny: \acrotiny{CAES} Language for Synchronous Hardware, where \acrotiny{CAES} is the acronyom of our chair.} (pronounced: clash). This compiler converts the Haskell code to equivalently behaving synthesizable \VHDL\ code, ready to be converted to an actual netlist format by an (optimizing) \VHDL\ synthesis tool.
+
+To the best knowledge of the authors, \CLaSH\ is the only (functional) 
+\acro{HDL} that allows circuit specification to be written in a very concise 
+way and at the same time support such advanced features as polymorphic typing, 
+user-defined higher-order functions and pattern matching.
 
 \section{Hardware description in Haskell}
+This section describes the basic language elements of \CLaSH\ and the support 
+of these elements within the \CLaSH\ compiler. In various subsections, the 
+relation between the language elements and their eventual netlist 
+representation is also highlighted. 
 
   \subsection{Function application}
-    The basic syntactic elements of a functional program are functions
-    and function application. These have a single obvious translation to a 
-    netlist: every function becomes a component, every function argument is an
-    input port and the result value is of a function is an output port. This 
-    output port can have a complex type (such as a tuple), so having just a 
-    single output port does not create a limitation. Each function application 
-    in turn becomes a 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 itself.
-
-    Since every top level function generates its own component, the
-    hierarchy of function calls is reflected in the final netlist aswell, 
-    creating a hierarchical description of the hardware. This separation in 
-    different components makes the resulting \VHDL\ output easier to read and 
-    debug.
-
-    As an example we can see the netlist of the |mac| function in
-    \Cref{img:mac-comb}; the |mac| function applies both the |mul| and |add|
-    function to calculate $a * b + c$:
+    Two basic elements of a functional program are functions and function 
+    application. These have a single obvious translation to a netlist format: 
+    \begin{inparaenum}
+      \item every function is translated to a component, 
+      \item every function argument is translated to an input port,
+      \item the result value of a function is translated to an output port, 
+            and
+      \item function applications are translated to component instantiations.
+    \end{inparaenum} 
+    The result value can have a composite type (such as a tuple), so having 
+    just a single result value does not pose any limitation. The actual 
+    arguments of a function application are assigned to signals, which are 
+    then mapped to the corresponding input ports of the component. The output 
+    port of the function is also mapped to a signal, which is used as the 
+    result of the application itself. Since every top level function generates 
+    its own component, the hierarchy of function calls is reflected in the 
+    final netlist. %, creating a hierarchical description of the hardware. 
+    % The separation in different components makes it easier for a developer 
+    % to understand and possibly hand-optimize the resulting \VHDL\ output of 
+    % the \CLaSH\ compiler.
+
+    The short example below (\ref{code:mac}) gives a demonstration of 
+    the conciseness that can be achieved with \CLaSH\ when compared with 
+    other (more traditional) \acrop{HDL}. The example is a combinational 
+    multiply-accumulate circuit that works for \emph{any} word length (this 
+    type of polymorphism will be further elaborated in 
+    \Cref{sec:polymorhpism}). The corresponding netlist is depicted in 
+    \Cref{img:mac-comb}.
     
+    \hspace{-1.7em}
+    \begin{minipage}{0.93\linewidth}
     \begin{code}
     mac a b c = add (mul a b) c
     \end{code}
+    \end{minipage}
+    \begin{minipage}{0.07\linewidth}
+      \begin{example}
+      \label{code:mac}
+      \end{example}
+    \end{minipage}
     
     \begin{figure}
-    \centerline{\includegraphics{mac}}
-    \caption{Combinatorial Multiply-Accumulate}
+    \centerline{\includegraphics{mac.svg}}
+    \caption{Combinational Multiply-Accumulate}
     \label{img:mac-comb}
+    \vspace{-1.5em}
     \end{figure}
     
-    The result of using a complex input type can be seen in 
-    \cref{img:mac-comb-nocurry} where the |mac| function now uses a single
-    input tuple for the |a|, |b|, and |c| arguments:
+    The use of a composite result value is demonstrated in the next example 
+    (\ref{code:mac-composite}), where the multiply-accumulate circuit not only 
+    returns the accumulation result, but also the intermediate multiplication 
+    result (see \Cref{img:mac-comb-composite}, where the double arrow suggests 
+    the composite output).
     
+    \hspace{-1.7em}
+    \begin{minipage}{0.93\linewidth}
     \begin{code}
-    mac (a, b, c) = add (mul a b) c
+    mac a b c = (z, add z c)
+      where
+        z = mul a b
     \end{code}
+    \end{minipage}
+    \begin{minipage}{0.07\linewidth}
+      \begin{example}
+      \label{code:mac-composite}
+      \end{example}
+    \end{minipage}
+    \vspace{-1.5em}
     
     \begin{figure}
-    \centerline{\includegraphics{mac-nocurry}}
-    \caption{Combinatorial Multiply-Accumulate (complex input)}
-    \label{img:mac-comb-nocurry}
+    \vspace{1em}
+    \centerline{\includegraphics{mac-nocurry.svg}}
+    \caption{Combinational Multiply-Accumulate (composite output)}
+    \label{img:mac-comb-composite}
+    \vspace{-1.5em}
     \end{figure}
 
   \subsection{Choice}
-    In Haskell, choice can be achieved by a large set of language constructs, 
-    consisting of: \hs{case} constructs, \hs{if-then-else} constructs, 
-    pattern matching, and guards. The easiest of these are the \hs{case} 
-    constructs (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 in \VHDL, where the conditions use 
-    equality comparisons against the constructors in the \hs{case} 
-    expressions. We can see two versions of a contrived example, the first 
-    using a \hs{case} construct and the other using a \hs{if-then-else} 
-    constructs, in the code below. The example sums two values when they are 
-    equal or non-equal (depending on the predicate given) and returns 0 
-    otherwise.
+    In Haskell, choice can be achieved by a large set of syntactic elements, 
+    consisting of: \hs{case} expressions, \hs{if-then-else} expressions, 
+    pattern matching, and guards. The most general of these are the \hs{case} 
+    expressions (\hs{if} expressions can be directly translated to 
+    \hs{case} expressions). When transforming a \CLaSH\ description to a   
+    netlist, a \hs{case} expression is translated to a multiplexer. The 
+    control value of the \hs{case} expression is fed into a number of 
+    comparators, and their combined output forms the selection port of the 
+    multiplexer. The result of each alternative in the \hs{case} expression is 
+    linked to the corresponding input port of the multiplexer.
+    % A \hs{case} expression can in turn simply be translated to a conditional 
+    % assignment in \VHDL, where the conditions use equality comparisons 
+    % against the constructors in the \hs{case} expressions. 
+    
+    % Two versions of a contrived example are displayed below, the first  
+    % (\ref{lst:code3}) using a \hs{case} expression and the second 
+    % (\ref{lst:code4}) using an \hs{if-then-else} expression. Both examples 
+    % sum two values when they are equal or non-equal (depending on the given 
+    % predicate, the \hs{pred} variable) and return 0 otherwise. 
+    
+    A code example (\ref{code:counter1}) that uses a \hs{case} expression and 
+    \hs{if-then-else} expressions is shown below. The function counts up or 
+    down depending on the \hs{direction} variable, and has a \hs{bound} 
+    variable that determines both the upper bound and wrap-around point of the 
+    counter. The \hs{direction} variable is of the following, user-defined, 
+    enumeration datatype:
     
     \begin{code}
-    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
+    data Direction = Up | Down
     \end{code}
 
-    \begin{code}
-    sumif pred a b = 
-      if pred == Eq then 
-        if a == b then a + b else 0
-      else 
-        if a != b then a + b else 0
+    The naive netlist corresponding to this example is depicted in 
+    \Cref{img:counter}. Note that the \hs{direction} variable is only
+    compared to \hs{Up}, as an inequality immediately implies that 
+    \hs{direction} is \hs{Down} (as derived by the compiler).
+
+    \hspace{-1.7em}
+    \begin{minipage}{0.93\linewidth}
+    \begin{code}    
+    counter bound direction x = case direction of
+        Up    -> if   x < bound   then 
+                      x + 1       else 
+                      0
+        Down  -> if   x > 0       then 
+                      x - 1       else 
+                      bound
     \end{code}
+    \end{minipage}
+    \begin{minipage}{0.07\linewidth}
+      \begin{example}
+      \label{code:counter1}
+      \end{example}
+    \end{minipage}
+    
+    % \hspace{-1.7em}
+    % \begin{minipage}{0.93\linewidth}
+    % \begin{code}
+    % sumif pred a b = 
+    %   if pred == Equal then 
+    %     if a == b then a + b else 0
+    %   else 
+    %     if a != b then a + b else 0
+    % \end{code}
+    % \end{minipage}
+    % \begin{minipage}{0.07\linewidth}
+    %   \begin{example}
+    %   \label{lst:code4}
+    %   \end{example}
+    % \end{minipage}
 
-    Both versions of the example correspond to the same netlist, which is 
-    depicted in \Cref{img:choice}
+    % \begin{figure}
+    % \vspace{1em}
+    % \centerline{\includegraphics{choice-case.svg}}
+    % \caption{Choice - sumif}
+    % \label{img:choice}
+    % \vspace{-1.5em}
+    % \end{figure}
 
     \begin{figure}
-    \centerline{\includegraphics{choice-case}}
-    \caption{Choice - sumif}
-    \label{img:choice}
+    \centerline{\includegraphics{counter.svg}}
+    \caption{Counter netlist}
+    \label{img:counter}
+    \vspace{-2em}
     \end{figure}
 
-    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. Expressions can also contain guards, 
-    where the expression is only executed if the guard evaluates to true. A 
-    pattern match (with optional guards) can be to a conditional assignments 
-    in \VHDL, where the conditions are an equality test of the argument and 
-    one of the patterns (combined with the guard if was present). A third 
-    version of the earlier example, using both pattern matching and guards, 
-    can be seen below:
+    A user-friendly and also very powerful form of choice that is not found in 
+    the traditional hardware description languages is pattern matching. A 
+    function can be defined in multiple clauses, where each clause corresponds 
+    to a pattern. When an argument matches a pattern, the corresponding clause 
+    will be used. Expressions can also contain guards, where the expression is 
+    only executed if the guard evaluates to true, and continues with the next 
+    clause if the guard evaluates to false. Like \hs{if-then-else} 
+    expressions, pattern matching and guards have a (straightforward) 
+    translation to \hs{case} expressions and can as such be mapped to 
+    multiplexers. A second version (\ref{code:counter2}) of the earlier 
+    example, now using both pattern matching and guards, can be seen below. 
+    The guard is the expression that follows the vertical bar (\hs{|}) and 
+    precedes the assignment operator (\hs{=}). The \hs{otherwise} guards 
+    always evaluate to \hs{true}.
     
+    The second version corresponds to the same naive netlist representation 
+    (\Cref{img:counter}) as the earlier example.
+    
+    \hspace{-1.7em}
+    \begin{minipage}{0.93\linewidth}
     \begin{code}
-    sumif Eq a b    | a == b = a + b
-    sumif Neq a b   | a != b = a + b
-    sumif _ _ _     = 0
+    counter bound Up    x  | x < bound  = x + 1
+                           | otherwise  = 0
+                           
+    counter bound Down  x  | x > 0      = x - 1
+                           | otherwise  = bound
     \end{code}
-    
-    The version using pattern matching and guards has the same netlist 
-    representation (\Cref{img:choice}) as the earlier two versions of the 
-    example.
+    \end{minipage}
+    \begin{minipage}{0.07\linewidth}
+      \begin{example}
+      \label{code:counter2}
+      \end{example}
+    \end{minipage}
 
     % \begin{figure}
     % \centerline{\includegraphics{choice-ifthenelse}}
@@ -643,402 +785,894 @@ by an optimizing \VHDL\ synthesis tool.
     % \end{figure}
 
   \subsection{Types}
-    Translation of two most basic functional concepts has been
-    discussed: function application and choice. Before looking further
-    into less obvious concepts like higher-order expressions and
-    polymorphism, the possible types that can be used in hardware
-    descriptions will be discussed.
-
-    Some way is needed to translate every value used to its hardware
-    equivalents. In particular, this means a hardware equivalent for
-    every \emph{type} used in a hardware description is needed.
-
-    The following types are \emph{built-in}, meaning that their hardware
-    translation is fixed into the \CLaSH\ compiler. A designer can also
-    define his own types, which will be translated into hardware types
-    using translation rules that are discussed later on.
-
-  \subsection{Built-in types}
+    Haskell is a statically-typed language, meaning that the type of a 
+    variable or function is determined at compile-time. Not all of 
+    Haskell's typing constructs have a clear translation to hardware, this 
+    section therefor only deals with the types that do have a clear 
+    correspondence to hardware. The translatable types are divided into two 
+    categories: \emph{built-in} types and \emph{user-defined} types. Built-in 
+    types are those types for which a fixed translation is defined within the 
+    \CLaSH\ compiler. The \CLaSH\ compiler has generic translation rules to
+    translate the user-defined types, which are described later on.
+
+    The \CLaSH\ compiler is able to infer unspecified (polymorphic) types,
+    meaning that a developer does not have to annotate every function with a 
+    type signature. Given that the top-level entity of a circuit design is 
+    annotated with specific types, the \CLaSH\ compiler can specialize 
+    polymorphic functions to functions with specific types.
+  
+    % Translation of two most basic functional concepts has been
+    % discussed: function application and choice. Before looking further
+    % into less obvious concepts like higher-order expressions and
+    % polymorphism, the possible types that can be used in hardware
+    % descriptions will be discussed.
+    % 
+    % Some way is needed to translate every value used to its hardware
+    % equivalents. In particular, this means a hardware equivalent for
+    % every \emph{type} used in a hardware description is needed.
+    % 
+    % The following types are \emph{built-in}, meaning that their hardware
+    % translation is fixed into the \CLaSH\ compiler. A designer can also
+    % define his own types, which will be translated into hardware types
+    % using translation rules that are discussed later on.
+
+  \subsubsection{Built-in types}
+    The following types have fixed translations defined within the \CLaSH\
+    compiler:
     \begin{xlist}
-      \item[\hs{Bit}]
-        This is the most basic type available. It can have two values:
-        \hs{Low} and \hs{High}. It is mapped directly onto the
-        \texttt{std\_logic} \VHDL\ type. 
-      \item[\hs{Bool}]
-        This is a basic logic type. It can have two values: \hs{True}
-        and \hs{False}. It is translated to \texttt{std\_logic} exactly
-        like the \hs{Bit} type (where a value of \hs{True} corresponds
-        to a value of \hs{High}). Supporting the Bool type is
-        particularly useful to support \hs{if ... then ... else ...}
-        expressions, which always have a \hs{Bool} value for the
-        condition.
-      \item[\hs{SizedWord}, \hs{SizedInt}]
-        These are types to represent integers. A \hs{SizedWord} is unsigned,
-        while a \hs{SizedInt} is signed. These types are parametrized by a
-        length type, so you can define an unsigned word of 32 bits wide as
-        follows:
-
-        \begin{code}
-        type Word32 = SizedWord D32
-        \end{code}
-
-        Here, a type synonym \hs{Word32} is defined that is equal to the
-        \hs{SizedWord} type constructor applied to the type \hs{D32}. \hs{D32}
-        is the \emph{type level representation} of the decimal number 32,
-        making the \hs{Word32} type a 32-bit unsigned word. These types are 
-        translated to the \VHDL\ \texttt{unsigned} and \texttt{signed} 
-        respectively.
-      \item[\hs{Vector}]
-        This is a vector type, that can contain elements of any other type and
-        has a fixed length. The \hs{Vector} type constructor takes two type 
-        arguments: the length of the vector and the type of the elements 
-        contained in it. The state type of an 8 element register bank would 
-        then for example be:
+      \item[\bf{Bit}]
+        the most basic type available. It can have two values:
+        \hs{Low} or \hs{High}. 
+        % It is mapped directly onto the \texttt{std\_logic} \VHDL\ type. 
+      \item[\bf{Bool}]
+        this is a basic logic type. It can have two values: \hs{True}
+        or \hs{False}. 
+        % It is translated to \texttt{std\_logic} exactly like the \hs{Bit} 
+        % type (where a value of \hs{True} corresponds to a value of 
+        % \hs{High}). 
+        Supporting the Bool type is required in order to support the
+        \hs{if-then-else} expression.
+      \item[\bf{Signed}, \bf{Unsigned}]
+        these are types to represent integers, and both are parametrizable in 
+        their size. The overflow behavior of the numeric operators defined for 
+        these types is \emph{wrap-around}.
+        % , so you can define an unsigned word of 32 bits wide as follows:
+
+        % \begin{code}
+        % type Word32 = SizedWord D32
+        % \end{code}
+
+        % Here, a type synonym \hs{Word32} is defined that is equal to the
+        % \hs{SizedWord} type constructor applied to the type \hs{D32}. 
+        % \hs{D32} is the \emph{type level representation} of the decimal 
+        % number 32, making the \hs{Word32} type a 32-bit unsigned word. These 
+        % types are translated to the \VHDL\ \texttt{unsigned} and 
+        % \texttt{signed} respectively.
+      \item[\bf{Vector}]
+        this type can contain elements of any type and has a static length. 
+        The \hs{Vector} type constructor takes two arguments: the length of 
+        the vector and the type of the elements contained in it. The 
+        short-hand notation used for the vector type in the rest of paper is: 
+        \hs{[a|n]}, where \hs{a} is the element type, and \hs{n} is the length 
+        of the vector. 
+        % Note that this is a notation used in this paper only, vectors are 
+        % slightly more verbose in real \CLaSH\ descriptions.
+        % The state type of an 8 element register bank would then for example 
+        % be:
+
+        % \begin{code}
+        % type RegisterState = Vector D8 Word32
+        % \end{code}
+
+        % Here, a type synonym \hs{RegisterState} is defined that is equal to
+        % the \hs{Vector} type constructor applied to the types \hs{D8} (The 
+        % type level representation of the decimal number 8) and \hs{Word32} 
+        % (The 32 bit word type as defined above). In other words, the 
+        % \hs{RegisterState} type is a vector of 8 32-bit words. A fixed size 
+        % vector is translated to a \VHDL\ array type.
+      \item[\bf{Index}]
+        the main purpose of the \hs{Index} type is to be used as an index into 
+        a \hs{Vector}, and has an integer range from zero to a specified upper 
+        bound.
+        % This means that its range is not limited to powers of two, but 
+        % can be any number.  
+        If a value of this type exceeds either bounds, an error will be thrown 
+        during simulation. 
+
+        % \comment{TODO: Perhaps remove this example?} To define an index for 
+        % the 8 element vector above, we would do:
+
+        % \begin{code}
+        % type RegisterIndex = RangedWord D7
+        % \end{code}
+
+        % Here, a type synonym \hs{RegisterIndex} is defined that is equal to
+        % the \hs{RangedWord} type constructor applied to the type \hs{D7}. In
+        % other words, this defines an unsigned word with values from
+        % 0 to 7 (inclusive). This word can be be used to index the
+        % 8 element vector \hs{RegisterState} above. This type is translated 
+        % to the \texttt{unsigned} \VHDL type.
+    \end{xlist}
 
+  \subsubsection{User-defined types}
+    % There are three ways to define new types in Haskell: algebraic
+    % data-types with the \hs{data} keyword, type synonyms with the \hs{type}
+    % keyword and datatype renaming constructs with the \hs{newtype} keyword. 
+    % \GHC\ offers a few more advanced ways to introduce types (type families,
+    % existential typing, {\acro{GADT}}s, etc.) which are not standard 
+    % Haskell. As it is currently unclear how these advanced type constructs 
+    % correspond to hardware, they are for now unsupported by the \CLaSH\ 
+    % compiler.
+    A designer may define a completely new type by an algebraic datatype 
+    declaration using the \hs{data} keyword. Type synonyms can be introduced 
+    using the \hs{type} keyword.
+    % Only an algebraic datatype declaration actually introduces a
+    % completely new type. Type synonyms and type renaming only define new 
+    % names for existing types, where synonyms are completely interchangeable 
+    % and a type renaming requires an explicit conversion. 
+    Type synonyms do not need any particular translation, as a synonym will 
+    use the same representation as the original type. 
+    
+    Algebraic datatypes can be categorized as follows:
+    \begin{xlist}
+      \item[\bf{Single constructor}]
+        datatypes with a single constructor with one or more fields allow 
+        values to be packed together in a record-like structure. Haskell's 
+        built-in tuple types are also defined as single constructor algebraic 
+        types (using a bit of syntactic sugar). An example of a  single 
+        constructor type with multiple fields is the following pair of 
+        integers:
         \begin{code}
-        type RegisterState = Vector D8 Word32
+        data IntPair = IntPair Int Int
         \end{code}
-
-        Here, a type synonym \hs{RegisterState} is defined that is equal to
-        the \hs{Vector} type constructor applied to the types \hs{D8} (The 
-        type level representation of the decimal number 8) and \hs{Word32} 
-        (The 32 bit word type as defined above). In other words, the 
-        \hs{RegisterState} type is a vector of 8 32-bit words. A fixed size 
-        vector is translated to a \VHDL\ array type.
-      \item[\hs{RangedWord}]
-        This is another type to describe integers, but unlike the previous
-        two it has no specific bit-width, but an upper bound. This means that
-        its range is not limited to powers of two, but can be any number.
-        A \hs{RangedWord} only has an upper bound, its lower bound is
-        implicitly zero. The main purpose of the \hs{RangedWord} type is to be 
-        used as an index to a \hs{Vector}.
-
-        \comment{TODO: Perhaps remove this example?} To define an index for 
-        the 8 element vector above, we would do:
-
+        % These types are translated to \VHDL\ record types, with one field 
+        % for every field in the constructor.
+      \item[\bf{Multiple constructors, No fields}]
+        datatypes with multiple constructors, but without any
+        fields are essentially enumeration types. 
+        % Note that Haskell's \hs{Bool} type is also defined as an enumeration 
+        % type, but that there is a fixed translation for that type within the 
+        % \CLaSH\ compiler. 
+        An example of an enumeration type definition is:
         \begin{code}
-        type RegisterIndex = RangedWord D7
+        data TrafficLight = Red | Orange | Green
         \end{code}
-
-        Here, a type synonym \hs{RegisterIndex} is defined that is equal to
-        the \hs{RangedWord} type constructor applied to the type \hs{D7}. In
-        other words, this defines an unsigned word with values from
-        0 to 7 (inclusive). This word can be be used to index the
-        8 element vector \hs{RegisterState} above. This type is translated to 
-        the \texttt{unsigned} \VHDL type.
-    \end{xlist}
-
-  \subsection{User-defined types}
-    There are three ways to define new types in Haskell: algebraic
-    data-types with the \hs{data} keyword, type synonyms with the \hs{type}
-    keyword and type renamings with the \hs{newtype} keyword. \GHC\
-    offers a few more advanced ways to introduce types (type families,
-    existential typing, {\small{GADT}}s, etc.) which are not standard
-    Haskell. These are not currently supported.
-
-    Only an algebraic datatype declaration actually introduces a
-    completely new type, for which we provide the \VHDL\ translation
-    below. Type synonyms and renamings only define new names for
-    existing types (where synonyms are completely interchangeable and
-    renamings need explicit conversion). Therefore, these do not need
-    any particular \VHDL\ translation, a synonym or renamed type will
-    just use the same representation as the original type. The
-    distinction between a renaming and a synonym does no longer matter
-    in hardware and can be disregarded in the generated \VHDL.
-
-    For algebraic types, we can make the following distinction: 
-
-    \begin{xlist}
-      \item[\bf{Single constructor}]
-        Algebraic datatypes with a single constructor with one or more
-        fields, are essentially a way to pack a few values together in a
-        record-like structure. An example of such a type is the following pair 
-        of integers:
-
-\begin{code}
-data IntPair = IntPair Int Int
-\end{code}
-
-        Haskell's builtin tuple types are also defined as single
-        constructor algebraic types and are translated according to this
-        rule by the \CLaSH\ compiler. These types are translated to \VHDL\ 
-        record types, with one field for every field in the constructor.
-      \item[\bf{No fields}]
-        Algebraic datatypes with multiple constructors, but without any
-        fields are essentially a way to get an enumeration-like type
-        containing alternatives. Note that Haskell's \hs{Bool} type is also 
-        defined as an enumeration type, but we have a fixed translation for 
-        that. These types are translated to \VHDL\ enumerations, with one 
-        value for each constructor. This allows references to these 
-        constructors to be translated to the corresponding enumeration value.
+        % These types are translated to \VHDL\ enumerations, with one 
+        % value for each constructor. This allows references to these 
+        % constructors to be translated to the corresponding enumeration 
+        % value.
       \item[\bf{Multiple constructors with fields}]
-        Algebraic datatypes with multiple constructors, where at least
-        one of these constructors has one or more fields are not
-        currently supported.
+        datatypes with multiple constructors, where at least
+        one of these constructors has one or more fields are currently not 
+        supported. Additional research is required to optimize the overlap of
+        fields belonging to the different constructors.
     \end{xlist}
 
-  \subsection{Polymorphic functions}
-    A powerful construct in most functional language is polymorphism.
-    This means the arguments of a function (and consequentially, values
-    within the function as well) do not need to have a fixed type.
-    Haskell supports \emph{parametric polymorphism}, meaning a
-    function's type can be parameterized with another type.
-
-    As an example of a polymorphic function, consider the following
-    \hs{append} function's type:
+  \subsection{Polymorphism}\label{sec:polymorhpism}
+    A powerful feature of some programming languages is polymorphism, it 
+    allows a function to handle values of different data types in a uniform 
+    way. Haskell supports \emph{parametric polymorphism}, meaning that 
+    functions can be written without mentioning specific types, and they can 
+    be used for arbitrary types.
+
+    As an example of a parametric polymorphic function, consider the type of 
+    the following \hs{first} function, which returns the first element of a 
+    tuple:\footnote{The \hs{::} operator is used to annotate a function
+    with its type.}
     
-    TODO: Use vectors instead of lists?
-
     \begin{code}
-    append :: [a] -> a -> [a]
+    first :: (a,b) -> a
     \end{code}
 
-    This type is parameterized by \hs{a}, which can contain any type at
-    all. This means that append can append an element to a list,
-    regardless of the type of the elements in the list (but the element
-    added must match the elements in the list, since there is only one
-    \hs{a}).
-
-    This kind of polymorphism is extremely useful in hardware designs to
-    make operations work on a vector without knowing exactly what elements
-    are inside, routing signals without knowing exactly what kinds of
-    signals these are, or working with a vector without knowing exactly
-    how long it is. Polymorphism also plays an important role in most
-    higher order functions, as we will see in the next section.
-
-    The previous example showed unconstrained polymorphism (TODO: How is
-    this really called?): \hs{a} can have \emph{any} type. Furthermore,
-    Haskell supports limiting the types of a type parameter to specific
-    class of types. An example of such a type class is the \hs{Num}
-    class, which contains all of Haskell's numerical types.
-
-    Now, take the addition operator, which has the following type:
-
+    This type is parameterized in \hs{a} and \hs{b}, which can both 
+    represent any type at all, as long as that type is supported by the 
+    \CLaSH\ compiler. This means that \hs{first} works for any tuple, 
+    regardless of what elements it contains. This kind of polymorphism is 
+    extremely useful in hardware designs, for example when routing signals 
+    without knowing their exact type, or specifying vector operations that 
+    work on vectors of any length and element type. Polymorphism also plays an 
+    important role in most higher order functions, as will be shown in the 
+    next section.
+
+    % Another type of polymorphism is \emph{ad-hoc 
+    % polymorphism}~\cite{polymorphism}, which refers to polymorphic 
+    % functions which can be applied to arguments of different types, but 
+    % which behave differently depending on the type of the argument to which 
+    % they are applied. In Haskell, ad-hoc polymorphism is achieved through 
+    % the use of \emph{type classes}, where a class definition provides the 
+    % general interface of a function, and class \emph{instances} define the 
+    % functionality for the specific types. An example of such a type class is 
+    % the \hs{Num} class, which contains all of Haskell's numerical 
+    % operations. A designer can make use of this ad-hoc polymorphism by 
+    % adding a \emph{constraint} to a parametrically polymorphic type 
+    % variable. Such a constraint indicates that the type variable can only be 
+    % instantiated to a type whose members supports the overloaded functions 
+    % associated with the type class. 
+    
+    Another type of polymorphism is \emph{ad-hoc polymorphism}, which refers
+    to function that can be applied to arguments of a limited set to types.
+    Furthermore, how such functions work may depend on the type of their
+    arguments. For example, addition only works for numeric types, and it 
+    works differently for e.g. integers and complex numbers.
+    
+    In Haskell, ad-hoc polymorphism is achieved through the use of \emph{type
+    classes}, where a class definition provides the general interface of a 
+    function, and class \emph{instances} define the functionality for the 
+    specific types. For example, all numeric operators are gathered in the 
+    \hs{Num} class, so every type that wants to use those operators must be
+    made an instance of \hs{Num}.
+    
+    By prefixing a type signature with class constraints, the constrained type 
+    parameters are forced to belong to that type class. For example, the 
+    arguments of the \hs{add} function must belong to the \hs{Num} type class 
+    because the \hs{add} function adds them with the (+) operator:
+    
     \begin{code}
-    (+) :: Num a => a -> a -> a
+    add :: Num a => a -> a -> a
+    add a b = a + b
     \end{code}
+    
+    % An example of a type signature that includes such a constraint if the 
+    % signature of the \hs{sum} function, which sums the values in a vector:
+    % \begin{code}
+    % sum :: Num a => [a|n] -> a
+    % \end{code}
+    % 
+    % This type is again parameterized by \hs{a}, but it can only contain
+    % types that are \emph{instances} of the \emph{type class} \hs{Num}, so 
+    % that the compiler knows that the addition (+) operator is defined for 
+    % that type.
+    
+    % A place where class constraints also play a role is in the size and 
+    % range parameters of the \hs{Vector} and numeric types. The reason being 
+    % that these parameters have to be limited to types that can represent 
+    % \emph{natural} numbers. The complete type of for example the \hs{Vector} 
+    % type is:
+    % \begin{code}
+    % Natural n => Vector n a
+    % \end{code}    
+    
+    % \CLaSH's built-in numerical types are also instances of the \hs{Num} 
+    % class. 
+    % so we can use the addition operator (and thus the \hs{sum}
+    % function) with \hs{Signed} as well as with \hs{Unsigned}.
+
+    \CLaSH\ supports both parametric polymorphism and ad-hoc polymorphism. A
+    circuit designer can specify his own type classes and corresponding 
+    instances. The \CLaSH\ compiler will infer the type of every polymorphic 
+    argument depending on how the function is applied. There is however one 
+    constraint: the top level function that is being translated can not have 
+    polymorphic arguments. The arguments of the top-level can not be 
+    polymorphic as there is no way to infer the \emph{specific} types of the 
+    arguments. 
+    
+    With regard to the built-in types, it should be noted that members of 
+    some of the standard Haskell type classes are supported as built-in 
+    functions. These include: the numerial operators of \hs{Num}, the equality 
+    operators of \hs{Eq}, and the comparison (order) operators of \hs{Ord}.
 
-    This type is again parameterized by \hs{a}, but it can only contain
-    types that are \emph{instances} of the \emph{type class} \hs{Num}.
-    Our numerical built-in types are also instances of the \hs{Num}
-    class, so we can use the addition operator on \hs{SizedWords} as
-    well as on {SizedInts}.
-
-    In \CLaSH, unconstrained polymorphism is completely supported. Any
-    function defined can have any number of unconstrained type
-    parameters. The \CLaSH\ compiler will infer the type of every such
-    argument depending on how the function is applied. There is one
-    exception to this: The top level function that is translated, can
-    not have any polymorphic arguments (since it is never applied, so
-    there is no way to find out the actual types for the type
-    parameters).
-
-    \CLaSH\ does not support user-defined type classes, but does use some
-    of the builtin ones for its builtin functions (like \hs{Num} and
-    \hs{Eq}).
-
-  \subsection{Higher order}
+  \subsection{Higher-order functions \& values}
     Another powerful abstraction mechanism in functional languages, is
-    the concept of \emph{higher order functions}, or \emph{functions as
-    a first class value}. This allows a function to be treated as a
-    value and be passed around, even as the argument of another
-    function. Let's clarify that with an example:
+    the concept of \emph{functions as a first class value} and
+    \emph{higher-order functions}. These concepts allows a function to be 
+    treated as a value and be passed around, even as the argument of another
+    function. The following example clarifies this concept:
     
+    \hspace{-1.7em}
+    \begin{minipage}{0.93\linewidth}
+    %format not = "\mathit{not}"
     \begin{code}
-    notList xs = map not xs
+    negate{-"\!\!\!"-}Vector xs = map not xs
     \end{code}
-
-    This defines a function \hs{notList}, with a single list of booleans
-    \hs{xs} as an argument, which simply negates all of the booleans in
-    the list. To do this, it uses the function \hs{map}, which takes
-    \emph{another function} as its first argument and applies that other
-    function to each element in the list, returning again a list of the
-    results.
-
-    As you can see, the \hs{map} function is a higher order function,
-    since it takes another function as an argument. Also note that
-    \hs{map} is again a polymorphic function: It does not pose any
-    constraints on the type of elements in the list passed, other than
-    that it must be the same as the type of the argument the passed
-    function accepts. The type of elements in the resulting list is of
-    course equal to the return type of the function passed (which need
-    not be the same as the type of elements in the input list). Both of
-    these can be readily seen from the type of \hs{map}:
+    \end{minipage}
+    \begin{minipage}{0.07\linewidth}
+      \begin{example}
+      \label{code:negatevector}
+      \end{example}
+    \end{minipage}
+
+    The code above defines the \hs{negate{-"\!\!\!"-}Vector} function, which 
+    takes a vector of booleans, \hs{xs}, and returns a vector where all the 
+    values are negated. It achieves this by calling the \hs{map} function, and 
+    passing it another \emph{function}, boolean negation, and the vector of 
+    booleans, \hs{xs}. The \hs{map} function applies the negation function to 
+    all the elements in the vector.
+
+    The \hs{map} function is called a higher-order function, since it takes 
+    another function as an argument. Also note that \hs{map} is again a 
+    parametric polymorphic function: it does not pose any constraints on the 
+    type of the input vector, other than that its elements must have the same 
+    type as the first argument of the function passed to \hs{map}. The element 
+    type of the resulting vector is equal to the return type of the function 
+    passed, which need not necessarily be the same as the element type of the 
+    input vector. All of these characteristics can be inferred from the type 
+    signature belonging to \hs{map}:
 
     \begin{code}
-    map :: (a -> b) -> [a] -> [b]
+    map :: (a -> b) -> [a|n] -> [b|n]
     \end{code}
-    
-    As an example from a common hardware design, let's look at the
-    equation of a FIR filter.
-
-    \begin{equation}
-    y_t  = \sum\nolimits_{i = 0}^{n - 1} {x_{t - i}  \cdot h_i } 
-    \end{equation}
-
-    A FIR filter multiplies fixed constants ($h$) with the current and
-    a few previous input samples ($x$). Each of these multiplications
-    are summed, to produce the result at time $t$.
 
-    This is easily and directly implemented using higher order
-    functions. Consider that the vector \hs{hs} contains the FIR
-    coefficients and the vector \hs{xs} contains the current input sample
-    in front and older samples behind. How \hs{xs} gets its value will be
-    show in the next section about state.
+    In Haskell, there are two more ways to obtain a function-typed value:
+    partial application and lambda abstraction. Partial application means that 
+    a function that takes multiple arguments can be applied to a single 
+    argument, and the result will again be a function, but takes one argument 
+    less. As an example, consider the following expression, that adds one to 
+    every element of a vector:
 
+    \hspace{-1.7em}
+    \begin{minipage}{0.93\linewidth}
     \begin{code}
-    fir ... = foldl1 (+) (zipwith (*) xs hs)
+    map (add 1) xs
     \end{code}
+    \end{minipage}
+    \begin{minipage}{0.07\linewidth}
+      \begin{example}
+      \label{code:partialapplication}
+      \end{example}
+    \end{minipage}
+
+    Here, the expression \hs{(add 1)} is the partial application of the
+    addition function to the value \hs{1}, which is again a function that
+    adds 1 to its (next) argument. 
+    
+    A lambda expression allows a designer to introduce an anonymous function 
+    in any expression. Consider the following expression, which again adds 1 
+    to every element of a vector:
 
-    Here, the \hs{zipwith} function is very similar to the \hs{map}
-    function: It takes a function two lists and then applies the
-    function to each of the elements of the two lists pairwise
-    (\emph{e.g.}, \hs{zipwith (+) [1, 2] [3, 4]} becomes 
-    \hs{[1 + 3, 2 + 4]}.
-
-    The \hs{foldl1} function takes a function and a single list and applies the
-    function to the first two elements of the list. It then applies to
-    function to the result of the first application and the next element
-    from the list. This continues until the end of the list is reached.
-    The result of the \hs{foldl1} function is the result of the last
-    application.
-
-    As you can see, the \hs{zipwith (*)} function is just pairwise
-    multiplication and the \hs{foldl1 (+)} function is just summation.
-
-    To make the correspondence between the code and the equation even
-    more obvious, we turn the list of input samples in the equation
-    around. So, instead of having the the input sample received at time
-    $t$ in $x_t$, $x_0$ now always stores the current sample, and $x_i$
-    stores the $ith$ previous sample. This changes the equation to the
-    following (Note that this is completely equivalent to the original
-    equation, just with a different definition of $x$ that better suits
-    the \hs{x} from the code):
-
-    \begin{equation}
-    y_t  = \sum\nolimits_{i = 0}^{n - 1} {x_i  \cdot h_i } 
-    \end{equation}
-
-    So far, only functions have been used as higher order values. In
-    Haskell, there are two more ways to obtain a function-typed value:
-    partial application and lambda abstraction. Partial application
-    means that a function that takes multiple arguments can be applied
-    to a single argument, and the result will again be a function (but
-    that takes one argument less). As an example, consider the following
-    expression, that adds one to every element of a vector:
-
+    \hspace{-1.7em}
+    \begin{minipage}{0.93\linewidth}
     \begin{code}
-    map ((+) 1) xs
+    map (\x -> x + 1) xs
     \end{code}
-
-    Here, the expression \hs{(+) 1} is the partial application of the
-    plus operator to the value \hs{1}, which is again a function that
-    adds one to its argument.
-
-    A labmda expression allows one to introduce an anonymous function
-    in any expression. Consider the following expression, which again
-    adds one to every element of a list:
-
+    \end{minipage}
+    \begin{minipage}{0.07\linewidth}
+      \begin{example}
+      \label{code:lambdaexpression}
+      \end{example}
+    \end{minipage}
+
+    Finally, not only built-in functions can have higher order arguments (such 
+    as the \hs{map} function), but any function defined in \CLaSH\ may have 
+    functions as arguments. This allows the circuit designer to apply a 
+    large amount of code reuse. The only exception is again the top-level 
+    function: if a function-typed argument is not instantiated with an actual 
+    function, no hardware can be generated.    
+
+    An example of a common circuit where higher-order functions and partial 
+    application lead to a very concise and natural description is a crossbar.
+    The code (\ref{code:crossbar}) for this example can be seen below:
+    
+    \hspace{-1.7em}
+    \begin{minipage}{0.93\linewidth}
     \begin{code}
-    map (\x -> x + 1) xs
+    crossbar inputs selects = map (mux inputs) selects
+      where
+        mux inp x = (inp ! x)
     \end{code}
-
-    Finally, higher order arguments are not limited to just builtin
-    functions, but any function defined in \CLaSH\ can have function
-    arguments. This allows the hardware designer to use a powerful
-    abstraction mechanism in his designs and have an optimal amount of
-    code reuse.
-
-    TODO: Describe ALU example (no code)
+    \end{minipage}
+    \begin{minipage}{0.07\linewidth}
+      \begin{example}
+      \label{code:crossbar}
+      \end{example}
+    \end{minipage}
+    
+    The the \hs{crossbar} function selects those values from \hs{inputs} that
+    are indicated by the indexes in the vector \hs{selects}. The crossbar is 
+    polymorphic in the width of the input (defined by the length of 
+    \hs{inputs}), the width of the output (defined by the length of 
+    \hs{selects}), and the signal type (defined by the element type of 
+    \hs{inputs}). The type-checker can also automatically infer that 
+    \hs{selects} is a vector of \hs{Index} values due to the use of the vector
+    indexing operator (\hs{!}).
 
   \subsection{State}
-    A very important concept in hardware it the concept of state. In a 
-    stateful design, the outputs depend on the history of the inputs, or th
-    state. State is usually stored in registers, which retain their value 
-    during a clock cycle. As we want to describe more than simple 
-    combinatorial designs, \CLaSH\ needs an abstraction mechanism for state.
+    In a stateful design, the outputs depend on the history of the inputs, or 
+    the state. State is usually stored in registers, which retain their valu
+    during a clock cycle. As \CLaSH\ has to be able to describe more than 
+    plain combinational designs, there is a need for an abstraction mechanism 
+    for state.
 
-    An important property in Haskell, and in most other functional languages, 
+    An important property in Haskell, and in many other functional languages, 
     is \emph{purity}. A function is said to be \emph{pure} if it satisfies two
     conditions:
     \begin{inparaenum}
       \item given the same arguments twice, it should return the same value in 
       both cases, and
-      \item when the function is called, it should not have observable 
-      side-effects.
+      \item that the function has no observable side-effects.
     \end{inparaenum}
-    This purity property is important for functional languages, since it 
-    enables all kinds of mathematical reasoning that could not be guaranteed 
-    correct for impure functions. Pure functions are as such a perfect match 
-    for a combinatorial circuit, where the output solely depends on the 
-    inputs. When a circuit has state however, it can no longer be simply
-    described by a pure function. Simply removing the purity property is not a 
-    valid option, as the language would then lose many of it mathematical 
-    properties. In an effort to include the concept of state in pure 
-    functions, the current value of the state is made an argument of the  
-    function; the updated state becomes part of the result.
+    % This purity property is important for functional languages, since it 
+    % enables all kinds of mathematical reasoning that could not be guaranteed 
+    % correct for impure functions. 
+    Pure functions are as such a perfect match for combinational circuits, 
+    where the output solely depends on the inputs. When a circuit has state 
+    however, it can no longer be described by a pure function. 
+    % Simply removing the purity property is not a valid option, as the 
+    % language would then lose many of it mathematical properties. 
+    \CLaSH\ deals with the concept of state by making the current state an 
+    additional argument of the function, and the updated state part of the 
+    result. In this sense the descriptions made in \CLaSH\ are the 
+    combinational parts of a mealy machine.
+    
+    A simple example is adding an accumulator register to the earlier 
+    multiply-accumulate circuit, of which the resulting netlist can be seen in 
+    \Cref{img:mac-state}:
+    
+    \hspace{-1.7em}
+    \begin{minipage}{0.93\linewidth}
+    \begin{code}
+    macS (State c) a b = (State c', c')
+      where
+        c' = mac a b c
+    \end{code}
+    \end{minipage}
+    \begin{minipage}{0.07\linewidth}
+      \begin{example}
+      \label{code:macstate}
+      \end{example}
+    \end{minipage}
+    
+    Note that the \hs{macS} function returns both the new state and the value
+    of the output port. The \hs{State} wrapper indicates which arguments are 
+    part of the current state, and what part of the output is part of the 
+    updated state. This aspect will also be reflected in the type signature of 
+    the function. Abstracting the state of a circuit in this way makes it very 
+    explicit: which variables are part of the state is completely determined 
+    by the type signature. This approach to state is well suited to be used in 
+    combination with the existing code and language features, such as all the 
+    choice elements, as state values are just normal values from Haskell's 
+    point of view. Stateful descriptions are simulated using the recursive 
+    \hs{run} function:
     
-    A simple example is the description of an accumulator circuit:
+    \hspace{-1.7em}
+    \begin{minipage}{0.93\linewidth}
     \begin{code}
-    acc :: Word -> State Word -> (State Word, Word)
-    acc inp (State s) = (State s', outp)
+    run f s (i : inps) = o : (run f s' inps)
       where
-        outp  = s + inp
-        s'    = outp
+        (s', o) = f s i
     \end{code}
-    This approach makes the state of a function very explicit: which variables 
-    are part of the state is completely determined by the type signature. This 
-    approach to state is well suited to be used in combination with the 
-    existing code and language features, such as all the choice constructs, as 
-    state values are just normal values.
-\section{\CLaSH\ prototype}
+    \end{minipage}
+    \begin{minipage}{0.07\linewidth}
+      \begin{example}
+      \label{code:run}
+      \end{example}
+    \end{minipage}
+    
+    The \hs{(:)} operator is the list concatenation operator, where the 
+    left-hand side is the head of a list and the right-hand side is the 
+    remainder of the list. The \hs{run} function applies the function the 
+    developer wants to simulate, \hs{f}, to the current state, \hs{s}, and the 
+    first input value, \hs{i}. The result is the first output value, \hs{o}, 
+    and the updated state \hs{s'}. The next iteration of the \hs{run} function 
+    is then called with the updated state, \hs{s'}, and the rest of the 
+    inputs, \hs{inps}. For the time being, and in the context of this paper, 
+    it is assumed that there is one input per clock cycle. Note that the order 
+    of \hs{s',o,s,i} in the where clause of the \hs{run} functions corresponds 
+    with the order of the input, output and state of the \hs{macS} function 
+    described earlier. Thus, in Haskell the expression \hs{run macS 0 inputs} 
+    simulates \hs{macS} on \hs{inputs} starting with the value \hs{0}
+
+    \begin{figure}
+    \centerline{\includegraphics{mac-state.svg}}
+    \caption{Stateful Multiply-Accumulate}
+    \label{img:mac-state}
+    \vspace{-1.5em}
+    \end{figure}
+    
+    The complete simulation can be compiled to an executable binary by a 
+    Haskell compiler, or executed in an Haskell interpreter. Both 
+    simulation paths require less effort from a circuit designer than first 
+    translating the description to \VHDL\ and then running a \VHDL\ 
+    simulation; it is also very likely that both simulation paths are much 
+    faster.
+    
+\section{The \CLaSH\ compiler}
+An important aspect in this research is the creation of the prototype 
+compiler, which allows us to translate descriptions made in the \CLaSH\ 
+language as described in the previous section to synthesizable \VHDL. 
+% , allowing a designer to actually run a \CLaSH\ design on an \acro{FPGA}.
+
+The Glasgow Haskell Compiler (\GHC)~\cite{ghc} is an open-source Haskell 
+compiler that also provides a high level \acro{API} to most of its internals. 
+The availability of this high-level \acro{API} obviated the need to design 
+many of the tedious parts of the prototype compiler, such as the parser, 
+semantics checker, and especially the type-checker. These parts together form 
+the front-end of the prototype compiler pipeline, as seen in
+\Cref{img:compilerpipeline}.
+
+\begin{figure}
+\vspace{1em}
+\centerline{\includegraphics{compilerpipeline.svg}}
+\caption{\CLaSHtiny\ compiler pipeline}
+\label{img:compilerpipeline}
+\vspace{-1.5em}
+\end{figure}
+
+The output of the \GHC\ front-end consists of the translation of the original 
+Haskell description to \emph{Core}~\cite{Sulzmann2007}, which is a small 
+typed functional language. This \emph{Core} language is relatively easy to 
+process compared to the larger Haskell language. A description in \emph{Core} 
+can still contain elements which have no direct translation to hardware, such 
+as polymorphic types and function-valued arguments. Such a description needs 
+to be transformed to a \emph{normal form}, which only contains elements that 
+have a direct translation. The second stage of the compiler, the 
+\emph{normalization} phase, exhaustively applies a set of 
+\emph{meaning-preserving} transformations on the \emph{Core} description until 
+this description is in a \emph{normal form}. This set of transformations 
+includes transformations typically found in reduction systems and lambda 
+calculus~\cite{lambdacalculus}, such as $\beta$-reduction and 
+$\eta$-expansion. It also includes self-defined transformations that are 
+responsible for the reduction of higher-order functions to `regular' 
+first-order functions, and specializing polymorphic types to concrete types.
+
+The final step in the compiler pipeline is the translation to a \VHDL\ 
+\emph{netlist}, which is a straightforward process due to the resemblance of a 
+normalized description and a set of concurrent signal assignments. The 
+end-product of the \CLaSH\ compiler is called a \VHDL\ \emph{netlist} as the 
+result resembles an actual netlist description, and the fact that it is \VHDL\ 
+is only an implementation detail; e.g., the output could have been Verilog.
+
+\section{Use cases}
+\label{sec:usecases}
+\subsection{FIR Filter}
+As an example of a common hardware design where the relation between 
+functional languages and mathematical functions, combined with the use of 
+higher-order functions leads to a very natural description is a \acro{FIR} 
+filter:
+
+\begin{equation}
+y_t  = \sum\nolimits_{i = 0}^{n - 1} {x_{t - i}  \cdot h_i } 
+\end{equation}
+
+A \acro{FIR} filter multiplies fixed constants ($h$) with the current 
+and a few previous input samples ($x$). Each of these multiplications
+are summed, to produce the result at time $t$. The equation of a \acro{FIR} 
+filter is equivalent to the equation of the dot-product of two vectors, which 
+is shown below:
+
+\begin{equation}
+\mathbf{a}\bullet\mathbf{b} = \sum\nolimits_{i = 0}^{n - 1} {a_i \cdot b_i } 
+\end{equation}
+
+The equation for the dot-product is easily and directly implemented using 
+higher-order functions:
+
+\hspace{-1.7em}
+\begin{minipage}{0.93\linewidth}
+\begin{code}
+as *+* bs = fold (+) (zipWith (*) as bs)
+\end{code}
+\end{minipage}
+\begin{minipage}{0.07\linewidth}
+  \begin{example}
+  \label{code:dotproduct}
+  \end{example}
+\end{minipage}
+
+The \hs{zipWith} function is very similar to the \hs{map} function seen 
+earlier: It takes a function, two vectors, and then applies the function to 
+each of the elements in the two vectors pairwise (\emph{e.g.}, \hs{zipWith (*) 
+[1, 2] [3, 4]} becomes \hs{[1 * 3, 2 * 4]}).
+
+The \hs{fold} function takes a binary function, a single vector, and applies 
+the function to the first two elements of the vector. It then applies the
+function to the result of the first application and the next element in the 
+vector. This continues until the end of the vector is reached. The result of 
+the \hs{fold} function is the result of the last application. It is obvious 
+that the \hs{zipWith (*)} function is pairwise multiplication and that the 
+\hs{fold (+)} function is summation.
+% Returning to the actual \acro{FIR} filter, we will slightly change the 
+% equation describing it, so as to make the translation to code more obvious and 
+% concise. What we do is change the definition of the vector of input samples 
+% and delay the computation by one sample. Instead of having the input sample 
+% received at time $t$ stored in $x_t$, $x_0$ now always stores the newest 
+% sample, and $x_i$ stores the $ith$ previous sample. This changes the equation 
+% to the following (note that this is completely equivalent to the original 
+% equation, just with a different definition of $x$ that will better suit the 
+% transformation to code):
+% 
+% \begin{equation}
+% y_t  = \sum\nolimits_{i = 0}^{n - 1} {x_i  \cdot h_i } 
+% \end{equation}
+The complete definition of the \acro{FIR} filter in \CLaSH\ is:
+
+\hspace{-1.7em}
+\begin{minipage}{0.93\linewidth}
+\begin{code}
+fir (State (xs,hs)) x = 
+  (State (shiftInto x xs,hs), (x +> xs) *+* hs)
+\end{code}
+\end{minipage}
+\begin{minipage}{0.07\linewidth}
+  \begin{example}
+  \label{code:fir}
+  \end{example}
+\end{minipage}
+
+where the vector \hs{xs} contains the previous input samples, the vector 
+\hs{hs} contains the \acro{FIR} coefficients, and \hs{x} is the current input 
+sample. The concatenate operator (\hs{+>}) creates a new vector by placing the 
+current sample (\hs{x}) in front of the previous samples vector (\hs{xs}). The 
+code for the \hs{shiftInto} function, that adds the new input sample (\hs{x}) 
+to the list of previous input samples (\hs{xs}) and removes the oldest sample, 
+is shown below:
+
+\hspace{-1.7em}
+\begin{minipage}{0.93\linewidth}
+\begin{code}
+shiftInto x xs = x +> init xs  
+\end{code}
+\end{minipage}
+\begin{minipage}{0.07\linewidth}
+  \begin{example}
+  \label{code:shiftinto}
+  \end{example}
+\end{minipage}
+
+where the \hs{init} function returns all but the last element of a vector. 
+The resulting netlist of a 4-taps \acro{FIR} filter, created by specializing 
+the vectors of the \acro{FIR} code to a length of 4, is depicted in 
+\Cref{img:4tapfir}.
+
+\begin{figure}
+\centerline{\includegraphics{4tapfir.svg}}
+\caption{4-taps \acrotiny{FIR} Filter}
+\label{img:4tapfir}
+\vspace{-1.5em}
+\end{figure}
+
+\subsection{Higher-order CPU}
+%format fun x = "\textit{fu}_" x
+In this section discusses a somewhat more serious example in which 
+user-defined higher-order function, partial application, lambda expressions, 
+and pattern matching are exploited. The example concerns a \acro{CPU} which 
+consists of four function unites \hs{fun 0,{-"\ldots"-},fun 3} (see 
+\Cref{img:highordcpu}) that each perform some binary operation.
+
+\begin{figure}
+\centerline{\includegraphics{highordcpu.svg}}
+\caption{CPU with higher-order Function Units}
+\label{img:highordcpu}
+\vspace{-1.5em}
+\end{figure}
+
+Every function unit has seven data inputs (of type \hs{Word}), and two address 
+inputs (of type \hs{Index 6}) which indicate which data inputs have to be 
+chosen as arguments for the the binary operation that the unit performs. These 
+data inputs consists of one external input \hs{x}, two fixed initialization 
+values (0 and 1), and the previous outputs of the four function units. The 
+output of the \acro{CPU} as a whole is the previous output of \hs{fun 3}.
+
+The function units \hs{fun 1, fun 2, fun 3} can perform a fixed binary 
+operation, whereas \hs{fun 0} has an additional input for an opcode to choose 
+a binary operation out of a few possibilities.
+
+Each function unit outputs its result into a register, i.e., the state of the 
+\acro{CPU}. This can can e.g. be defined as follows:
+
+\begin{code}
+type CpuState = State [Word | 4]
+\end{code}
+
+Every function unit can now be defined by the following higher-order function 
+\hs{fu}, which takes three arguments: the operation \hs{op} that the function 
+unit performs, the seven \hs{inputs}, and the pair \hs{(a1,a2)} of two 
+addresses:
+
+\hspace{-1.7em}
+\begin{minipage}{0.93\linewidth}
+\begin{code}
+fu op inputs (a1, a2) = regIn
+  where
+    arg1     = inputs!a1
+    arg2     = inputs!a2
+    regIn   = op arg1 arg2
+\end{code}
+\end{minipage}
+\begin{minipage}{0.07\linewidth}
+  \begin{example}
+  \label{code:functionunit}
+  \end{example}
+\end{minipage}
+
+Using partial application we now define:
 
-foo\par bar
+\hspace{-1.7em}
+\begin{minipage}{0.93\linewidth}
+\begin{code}
+fun 1 = fu add
+fun 2 = fu sub
+fun 3 = fu mul
+\end{code}
+\end{minipage}
+\begin{minipage}{0.07\linewidth}
+  \begin{example}
+  \label{code:functionunits1to3}
+  \end{example}
+\end{minipage}
+
+In order to define \hs{fun 0} we first define the type \hs{Opcode} for the 
+opcode and the function \hs{multiop} that chooses a specific operation given 
+the opcode. We assume that the functions \hs{shifts} (which shifts its first 
+operand by the number of bits indicate in the second operand), \hs{xor} (for 
+the bitwise \hs{xor}), and (==) (for equality) already exits.
+
+\hspace{-1.7em}
+\begin{minipage}{0.93\linewidth}
+\begin{code}
+data Opcode = Shift | Xor | Equal
+
+multiop Shift   = shift
+multiop Xor     = xor
+multiop Equal   = \a b -> if a == b then 1 else 0
+\end{code}
+\end{minipage}
+\begin{minipage}{0.07\linewidth}
+  \begin{example}
+  \label{code:multiop}
+  \end{example}
+\end{minipage}
+
+Note that the result of \hs{multiop} is a binary function; this is supported 
+by \CLaSH. We can now define \hs{fun 0} as a function which takes an opcode as 
+additional argument:
+
+\hspace{-1.7em}
+\begin{minipage}{0.93\linewidth}
+\begin{code}
+fun 0 c = fu (multiop c)
+\end{code}
+\end{minipage}
+\begin{minipage}{0.07\linewidth}
+  \begin{example}
+  \label{code:functionunit0}
+  \end{example}
+\end{minipage}
+
+Now we come to the definition \hs{cpu} of the full \acro{CPU}. Its type is:
+
+\begin{code}
+cpu :: CpuState 
+  -> (Word, Opcode, [(Index 6, Index 6) | 4])
+  -> (CpuState, Word)
+\end{code}
+
+Note that this type fits the requirements of the function \hs{run}. The 
+definition of the \hs{cpu} now is:
+
+\hspace{-1.7em}
+\begin{minipage}{0.93\linewidth}
+\begin{code}
+cpu (State s) (x,opc,addrs) = (State s', out)
+  where
+    inputs    =   x +> (0 +> (1 +> s))
+    s'        =   [{-"\;"-}fun 0 opc   inputs (addrs!0)
+                  ,{-"\;"-}fun 1       inputs (addrs!1)
+                  ,{-"\;"-}fun 2       inputs (addrs!2)
+                  ,{-"\;"-}fun 3       inputs (addrs!3)
+                  ]
+    out       =   last s
+\end{code}
+\end{minipage}
+\begin{minipage}{0.07\linewidth}
+  \begin{example}
+  \label{code:cpu}
+  \end{example}
+\end{minipage}
+
+While this is still a simple (and maybe not very useful) design, it 
+illustrates some possibilities that \CLaSH\ offers and suggests how to write 
+actual designs.
+
+% Each of the function units has both its operands connected to all data
+% sources, and can be programmed to select any data source for either
+% operand. In addition, the leftmost function unit has an additional
+% opcode input to select the operation it performs. The previous output of the 
+% rightmost function unit is the output of the entire \acro{CPU}.
+% 
+% The code of the function unit (\ref{code:functionunit}), which arranges the 
+% operand selection for the function unit, is shown below. Note that the actual 
+% operation that takes place inside the function unit is supplied as the 
+% (higher-order) argument \hs{op}, which is a function that takes two arguments.
+% 
+% 
+% 
+% The \hs{multiop} function (\ref{code:multiop}) defines the operation that takes place in the leftmost function unit. It is essentially a simple three operation \acro{ALU} that makes good use of pattern matching and guards in its description. The \hs{shift} function used here shifts its first operand by the number of bits indicated in the second operand, the \hs{xor} function produces
+% the bitwise xor of its operands.
+% 
+% 
+% The \acro{CPU} function (\ref{code:cpu}) ties everything together. It applies 
+% the function unit (\hs{fu}) to several operations, to create a different 
+% function unit each time. The first application is interesting, as it does not 
+% just pass a function to \hs{fu}, but a partial application of \hs{multiop}. 
+% This demonstrates how one function unit can effectively get extra inputs 
+% compared to the others.
+% 
+% The vector \hs{inputs} is the set of data sources, which is passed to
+% each function unit as a set of possible operants. The \acro{CPU} also receives 
+% a vector of address pairs, which are used by each function unit to select 
+% their operand. 
+% The application of the function units to the \hs{inputs} and
+% \hs{addrs} arguments seems quite repetitive and could be rewritten to use
+% a combination of the \hs{map} and \hs{zipwith} functions instead.
+% However, the prototype compiler does not currently support working with 
+% lists of functions, so a more explicit version of the code is given instead.
+
+% While this is still a simple example, it could form the basis of an actual 
+% design, in which the same techniques can be reused.
 
 \section{Related work}
-Many functional hardware description languages have been developed over the 
-years. Early work includes such languages as $\mu$\acro{FP}~\cite{muFP}, an 
-extension of Backus' \acro{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. \acro{HML}~\cite{HML2} is a 
-hardware modeling language based on the strict functional language 
-\acro{ML}, and has support for polymorphic types and higher-order functions. 
-Published work suggests that there is no direct simulation support for 
-\acro{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 pattern 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.
+This section describes the features of existing (functional) hardware 
+description languages and highlights the advantages that this research has 
+over existing work.
+
+% Many functional hardware description languages have been developed over the 
+% years. Early work includes such languages as $\mu$\acro{FP}~\cite{muFP}, an 
+% extension of Backus' \acro{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. 
+
+\acro{HML}~\cite{HML2} is a hardware modeling language based on the strict 
+functional language \acro{ML}, and has support for polymorphic types and 
+higher-order functions. There is no direct simulation support for \acro{HML}, 
+so a description in \acro{HML} has to be translated to \VHDL\ and the 
+translated description can then be simulated in a \VHDL\ simulator. Certain 
+aspects of HML, such as higher-order functions are however not supported by 
+the \VHDL\ translator~\cite{HML3}. The \CLaSH\ compiler on the other hand can 
+correctly translate all of its language constructs.
+
+Like the research presented in this paper, many functional hardware 
+description languages have some sort of foundation in the functional 
+programming language Haskell. Hawk~\cite{Hawk1} is a hardware modeling 
+language embedded in Haskell and has sequential environments that make it 
+easier to specify stateful computation (by using the \acro{ST} monad). Hawk 
+specifications can be simulated; to the best knowledge of the authors there is 
+however no support for automated circuit synthesis. 
+
+The ForSyDe~\cite{ForSyDe2} system uses Haskell to specify abstract system 
+models. A designer can model systems using heterogeneous models of 
+computation, which include continuous time, synchronous and untimed models of 
+computation. Using so-called domain interfaces a designer can simulate 
+electronic systems which have both analog and digital parts. ForSyDe has 
+several backends including simulation and automated synthesis, though 
+automated synthesis is restricted to the synchronous model of computation. 
+Though ForSyDe offers higher-order functions and polymorphism, ForSyDe's 
+choice elements are limited to \hs{if} and \hs{case} expressions. ForSyDe's 
+explicit conversions, where functions have to be wrapped in processes and 
+processes have to be wrapped in systems, combined with the explicit 
+instantiations of components, also makes ForSyDe far more verbose than \CLaSH.
+
+Lava~\cite{Lava,kansaslava} is a hardware description language embedded in 
+Haskell which focuses on the structural representation of hardware. Like 
+\CLaSH, Lava has support for polymorphic types and higher-order functions. 
+Besides support for simulation and circuit synthesis, Lava descriptions can be 
+interfaced with formal method tools for formal verification. As discussed in 
+the introduction, taking the embedded language approach does not allow for 
+Haskell's choice elements to be captured within the circuit descriptions. In 
+this respect \CLaSH\ differs from Lava, in that all of Haskell's choice 
+elements, such as \hs{case}-expressions and pattern matching, are synthesized 
+to choice elements in the eventual circuit. Consequently, descriptions 
+containing rich control structures can be specified in a more user-friendly 
+way in \CLaSH\ than possible within Lava, and hence are less error-prone.
+
+Bluespec~\cite{Bluespec} is a high-level synthesis language that features 
+guarded atomic transactions and allows for the automated derivation of control 
+structures based on these atomic transactions. Bluespec, like \CLaSH, supports 
+polymorphic typing and function-valued arguments. Bluespec's syntax and 
+language features \emph{had} their basis in Haskell. However, in order to 
+appeal to the users of the traditional \acrop{HDL}, Bluespec has adapted 
+imperative features and a syntax that resembles Verilog. As a result, Bluespec 
+is (unnecessarily) verbose when compared to \CLaSH.
+
+The merits of polymorphic typing and function-valued arguments are now also 
+recognized in the traditional \acrop{HDL}, exemplified by the new \VHDL-2008 
+standard~\cite{VHDL2008}. \VHDL-2008 support for generics has been extended to 
+types and subprograms, allowing a designer to describe components with 
+polymorphic ports and function-valued arguments. Note that the types and 
+subprograms still require an explicit generic map, while the \CLaSH\ compiler 
+automatically infers types, and automatically propagates function-valued 
+arguments. There are also no (generally available) \VHDL\ synthesis tools that 
+currently support the \VHDL-2008 standard.
 
 % Wired~\cite{Wired},, T-Ruby~\cite{T-Ruby}, Hydra~\cite{Hydra}. 
 % 
@@ -1131,29 +1765,62 @@ generic map, whereas type-inference and type-specialization are implicit in
 
 
 \section{Conclusion}
-The conclusion goes here.
-
-
-
+This research demonstrates once more that functional languages are well suited 
+for hardware descriptions: function applications provide an elegant notation 
+for component instantiation. While circuit descriptions made in \CLaSH\ are 
+very concise when compared to other (traditional) \acrop{HDL}, their intended 
+functionality remains clear. \CLaSH\ goes beyond the existing (functional) 
+hardware descriptions languages by including advanced choice elements, such as 
+pattern matching and guards, which are well suited to describe the conditional 
+assignments in control-oriented circuits. Besides being able to translate 
+these basic constructs to synthesizable \VHDL, the prototype compiler can also 
+correctly translate descriptions that contain both polymorphic types and 
+user-defined higher-order functions.
+
+% Where recent functional hardware description languages have mostly opted to 
+% embed themselves in an existing functional language, this research features 
+% a `true' compiler. As a result there is a clear distinction between 
+% compile-time and run-time, which allows a myriad of choice constructs to be 
+% part of the actual circuit description; a feature the embedded hardware 
+% description languages do not offer.
+
+Besides simple circuits such as variants of both the \acro{FIR} filter and 
+the higher-order \acro{CPU} shown in \Cref{sec:usecases}, the \CLaSH\ compiler 
+has also been able to translate non-trivial functional descriptions such as a 
+streaming reduction circuit~\cite{reductioncircuit} for floating point 
+numbers.
+
+\section{Future Work}
+The choice of describing state explicitly as and extra argument and result can 
+be seen as a mixed blessing. Even though descriptions that use state are 
+usually very clear, distributing and collecting substate can become tedious 
+and even error-prone. Automating the required distribution and collection, or 
+finding a more suitable abstraction mechanism for state would make \CLaSH\ 
+easier to use. Currently, one of the examined approaches to suppress state in 
+the specification is by using Haskell's arrow-abstraction.
+
+The transformations in the normalization phase of the prototype compiler are 
+developed in an ad-hoc manner, which makes the existence of many desirable 
+properties unclear. Such properties include whether the complete set of 
+transformations will always lead to a normal form or whether the normalization 
+process always terminates. Though extensive use of the compiler suggests that 
+these properties usually hold, they have not been formally proven. A 
+systematic approach to defining the set of transformations allows one to proof 
+that the earlier mentioned properties do indeed hold.
 
 % conference papers do not normally have an appendix
 
 
 % use section* for acknowledgement
-\section*{Acknowledgment}
-
-
-The authors would like to thank...
-
-
-
-
+% \section*{Acknowledgment}
+% 
+% The authors would like to thank...
 
 % trigger a \newpage just before the given reference
 % number - used to balance the columns on the last page
 % adjust value as needed - may need to be readjusted if
 % the document is modified later
-%\IEEEtriggeratref{8}
+% \IEEEtriggeratref{14}
 % The "triggered" command can be changed if desired:
 %\IEEEtriggercmd{\enlargethispage{-5in}}
 
@@ -1166,7 +1833,7 @@ The authors would like to thank...
 % http://www.michaelshell.org/tex/ieeetran/bibtex/
 \bibliographystyle{IEEEtran}
 % argument is your BibTeX string definitions and bibliography database(s)
-\bibliography{IEEEabrv,clash.bib}
+\bibliography{clash}
 %
 % <OR> manually copy in the resultant .bbl file
 % set second argument of \begin to the number of references