X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Fdsd-paper.git;a=blobdiff_plain;f=c%CE%BBash.tex;h=3c16f27731747427b9bb1bb675f5ea49d05894ef;hp=f3988f5264b0ae0872397fd1b1612e296882b324;hb=edf6a3b674b4ac1893db075da81069ac0c088002;hpb=4dfd0446bd5cdebd6a50c7cb6287148fbff6cc33 diff --git "a/c\316\273ash.tex" "b/c\316\273ash.tex" index f3988f5..3c16f27 100644 --- "a/c\316\273ash.tex" +++ "b/c\316\273ash.tex" @@ -63,21 +63,16 @@ % 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} @@ -103,7 +98,7 @@ % *** 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 @@ -343,41 +338,45 @@ % (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\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 @@ -441,22 +440,367 @@ The abstract goes here. \IEEEpeerreviewmaketitle - \section{Introduction} - -foo\par bar % Won't compile without at least two paragraphs. - +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} -foo\par bar - -\section{Cλash prototype} + \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 ``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 ``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} - -foo\par bar +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. @@ -576,20 +920,20 @@ The authors would like to thank... % 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} % % 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} @@ -597,4 +941,4 @@ H.~Kopka and P.~W. Daly, \emph{A Guide to \LaTeX}, 3rd~ed.\hskip 1em plus % that's all folks \end{document} - +% vim: set ai sw=2 sts=2 expandtab: