Beautify list environments
[matthijs/master-project/dsd-paper.git] / cλash.lhs
index e824b76d59fc75493b62a462621dd4d031479327..25ec7a281aed0e120a9d7c3d6feb90a62a4b6cb7 100644 (file)
 
 % 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.
     \setlength{\leftmargin}{\labelwidth}
     \addtolength{\leftmargin}{\labelsep}
     \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}}}
+
 %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}}
 % \and
 % \IEEEauthorblockN{Homer Simpson}
 % \IEEEauthorblockA{Twentieth Century Fox\\
@@ -469,12 +475,41 @@ 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.
+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.
+
+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}. What this 
+means is that a developer is given a library of Haskell functions and types 
+that together form the language primitives of the domain specific language. 
+Using these functions, the designer does not only describes a circuit, but 
+actually builds a large domain-specific datatype 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 to be used as hardware description language. By taking this approach, 
+we can capture certain language constructs, such as Haskell's choice elements 
+(if-statement, case-statment, etc.), which are not available in the functional 
+hardware description languages that are embedded in Haskell. 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.
+
+Like the standard hardware description languages, descriptions made in a 
+functional hardware description languages must eventually be converted into a 
+netlist. This research also features an a prototype translater 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 optimizing \VHDL\ synthesis tools.
 
-What gives functional languages as hardware description languages their merits 
-is the fact that basic combinatorial circuits are equivalent to mathematical 
-function, and that functional languages lend themselves very well to describe 
-and compose these mathematical functions.
 \section{Hardware description in Haskell}
 
   \subsection{Function application}
@@ -501,13 +536,13 @@ and compose these mathematical functions.
     Example that defines the \texttt{mac} function by applying the
     \texttt{add} and \texttt{mul} functions to calculate $a * b + c$:
 
-\begin{verbatim}
+\begin{code}
 mac a b c = add (mul a b) c
-\end{verbatim}
+\end{code}
 
-    TODO: Pretty picture
+\comment{TODO: Pretty picture}
 
-  \subsection{Choices }
+  \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
@@ -537,30 +572,26 @@ mac a b c = add (mul a b) c
     expression, one using only case expressions and one using pattern
     matching and guards.
 
-\begin{verbatim}
-sumif cmp a b = if cmp == Eq && a == b 
-                || cmp == Neq && a != b
-                then a + b
-                else 0
-\end{verbatim}
-
-\begin{verbatim}
-sumif cmp a b = case cmp 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
+    \begin{code}
+    sumif pred a b =  if  pred == Eq && a == b ||
+                          pred == Neq && a != b
+                      then  a + b
+                      else  0
+
+    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
+
+    sumif Eq a b    | a == b = a + b
+    sumif Neq a b   | a != b = a + b
+    sumif _ _ _     = 0
+    \end{code}
+
+  \comment{TODO: Pretty picture}
 
   \subsection{Types}
     Translation of two most basic functional concepts has been
@@ -598,61 +629,54 @@ sumif _ _ _ = 0
         length type, so you can define an unsigned word of 32 bits wide as
         follows:
 
-\begin{verbatim}
-type Word32 = SizedWord D32
-\end{verbatim}
+        \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.
+        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.
+        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:
 
-        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}
+        \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.
+        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}.
-
-        TODO: Perhaps remove this example?
+        implicitly zero. The main purpose of the \hs{RangedWord} type is to be 
+        used as an index to a \hs{Vector}.
 
-        To define an index for the 8 element vector above, we would do:
+        \comment{TODO: Perhaps remove this example?} To define an index for 
+        the 8 element vector above, we would do:
 
-\begin{verbatim}
-type RegisterIndex = RangedWord D7
-\end{verbatim}
+        \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.
+        8 element vector \hs{RegisterState} above. This type is translated to 
+        the \texttt{unsigned} \VHDL type.
     \end{xlist}
 
   \subsection{User-defined types}
@@ -679,53 +703,86 @@ type RegisterIndex = RangedWord D7
       \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:
+        record-like structure. An example of such a type is the following pair 
+        of integers:
 
-\begin{verbatim}
+\begin{code}
 data IntPair = IntPair Int Int
-\end{verbatim}
+\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.
+        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.
+        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[\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}
-
+    \end{xlist}
 
+  \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 
+    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.
+    
+    A simple example is the description of an accumulator circuit:
+    \begin{code}
+    acc :: Word -> State Word -> (State Word, Word)
+    acc inp (State s) = (State s', outp)
+      where
+        outp  = s + inp
+        s'    = outp
+    \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}
 
 foo\par bar
 
 \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. 
@@ -747,24 +804,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 \VHDL\ 2008 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.