% should be used if it is desired that the figures are to be displayed in
% draft mode.
%
-\documentclass[conference]{IEEEtran}
+\documentclass[conference,pdf,a4paper,10pt,final,twoside,twocolumn]{IEEEtran}
% Add the compsoc option for Computer Society conferences.
%
% If IEEEtran.cls has not been installed into the LaTeX system files,
% manually specify the path to it like:
% \documentclass[conference]{../sty/IEEEtran}
-
-
-
-
% Some very useful LaTeX packages include:
% (uncomment the ones you want to load)
-
% *** MISC UTILITY PACKAGES ***
%
%\usepackage{ifpdf}
% *** CITATION PACKAGES ***
%
-%\usepackage{cite}
+\usepackage{cite}
% cite.sty was written by Donald Arseneau
% V1.6 and later of IEEEtran pre-defines the format of the cite.sty package
% \cite{} output to follow that of IEEE. Loading the cite package will
% (Unless specifically asked to do so by the journal or conference you plan
% to submit to, of course. )
-
% correct bad hyphenation here
\hyphenation{op-tical net-works semi-conduc-tor}
+% Macro for certain acronyms in small caps. Doesn't work with the
+% default font, though (it contains no smallcaps it seems).
+\def\VHDL{\textsc{vhdl}}
+\def\GHC{\textsc{ghc}}
+\def\CLaSH{\textsc{C$\lambda$aSH}}
+
+% Macro for pretty printing haskell snippets. Just monospaced for now, perhaps
+% we'll get something more complex later on.
+\def\hs#1{\texttt{#1}}
+\def\quote#1{``{#1}"}
\begin{document}
%
% paper title
% can use linebreaks \\ within to get better formatting as desired
-\title{Bare Demo of IEEEtran.cls for Conferences}
+\title{\CLaSH: Structural Descriptions \\ of Synchronous Hardware using Haskell}
% author names and affiliations
% use a multiple column layout for up to three different
% affiliations
-\author{\IEEEauthorblockN{Michael Shell}
-\IEEEauthorblockA{School of Electrical and\\Computer Engineering\\
-Georgia Institute of Technology\\
-Atlanta, Georgia 30332--0250\\
-Email: http://www.michaelshell.org/contact.html}
-\and
-\IEEEauthorblockN{Homer Simpson}
-\IEEEauthorblockA{Twentieth Century Fox\\
-Springfield, USA\\
-Email: homer@thesimpsons.com}
-\and
-\IEEEauthorblockN{James Kirk\\ and Montgomery Scott}
-\IEEEauthorblockA{Starfleet Academy\\
-San Francisco, California 96678-2391\\
-Telephone: (800) 555--1212\\
-Fax: (888) 555--1212}}
+\author{\IEEEauthorblockN{Christiaan P.R. Baaij, Matthijs Kooijman, Jan Kuper, Marco E.T. Gerards, Bert Molenkamp, Sabih H. Gerez}
+\IEEEauthorblockA{University of Twente, Department of EEMCS\\
+P.O. Box 217, 7500 AE, Enschede, The Netherlands\\
+c.p.r.baaij@utwente.nl, matthijs@stdin.nl}}
+% \and
+% \IEEEauthorblockN{Homer Simpson}
+% \IEEEauthorblockA{Twentieth Century Fox\\
+% Springfield, USA\\
+% Email: homer@thesimpsons.com}
+% \and
+% \IEEEauthorblockN{James Kirk\\ and Montgomery Scott}
+% \IEEEauthorblockA{Starfleet Academy\\
+% San Francisco, California 96678-2391\\
+% Telephone: (800) 555--1212\\
+% Fax: (888) 555--1212}}
% conference papers do not typically use \thanks and this command
% is locked out in conference mode. If really needed, such as for
\IEEEpeerreviewmaketitle
-
\section{Introduction}
-% no \IEEEPARstart
-This demo file is intended to serve as a ``starter file''
-for IEEE conference papers produced under \LaTeX\ using
-IEEEtran.cls version 1.7 and later.
-% You must have at least 2 lines in the paragraph with the drop letter
-% (should never be an issue)
-I wish you the best of success.
-
-\hfill mds
-
-\hfill January 11, 2007
-
-\subsection{Subsection Heading Here}
-Subsection text here.
-
-
-\subsubsection{Subsubsection Heading Here}
-Subsubsection text here.
-
+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}
+ 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.
+
+ 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
+
+ \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).
+
+ \begin{description}
+ \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}]
+ 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 \small{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}]
+ 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.
+ \end{description}
+ \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 will be left outside the scope of this research.
+
+ 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{description}
+
+ \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{description}
+
+
+\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
+particularly for describing and reasoning about regular circuits. The
+Ruby~\cite{Ruby} language uses relations, instead of functions, to describe
+circuits, and has a particular focus on layout. \textsc{hml}~\cite{HML2} is a
+hardware modeling language based on the strict functional language
+\textsc{ml}, and has support for polymorphic types and higher-order functions.
+Published work suggests that there is no direct simulation support for
+\textsc{hml}, and that the translation to \VHDL\ is only partial.
+
+Like this work, many functional hardware description languages have some sort
+of foundation in the functional programming language Haskell.
+Hawk~\cite{Hawk1} uses Haskell to describe system-level executable
+specifications used to model the behavior of superscalar microprocessors. Hawk
+specifications can be simulated, but there seems to be no support for
+automated circuit synthesis. The ForSyDe~\cite{ForSyDe2} system uses Haskell
+to specify abstract system models, which can (manually) be transformed into an
+implementation model using semantic preserving transformations. ForSyDe has
+several simulation and synthesis backends, though synthesis is restricted to
+the synchronous subset of the ForSyDe language.
+
+Lava~\cite{Lava} is a hardware description language that focuses on the
+structural representation of hardware. Besides support for simulation and
+circuit synthesis, Lava descriptions can be interfaced with formal method
+tools for formal verification. Lava descriptions are actually circuit
+generators when viewed from a synthesis viewpoint, in that the language
+elements of Haskell, such as choice, can be used to guide the circuit
+generation. If a developer wants to insert a choice element inside an actual
+circuit he will have to specify this explicitly as a component. In this
+respect \CLaSH\ differs from Lava, in that all the choice elements, such as
+case-statements and patter matching, are synthesized to choice elements in the
+eventual circuit. As such, richer control structures can both be specified and
+synthesized in \CLaSH\ compared to any of the languages mentioned in this
+section.
+
+The merits of polymorphic typing, combined with higher-order functions, are
+now also recognized in the `main-stream' hardware description languages,
+exemplified by the new \VHDL\ 2008 standard~\cite{VHDL2008}. \VHDL-2008 has
+support to specify types as generics, thus allowing a developer to describe
+polymorphic components. Note that those types still require an explicit
+generic map, whereas type-inference and type-specialization are implicit in
+\CLaSH.
+
+Wired~\cite{Wired},, T-Ruby~\cite{T-Ruby}, Hydra~\cite{Hydra}.
+
+A functional language designed specifically for hardware design is
+$re{\mathit{FL}}^{ect}$~\cite{reFLect}, which draws experience from earlier
+language called \textsc{fl}~\cite{FL} to la
% An example of a floating figure using the graphicx package.
% Note that \label must occur AFTER (or within) \caption.
% http://www.ctan.org/tex-archive/biblio/bibtex/contrib/doc/
% The IEEEtran BibTeX style support page is at:
% http://www.michaelshell.org/tex/ieeetran/bibtex/
-%\bibliographystyle{IEEEtran}
+\bibliographystyle{IEEEtran}
% argument is your BibTeX string definitions and bibliography database(s)
-%\bibliography{IEEEabrv,../bib/paper}
+\bibliography{IEEEabrv,cλash.bib}
%
% <OR> manually copy in the resultant .bbl file
% set second argument of \begin to the number of references
% (used to reserve space for the reference number labels box)
-\begin{thebibliography}{1}
-
-\bibitem{IEEEhowto:kopka}
-H.~Kopka and P.~W. Daly, \emph{A Guide to \LaTeX}, 3rd~ed.\hskip 1em plus
- 0.5em minus 0.4em\relax Harlow, England: Addison-Wesley, 1999.
-
-\end{thebibliography}
+% \begin{thebibliography}{1}
+%
+% \bibitem{IEEEhowto:kopka}
+% H.~Kopka and P.~W. Daly, \emph{A Guide to \LaTeX}, 3rd~ed.\hskip 1em plus
+% 0.5em minus 0.4em\relax Harlow, England: Addison-Wesley, 1999.
+%
+% \end{thebibliography}
% that's all folks
\end{document}
-
+% vim: set ai sw=2 sts=2 expandtab:
projects / matthijs / master-project / dsd-paper.git / blobdiff