Add part about the run-function to the section about state
[matthijs/master-project/dsd-paper.git] / cλash.lhs
index ca4f1cdc8ece28c34c6c457ee71477814747fc12..2adeed6e903eaf48d805917ad38a44e8f94de739 100644 (file)
@@ -63,6 +63,7 @@
 % should be used if it is desired that the figures are to be displayed in
 % draft mode.
 %
+
 \documentclass[conference,pdf,a4paper,10pt,final,twoside,twocolumn]{IEEEtran}
 % Add the compsoc option for Computer Society conferences.
 %
@@ -93,9 +94,6 @@
 
 
 
-
-
-
 % *** CITATION PACKAGES ***
 %
 \usepackage{cite}
 % *** GRAPHICS RELATED PACKAGES ***
 %
 \ifCLASSINFOpdf
-  \usepackage[pdftex]{graphicx}
+  \usepackage[pdftex]{graphicx}
   % declare the path(s) where your graphic files are
   % \graphicspath{{../pdf/}{../jpeg/}}
   % and their extensions so you won't have to specify these with
 
 % Macro for certain acronyms in small caps. Doesn't work with the
 % default font, though (it contains no smallcaps it seems).
-\def\VHDL{{\small{VHDL}}}
-\def\GHC{{\small{GHC}}}
-\def\CLaSH{\textsc{C$\lambda$aSH}}
+\def\acro#1{{\small{#1}}}
+\def\VHDL{\acro{VHDL}}
+\def\GHC{\acro{GHC}}
+\def\CLaSH{{\small{C}}$\lambda$a{\small{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{\parsep}{0.5ex plus 0.2ex minus 0.1ex}
+    \setlength{\listparindent}{\parindent}
     \setlength{\itemsep}{0 ex plus 0.2ex}
     \renewcommand{\makelabel}[1]{##1:\hfil}
     }
   }
 {\end{list}}
 
+\usepackage{paralist}
+\usepackage{xcolor}
+\def\comment#1{{\color[rgb]{1.0,0.0,0.0}{#1}}}
+
+\usepackage{cleveref}
+\crefname{figure}{figure}{figures}
+\newcommand{\fref}[1]{\cref{#1}} 
+\newcommand{\Fref}[1]{\Cref{#1}}
+
+
 %include polycode.fmt
+%include clash.fmt
 
 \begin{document}
 %
 % paper title
 % can use linebreaks \\ within to get better formatting as desired
-\title{\CLaSH: Structural Descriptions \\ of Synchronous Hardware using Haskell}
+\title{C$\lambda$aSH: Structural Descriptions \\ of Synchronous Hardware using Haskell}
 
 
 % author names and 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\\
 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}}
 % \and
 % \IEEEauthorblockN{Homer Simpson}
 % \IEEEauthorblockA{Twentieth Century Fox\\
@@ -459,324 +470,630 @@ The abstract goes here.
 \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\ 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.
+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 combinatorial circuits can be directly 
+modeled as 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 languages. As the hardware descriptions are plain Haskell 
+functions, these descriptions can be compiled for simulation using an 
+optimizing Haskell compiler such as the Glasgow 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. A developer describes the behavior of the hardware between 
+clock cycles, as such, only synchronous systems can be described. Many 
+functional hardware description model 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.
+
 \section{Hardware description in Haskell}
 
   \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 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 itself.
+    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 output port can have a complex type (such as a tuple), so having just 
+    a single output port does not pose any limitation. The arguments of a 
+    function applications are assigned to a signal, 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 of function calls is reflected in the final \VHDL\
-    output as well, creating a hierarchical \VHDL\ description of the
-    hardware.  This separation in different components makes the
-    resulting \VHDL\ output easier to read and debug.
-
-    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 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
+    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$:
+    
+    \begin{code}
+    mac a b c = add (mul a b) c
+    \end{code}
+    
+    \begin{figure}
+    \centerline{\includegraphics{mac}}
+    \caption{Combinatorial Multiply-Accumulate}
+    \label{img:mac-comb}
+    \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:
+    
+    \begin{code}
+    mac (a, b, c) = add (mul a b) c
+    \end{code}
+    
+    \begin{figure}
+    \centerline{\includegraphics{mac-nocurry}}
+    \caption{Combinatorial Multiply-Accumulate (complex input)}
+    \label{img:mac-comb-nocurry}
+    \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 (\hs{if} expressions can be very directly translated to 
+    \hs{case} expressions). A \hs{case} construct is translated to a 
+    multiplexer, where the control value is linked to the selection port and 
+    the  output of each case is linked to the corresponding input port on 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. 
+    We can see two versions of a contrived example below, 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. Both versions of the example roughly correspond to the same 
+    netlist, which is depicted in \Cref{img:choice}.
+    
+    \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
+    \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
+    \end{code}
+
+    \begin{figure}
+    \centerline{\includegraphics{choice-case}}
+    \caption{Choice - sumif}
+    \label{img:choice}
+    \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. Like 
+    \hs{if-then-else} constructs, pattern matching and guards have a 
+    (straightforward) translation to \hs{case} constructs and can as such be 
+    mapped to multiplexers. A third version of the earlier example, using both 
+    pattern matching and guards, can be seen below. The version using pattern 
+    matching and guards also has roughly the same netlist representation 
+    (\Cref{img:choice}) as the earlier two versions of the example.
+    
+    \begin{code}
+    sumif Eq a b    | a == b = a + b
+    sumif Neq a b   | a != b = a + b
+    sumif _ _ _     = 0
+    \end{code}
+
+    % \begin{figure}
+    % \centerline{\includegraphics{choice-ifthenelse}}
+    % \caption{Choice - \emph{if-then-else}}
+    % \label{img:choice}
+    % \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 values used to its hardware
-    equivalents. In particular, this means a hardware equivalent for
-    every \emph{type} used in a hardware description is needed
-
-    Since most functional languages have a lot of standard types that
-    are hard to translate (integers without a fixed size, lists without
-    a static length, etc.), a number of \quote{built-in} types will be
-    defined first. These types are built-in in the sense that our
-    compiler will have a fixed \VHDL\ type for these. User defined types,
-    on the other hand, will have their hardware type derived directly
-    from their Haskell declaration automatically, according to the rules
-    sketched here.
-
-  \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 \CLaSH\ package, so they are user-defined types
-    from Haskell's point of view).
-
+    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, as such this 
+    section will only deal 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 direct translation is defined within the \CLaSH\ 
+    compiler; the term user-defined types should not require any further 
+    elaboration. The translatable types are also inferable by the compiler, 
+    meaning that a developer does not have to annotate every function with a 
+    type signature.
+  
+    % 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 direct translation defined within the \CLaSH\
+    compiler:
     \begin{xlist}
-      \item[\hs{Bit}]
-        This is the most basic type available. It is mapped directly onto
-        the \texttt{std\_logic} \VHDL\ type. Mapping this to the
-        \texttt{bit} type might make more sense (since the Haskell version
-        only has two values), but using \texttt{std\_logic} is more standard
-        (and allowed for some experimentation with don't care values)
-
-      \item[\hs{Bool}]
-        This is the only built-in Haskell type supported and is translated
-        exactly like the 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.
-
-        A \hs{Bool} is translated to a \texttt{std\_logic}, just like \hs{Bit}.
-      \item[\hs{SizedWord}, \hs{SizedInt}]
+      \item[\bf{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[\bf{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 required in order to support the
+        \hs{if-then-else} construct, which requires a \hs{Bool} value for 
+        the condition.
+      \item[\bf{SizedWord}, \bf{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
-        ollows:
-
-\begin{verbatim}
-  type Word32 = SizedWord D32
-\end{verbatim}
-
-        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. It has two type parameters: its
-        length and the type of the elements contained in it. By putting the
-        length parameter in the type, the length of a vector can be determined
-        at compile time, instead of only at run-time for conventional lists.
-
-        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:
-
-\begin{verbatim}
-type RegisterState = Vector D8 Word32
-\end{verbatim}
-
-        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}]
+        while a \hs{SizedInt} is signed. Both are parametrizable in their 
+        size. 
+        % , 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 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 short-hand notation used for the vector type in  
+        the rest of paper is: \hs{[a|n]}. Where the \hs{a} is the element 
+        type, and \hs{n} is the length of the vector.
+        % 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}]
         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. There is a lot of added implementation complexity
-        when adding a lower bound and having just an upper bound was enough
-        for the primary purpose of this type: type-safely indexing vectors.
-
-        To define an index for the 8 element vector above, we would do:
-
-\begin{verbatim}
-type RegisterIndex = RangedWord D7
-\end{verbatim}
-
-        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.
+        An \hs{Index} only has an upper bound, its lower bound is
+        implicitly zero. The main purpose of the \hs{Index} 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:
+
+        % \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}
-  \subsection{User-defined types}
+
+  \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 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 will be left outside the scope of this research.
+    keyword and datatype renaming constructs 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. 
+    As it is currently unclear how these advanced type constructs correspond 
+    with hardware, they are for now unsupported by the \CLaSH\ compiler
 
     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: 
+    completely new type. Type synonyms and renaming constructs only define new 
+    names for existing types, where synonyms are completely interchangeable 
+    and renaming constructs need explicit conversions. Therefore, these do not 
+    need any particular translation, a synonym or renamed type will just use 
+    the same representation as the original type. For algebraic types, we can 
+    make the following distinctions: 
 
     \begin{xlist}
-      \item[Product types]
-        A product type is an algebraic datatype with a single constructor with
-        two or more fields, denoted in practice like (a,b), (a,b,c), etc. This
-        is essentially a way to pack a few values together in a record-like
-        structure. In fact, the built-in tuple types are just algebraic product
-        types (and are thus supported in exactly the same way).
-
-        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
-        constructor algebraic data-types, including those with just one
-        field (which are technically not a product, but generate a VHDL
-        record for implementation simplicity).
-      \item[Enumerated types]
-        An enumerated type is an algebraic datatype with multiple constructors, but
-        none of them have fields. This is 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.
-      \item[Sum types]
-        A sum type is an algebraic datatype with multiple constructors, where
-        the constructors have one or more fields. Technically, a type with
-        more than one field per constructor is a sum of products type, but
-        for our purposes this distinction does not really make a
-        difference, so this distinction is note made.
-
-        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.
-
-        Sum types are currently not supported by the prototype, since there is
-        no obvious \VHDL\ alternative. They can easily be emulated, however, as
-        we will see from an example:
-
-\begin{verbatim}
-data Sum = A Bit Word | B Word
-\end{verbatim}
-
-        An obvious way to translate this would be to create an enumeration to
-        distinguish the constructors and then create a big record that
-        contains all the fields of all the constructors. This is the same
-        translation that would result from the following enumeration and
-        product type (using a tuple for clarity):
-
-\begin{verbatim}
-data SumC = A | B
-type Sum = (SumC, Bit, Word, Word)
-\end{verbatim}
-
-        Here, the \hs{SumC} type effectively signals which of the latter three
-        fields of the \hs{Sum} type are valid (the first two if \hs{A}, the
-        last one if \hs{B}), all the other ones have no useful value.
-
-        An obvious problem with this naive approach is the space usage: the
-        example above generates a fairly big \VHDL\ type. Since we can be
-        sure that the two \hs{Word}s in the \hs{Sum} type will never be valid
-        at the same time, this is a waste of space.
-
-        Obviously, duplication detection could be used to reuse a
-        particular field for another constructor, but this would only
-        partially solve the problem. If two fields would be, for
-        example, an array of 8 bits and an 8 bit unsigned word, these are
-        different types and could not be shared. However, in the final
-        hardware, both of these types would simply be 8 bit connections,
-        so we have a 100\% size increase by not sharing these.
-      \end{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. Haskell's built-in tuple types are also defined 
+        as single constructor algebraic types  An example of a single 
+        constructor type is the following pair of integers:
+        \begin{code}
+        data IntPair = IntPair Int Int
+        \end{code}
+        % 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. An example of such an enum type is the type that represents the
+        colors in a traffic light:
+        \begin{code}
+        data TrafficLight = Red | Orange | Green
+        \end{code}
+        % 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.
+    \end{xlist}
 
+  \subsection{Polymorphism}
+    A powerful construct in most functional languages is polymorphism, it 
+    allows a function to handle values of different data types in a uniform 
+    way. Haskell supports \emph{parametric polymorphism}~\cite{polymorphism}, 
+    meaning functions can be written without mention of any specific type and 
+    can be used transparently with any number of new types.
+
+    As an example of a parametric polymorphic function, consider the type of 
+    the following \hs{append} function, which appends an element to a vector:
+    \begin{code}
+    append :: [a|n] -> a -> [a|n + 1]
+    \end{code}
+
+    This type is parameterized by \hs{a}, which can contain any type at
+    all. This means that \hs{append} can append an element to a vector,
+    regardless of the type of the elements in the list (as long as the type of 
+    the value to be added is of the same type as the values in the vector). 
+    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.
+
+    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 
+    type classes, where a class definition provides the general interface of a 
+    function, and class 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 developer can make use 
+    of this ad-hoc polymorphism by adding a 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. 
+    
+    As an example we will take a look at type signature of the function 
+    \hs{sum}, 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  
+    we know that the addition (+) operator is defined for that type. 
+    \CLaSH's built-in numerical types are also instances of the \hs{Num}
+    class, so we can use the addition operator on \hs{SizedWords} as
+    well as on \hs{SizedInts}.
+
+    In \CLaSH, parametric 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 (as 
+    they are 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 built-in type classes for its built-in function, such as: \hs{Num} 
+    for numerical operations, \hs{Eq} for the equality operators, and
+    \hs{Ord} for the comparison/order operators.
+
+  \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. The following example should clarify this concept:
+    
+    \begin{code}
+    negVector xs = map not xs
+    \end{code}
+
+    The code above defines a function \hs{negVector}, which takes a vector of
+    booleans, and returns a vector where all the values are negated. It 
+    achieves this by calling the \hs{map} function, and passing it 
+    \emph{another 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 vector elements, other than that it must be the same type as 
+    the input type 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 readily be inferred from the type 
+    signature belonging to \hs{map}:
+
+    \begin{code}
+    map :: (a -> b) -> [a|n] -> [b|n]
+    \end{code}
+    
+    As an example of a common hardware design where the use of higher-order
+    functions leads to a very natural description is a FIR filter, which is 
+    basically the dot-product of two vectors:
+
+    \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$. The equation of a FIR 
+    filter is indeed equivalent to the equation of the dot-product, which is 
+    shown below:
+    
+    \begin{equation}
+    \mathbf{x}\bullet\mathbf{y} = \sum\nolimits_{i = 0}^{n - 1} {x_i \cdot y_i } 
+    \end{equation}
+
+    We can easily and directly implement the equation for the dot-product
+    using higher-order functions:
+
+    \begin{code}
+    xs *+* ys = foldl1 (+) (zipWith (*) xs hs)
+    \end{code}
+
+    The \hs{zipWith} function is very similar to the \hs{map} function: 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]} $\equiv$ \hs{[3,8]}).
+
+    The \hs{foldl1} function takes a 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 from 
+    the vector. This continues until the end of the vector 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.
+
+    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:
+
+    \begin{code}
+    map ((+) 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 lambda expression allows one to introduce an 
+    anonymous function in any expression. Consider the following expression, 
+    which again adds one to every element of a vector:
+
+    \begin{code}
+    map (\x -> x + 1) xs
+    \end{code}
+
+    Finally, higher order arguments are not limited to just built-in
+    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.
+
+    \comment{TODO: Describe ALU example (no code)}
+
+  \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 the 
+    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.
+
+    An important property in Haskell, and in most 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.
+    \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 or 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. In this sense the
+    descriptions made in \CLaSH are the describing the combinatorial 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}:
+    
+    \begin{code}
+    macS (State c) a b = (State c', outp)
+      where
+        outp  = mac a b c
+        c'    = outp
+    \end{code}
+    
+    \begin{figure}
+    \centerline{\includegraphics{mac-state}}
+    \caption{Stateful Multiply-Accumulate}
+    \label{img:mac-state}
+    \end{figure}
+    
+    The \hs{State} keyword 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 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 constructs, as state values are just normal values.
+    
+    We can simulate stateful descriptions using the recursive \hs{run} 
+    function:
+    
+    \begin{code}
+    run f s (i:inps) = o : (run f s' inps)
+      where
+        (s', o) = f s i
+    \end{code}
+    
+    The \hs{run} function maps a list of inputs over the function that a 
+    developer wants to simulate, passing the state to each new iteration. Each
+    value in the input list corresponds to exactly one cycle of the (implicit) 
+    clock. The result of the simulation is a list of outputs for every clock
+    cycle. As both the \hs{run} function and the hardware description are 
+    plain hardware, the complete simulation can be compiled by an optimizing
+    Haskell compiler.
+    
 \section{\CLaSH\ prototype}
 
 foo\par bar
 
+\section{Use cases}
+Returning to the example of the FIR filter, we will slightly change the
+equation belong to it, so as to make the translation to code more obvious.
+What we will do is change the definition of the vector of input samples.
+So, instead of having the input sample received at time
+$t$ stored 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 will better suit
+the the transformation to code):
+
+\begin{equation}
+y_t  = \sum\nolimits_{i = 0}^{n - 1} {x_i  \cdot h_i } 
+\end{equation}
+
+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. The function that does this shifting of the input samples 
+is shown below:
+
+\begin{code}
+x >> xs = x +> tail xs  
+\end{code}
+
+Where the \hs{tail} function returns all but the first element of a 
+vector, and the concatenate operator ($\succ$) adds a new element to the 
+left of a vector. The complete definition of the FIR filter then becomes:
+
+\begin{code}
+fir (State (xs,hs)) x = (State (x >> xs,hs), xs *+* hs)
+\end{code}
+
+The resulting netlist of a 4-taps FIR filter based on the above definition
+is depicted in \Cref{img:4tapfir}.
+
+\begin{figure}
+\centerline{\includegraphics{4tapfir}}
+\caption{4-taps FIR Filter}
+\label{img:4tapfir}
+\end{figure}
+
 \section{Related work}
 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 
+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. \textsc{hml}~\cite{HML2} is a 
+circuits, and has a particular focus on layout. \acro{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. 
+\acro{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.
+\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. 
@@ -798,24 +1115,24 @@ 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 
+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 \VHDL2008 standard~\cite{VHDL2008}. \VHDL-2008 has 
+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
+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 \acro{FL}~\cite{FL} to la
 
 % An example of a floating figure using the graphicx package.
 % Note that \label must occur AFTER (or within) \caption.