Update VHDL command to use \small instead of \textsc
[matthijs/master-project/dsd-paper.git] / cλash.tex
index 9d4fb22e8c05715952ca6d5c04d65761b0e3d194..4a917f96233664a41daddcd0807b60db0783e31e 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{\textsc{vhdl}}
-\def\GHC{\textsc{ghc}}
+\def\VHDL{{\small{VHDL}}}
+\def\GHC{{\small{GHC}}}
 \def\CLaSH{\textsc{C$\lambda$aSH}}
 
 % Macro for pretty printing haskell snippets. Just monospaced for now, perhaps
@@ -441,9 +441,24 @@ 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 has allowed the productivity of hardware 
+engineers to keep pace with the development of chip technology. Standard 
+Hardware description languages, like \VHDL\ and Verilog, allowed an engineer 
+to describe circuits using a programming language. These standard languages 
+are very good at describing detailed hardware properties such as timing 
+behavior, but are generally cumbersome in expressing higher-level 
+abstractions. These languages also tend to have a complex syntax and a lack of 
+formal semantics. To overcome these complexities, and raise the abstraction 
+level, a great number of approaches based on functional languages has been 
+proposed \cite{T-Ruby,Hydra,HML2,Hawk1,Lava,ForSyDe1,Wired,reFLect}. The idea 
+of using functional languages started in the early 1980s \cite{Cardelli1981,
+muFP,DAISY,FHDL}, a time which also saw the birth of the currently popular 
+hardware description languages such as \VHDL.
+
+What gives functional languages as hardware description languages their merits 
+is the fact that basic combinatorial circuits are equivalent to mathematical 
+function, and that functional languages lend themselves very well to describe 
+and compose these mathematical functions.
 \section{Hardware description in Haskell}
 
   \subsection{Function application}
@@ -545,7 +560,7 @@ sumif _ _ _ = 0
     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,
+    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.
@@ -587,7 +602,7 @@ sumif _ _ _ = 0
         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 \small{VHDL} \texttt{unsigned} and
+        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
@@ -639,7 +654,7 @@ sumif _ _ _ = 0
     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
+    existential typing, {\small{GADT}}s, etc.) which are not standard
     Haskell.  These will be left outside the scope of this research.
 
     Only an algebraic datatype declaration actually introduces a
@@ -663,9 +678,9 @@ sumif _ _ _ = 0
         structure. In fact, the built-in tuple types are just algebraic product
         types (and are thus supported in exactly the same way).
 
-        The ``product'' in its name refers to the collection of values belonging
-        to this type. The collection for a product type is the Cartesian
-        product of the collections for the types of its fields.
+        The \quote{product} in its name refers to the collection of values 
+        belonging to this type. The collection for a product type is the 
+        Cartesian product of the collections for the types of its fields.
 
         These types are translated to \VHDL\ record types, with one field for
         every field in the constructor. This translation applies to all single
@@ -690,7 +705,7 @@ sumif _ _ _ = 0
         for our purposes this distinction does not really make a
         difference, so this distinction is note made.
 
-        The ``sum'' in its name refers again to the collection of values
+        The \quote{sum} in its name refers again to the collection of values
         belonging to this type. The collection for a sum type is the
         union of the the collections for each of the constructors.
 
@@ -737,17 +752,55 @@ sumif _ _ _ = 0
 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 particularly for describing and reasoning about regular circuits. The Ruby~\cite{Ruby} language uses relations, instead of functions, to describe circuits, and has a particular focus on layout. \textsc{hml}~\cite{HML2} is a hardware modeling language based on the strict functional language \textsc{ml}, and has support for polymorphic types and higher-order functions. Published work suggests that there is no direct simulation support for \textsc{hml}, and that the translation to \VHDL\ is only partial.
-
-Like this work, many functional hardware description languages have some sort of foundation in the functional programming language Haskell. Hawk~\cite{Hawk1} uses Haskell to describe system-level executable specifications used to model the behavior of superscalar microprocessors. Hawk specifications can be simulated, but there seems to be no support for automated circuit synthesis. The ForSyDe~\cite{ForSyDe2} system uses Haskell to specify abstract system models, which can (manually) be transformed into an implementation model using semantic preserving transformations. ForSyDe has several simulation and synthesis backends, though synthesis is restricted to the synchronous subset of the ForSyDe language.
-
-Lava~\cite{Lava} is a hardware description language that focuses on the structural representation of hardware. Besides support for simulation and circuit synthesis, Lava descriptions can be interfaced with formal method tools for formal verification. Lava descriptions are actually circuit generators when viewed from a synthesis viewpoint, in that the language elements of Haskell, such as choice, can be used to guide the circuit generation. If a developer wants to insert a choice element inside an actual circuit he will have to specify this explicitly as a component. In this respect \CLaSH\ differs from Lava, in that all the choice elements, such as case-statements and patter matching, are synthesized to choice elements in the eventual circuit. As such, richer control structures can both be specified and synthesized in \CLaSH\ compared to any of the languages mentioned in this section.
-
-The merits of polymorphic typing, combined with higher-order functions, are now also recognized in the `main-stream' hardware description languages, exemplified by the new \VHDL\ 2008 standard~\cite{VHDL2008}. \VHDL-2008 has support to specify types as generics, thus allowing a developer to describe polymorphic components. Note that those types still require an explicit generic map, whereas type-inference and type-specialization are implicit in \CLaSH.
+Many functional hardware description languages have been developed over the 
+years. Early work includes such languages as \textsc{$\mu$fp}~\cite{muFP}, an 
+extension of Backus' \textsc{fp} language to synchronous streams, designed 
+particularly for describing and reasoning about regular circuits. The 
+Ruby~\cite{Ruby} language uses relations, instead of functions, to describe 
+circuits, and has a particular focus on layout. \textsc{hml}~\cite{HML2} is a 
+hardware modeling language based on the strict functional language 
+\textsc{ml}, and has support for polymorphic types and higher-order functions. 
+Published work suggests that there is no direct simulation support for 
+\textsc{hml}, and that the translation to \VHDL\ is only partial.
+
+Like this work, many functional hardware description languages have some sort 
+of foundation in the functional programming language Haskell. 
+Hawk~\cite{Hawk1} uses Haskell to describe system-level executable 
+specifications used to model the behavior of superscalar microprocessors. Hawk 
+specifications can be simulated, but there seems to be no support for 
+automated circuit synthesis. The ForSyDe~\cite{ForSyDe2} system uses Haskell 
+to specify abstract system models, which can (manually) be transformed into an 
+implementation model using semantic preserving transformations. ForSyDe has 
+several simulation and synthesis backends, though synthesis is restricted to 
+the synchronous subset of the ForSyDe language.
+
+Lava~\cite{Lava} is a hardware description language that focuses on the 
+structural representation of hardware. Besides support for simulation and 
+circuit synthesis, Lava descriptions can be interfaced with formal method 
+tools for formal verification. Lava descriptions are actually circuit 
+generators when viewed from a synthesis viewpoint, in that the language 
+elements of Haskell, such as choice, can be used to guide the circuit 
+generation. If a developer wants to insert a choice element inside an actual 
+circuit he will have to specify this explicitly as a component. In this 
+respect \CLaSH\ differs from Lava, in that all the choice elements, such as 
+case-statements and patter matching, are synthesized to choice elements in the 
+eventual circuit. As such, richer control structures can both be specified and 
+synthesized in \CLaSH\ compared to any of the languages mentioned in this 
+section.
+
+The merits of polymorphic typing, combined with higher-order functions, are 
+now also recognized in the `main-stream' hardware description languages, 
+exemplified by the new \VHDL\ 2008 standard~\cite{VHDL2008}. \VHDL-2008 has 
+support to specify types as generics, thus allowing a developer to describe 
+polymorphic components. Note that those types still require an explicit 
+generic map, whereas type-inference and type-specialization are implicit in 
+\CLaSH.
 
 Wired~\cite{Wired},, T-Ruby~\cite{T-Ruby}, Hydra~\cite{Hydra}. 
 
-A functional language designed specifically for hardware design is $re{\mathit{FL}}^{ect}$~\cite{reFLect}, which draws experience from earlier language called \textsc{fl}~\cite{FL} to la
+A functional language designed specifically for hardware design is 
+$re{\mathit{FL}}^{ect}$~\cite{reFLect}, which draws experience from earlier 
+language called \textsc{fl}~\cite{FL} to la
 
 % An example of a floating figure using the graphicx package.
 % Note that \label must occur AFTER (or within) \caption.