-\chapter{Prototype}
- Choice of Haskell
- Core - description of the language (appendix?)
- Stages (-> Core, Normalization, -> VHDL)
- Implementation issues
-
- Haskell language coverage / constraints
- Recursion
- Builtin types
- Custom types (Sum types, product types)
- Function types / higher order expressions
+\chapter[chap:prototype]{Prototype}
+ An important step in this research is the creation of a prototype compiler.
+ Having this prototype allows us to apply the ideas from the previous chapter
+ to actual hardware descriptions and evaluate their usefulness. Having a
+ prototype also helps to find new techniques and test possible
+ interpretations.
+ Obviously the prototype was not created after all research
+ ideas were formed, but its implementation has been interleaved with the
+ research itself. Also, the prototype described here is the final version, it
+ has gone through a number of design iterations which we will not completely
+ describe here.
+
+ \section[sec:prototype:input]{Input language}
+ When implementing this prototype, the first question to ask is:
+ Which (functional) language will be used to describe our hardware?
+ (Note that this does not concern the \emph{implementation language}
+ of the compiler, just the language \emph{translated by} the
+ compiler).
+
+ Initially, we have two choices:
+
+ \startitemize
+ \item Create a new functional language from scratch. This has the
+ advantage of having a language that contains exactly those elements that
+ are convenient for describing hardware and can contain special
+ constructs that allows our hardware descriptions to be more powerful or
+ concise.
+ \item Use an existing language and create a new backend for it. This has
+ the advantage that existing tools can be reused, which will speed up
+ development.
+ \stopitemize
+
+
+ \placeintermezzo{}{
+ \startframedtext[width=8cm,background=box,frame=no]
+ \startalignment[center]
+ {\tfa No \small{EDSL} or Template Haskell}
+ \stopalignment
+ \blank[medium]
+
+ Note that in this consideration, embedded domain-specific
+ languages (\small{EDSL}) and Template Haskell (\small{TH})
+ approaches have not been included. As we have seen in
+ \in{section}[sec:context:fhdls], these approaches have all kinds
+ of limitations on the description language that we would like to
+ avoid.
+ \stopframedtext
+ }
+ Considering that we required a prototype which should be working quickly,
+ and that implementing parsers, semantic checkers and especially
+ typcheckers is not exactly the core of this research (but it is lots and
+ lots of work!), using an existing language is the obvious choice. This
+ also has the advantage that a large set of language features is available
+ to experiment with and it is easy to find which features apply well and
+ which do not. Another import advantage of using an existing language, is
+ that simulation of the code becomes trivial. Since there are existing
+ compilers and interpreters that can run the hardware description directly,
+ it can be simulated without also having to write an interpreter for the
+ new language.
+
+ A possible second prototype could use a custom language with just the useful
+ features (and possibly extra features that are specific to
+ the domain of hardware description as well).
+
+ The second choice to be made is which of the many existing languages to use. As
+ mentioned before, the chosen language is Haskell. This choice has not been the
+ result of a thorough comparison of languages, for the simple reason that
+ the requirements on the language were completely unclear at the start of
+ this research. The fact that Haskell is a language with a broad spectrum
+ of features, that it is commonly used in research projects and that the
+ primary compiler, \GHC, provides a high level API to its internals, made
+ Haskell an obvious choice.
+
+ \section[sec:prototype:output]{Output format}
+ The second important question is: what will be our output format?
+ This output format should at least allow for programming the
+ hardware design into a field-programmable gate array (\small{FPGA}).
+ The choice of output format is thus limited by what hardware
+ synthesis and programming tools can process.
+
+ Looking at other tools in the industry, the Electronic Design Interchange
+ Format (\small{EDIF}) is commonly used for storing intermediate
+ \emph{netlists} (lists of components and connections between these
+ components) and is commonly the target for \small{VHDL} and Verilog
+ compilers.
+
+ However, \small{EDIF} is not completely tool-independent. It specifies a
+ meta-format, but the hardware components that can be used vary between
+ various tool and hardware vendors, as well as the interpretation of the
+ \small{EDIF} standard. \cite[li89]
+
+ This means that when working with \small{EDIF}, our prototype would become
+ technology dependent (\eg\ only work with \small{FPGA}s of a specific
+ vendor, or even only with specific chips). This limits the applicability
+ of our prototype. Also, the tools we would like to use for verifying,
+ simulating and draw pretty pictures of our output (like Precision, or
+ QuestaSim) are designed for \small{VHDL} or Verilog input.
+
+ For these reasons, we will not use \small{EDIF}, but \small{VHDL} as our
+ output language. We choose \VHDL\ over Verilog simply because we are
+ familiar with \small{VHDL} already. The differences between \small{VHDL}
+ and Verilog are on the higher level, while we will be using \small{VHDL}
+ mainly to write low level, netlist-like descriptions anyway.
+
+ An added advantage of using VHDL is that we can profit from existing
+ optimizations in VHDL synthesizers. A lot of optimizations are done on the
+ VHDL level by existing tools. These tools have been under
+ development for years, so it would not be reasonable to assume we
+ could achieve a similar amount of optimization in our prototype (nor
+ should it be a goal, considering this is just a prototype).
+
+ \placeintermezzo{}{
+ \startframedtext[width=8cm,background=box,frame=no]
+ \startalignment[center]
+ {\tfa Translation vs. compilation vs. synthesis}
+ \stopalignment
+ \blank[medium]
+ In this thesis the words \emph{translation}, \emph{compilation} and
+ sometimes \emph{synthesis} will be used interchangedly to refer to the
+ process of translating the hardware description from the Haskell
+ language to the \VHDL\ language.
+
+ Similarly, the prototype created is referred to as both the
+ \emph{translator} as well as the \emph{compiler}.
+
+ The final part of this process is usually referred to as \emph{\VHDL\
+ generation}.
+ \stopframedtext
+ }
+
+ Note that we will be using \small{VHDL} as our output language, but will
+ not use its full expressive power. Our output will be limited to using
+ simple, structural descriptions, without any complex behavioural
+ descriptions like arbitrary sequential statements (which might not
+ be supported by all tools). This ensures that any tool that works
+ with \VHDL\ will understand our output (most tools do not support
+ synthesis of more complex \VHDL). This also leaves open the option
+ to switch to \small{EDIF} in the future, with minimal changes to the
+ prototype.
+
+ \section{Simulation and synthesis}
+ As mentioned above, by using the Haskell language, we get simulation of
+ our hardware descriptions almost for free. The only thing that is needed
+ is to provide a Haskell implementation of all built-in functions that can
+ be used by the Haskell interpreter to simulate them.
+
+ The main topic of this thesis is therefore the path from the Haskell
+ hardware descriptions to \small{FPGA} synthesis, focusing of course on the
+ \VHDL\ generation. Since the \VHDL\ generation process preserves the meaning
+ of the Haskell description exactly, any simulation done in Haskell
+ \emph{should} produce identical results as the synthesized hardware.
+
+ \section[sec:prototype:design]{Prototype design}
+ As suggested above, we will use the Glasgow Haskell Compiler (\small{GHC}) to
+ implement our prototype compiler. To understand the design of the
+ compiler, we will first dive into the \small{GHC} compiler a bit. Its
+ compilation consists of the following steps (slightly simplified):
+
+ \startuseMPgraphic{ghc-pipeline}
+ % Create objects
+ save inp, front, desugar, simpl, back, out;
+ newEmptyBox.inp(0,0);
+ newBox.front(btex Frontend etex);
+ newBox.desugar(btex Desugarer etex);
+ newBox.simpl(btex Simplifier etex);
+ newBox.back(btex Backend etex);
+ newEmptyBox.out(0,0);
+
+ % Space the boxes evenly
+ inp.c - front.c = front.c - desugar.c = desugar.c - simpl.c
+ = simpl.c - back.c = back.c - out.c = (0, 1.5cm);
+ out.c = origin;
+
+ % Draw lines between the boxes. We make these lines "deferred" and give
+ % them a name, so we can use ObjLabel to draw a label beside them.
+ ncline.inp(inp)(front) "name(haskell)";
+ ncline.front(front)(desugar) "name(ast)";
+ ncline.desugar(desugar)(simpl) "name(core)";
+ ncline.simpl(simpl)(back) "name(simplcore)";
+ ncline.back(back)(out) "name(native)";
+ ObjLabel.inp(btex Haskell source etex) "labpathname(haskell)", "labdir(rt)";
+ ObjLabel.front(btex Haskell AST etex) "labpathname(ast)", "labdir(rt)";
+ ObjLabel.desugar(btex Core etex) "labpathname(core)", "labdir(rt)";
+ ObjLabel.simpl(btex Simplified core etex) "labpathname(simplcore)", "labdir(rt)";
+ ObjLabel.back(btex Native code etex) "labpathname(native)", "labdir(rt)";
+
+ % Draw the objects (and deferred labels)
+ drawObj (inp, front, desugar, simpl, back, out);
+ \stopuseMPgraphic
+ \placefigure[right]{GHC compiler pipeline}{\useMPgraphic{ghc-pipeline}}
+
+ \startdesc{Frontend}
+ This step takes the Haskell source files and parses them into an
+ abstract syntax tree (\small{AST}). This \small{AST} can express the
+ complete Haskell language and is thus a very complex one (in contrast
+ with the Core \small{AST}, later on). All identifiers in this
+ \small{AST} are resolved by the renamer and all types are checked by the
+ typechecker.
+ \stopdesc
+ \startdesc{Desugaring}
+ This steps takes the full \small{AST} and translates it to the
+ \emph{Core} language. Core is a very small functional language with lazy
+ semantics, that can still express everything Haskell can express. Its
+ simpleness makes Core very suitable for further simplification and
+ translation. Core is the language we will be working with as well.
+ \stopdesc
+ \startdesc{Simplification}
+ Through a number of simplification steps (such as inlining, common
+ subexpression elimination, etc.) the Core program is simplified to make
+ it faster or easier to process further.
+ \stopdesc
+ \startdesc{Backend}
+ This step takes the simplified Core program and generates an actual
+ runnable program for it. This is a big and complicated step we will not
+ discuss it any further, since it is not required for our prototype.
+ \stopdesc
+
+ In this process, there are a number of places where we can start our work.
+ Assuming that we do not want to deal with (or modify) parsing, typechecking
+ and other frontend business and that native code is not really a useful
+ format anymore, we are left with the choice between the full Haskell
+ \small{AST}, or the smaller (simplified) core representation.
+
+ The advantage of taking the full \small{AST} is that the exact structure
+ of the source program is preserved. We can see exactly what the hardware
+ description looks like and which syntax constructs were used. However,
+ the full \small{AST} is a very complicated datastructure. If we are to
+ handle everything it offers, we will quickly get a big compiler.
+
+ Using the core representation gives us a much more compact datastructure
+ (a core expression only uses 9 constructors). Note that this does not mean
+ that the core representation itself is smaller, on the contrary.
+ Since the core language has less constructs, most Core expressions
+ are larger than the equivalent versions in Haskell.
+
+ However, the fact that the core language is so much smaller, means it is a
+ lot easier to analyze and translate it into something else. For the same
+ reason, \small{GHC} runs its simplifications and optimizations on the core
+ representation as well \cite[jones96].
+
+ We will use the normal Core representation, not the simplified Core. Even
+ though the simplified Core version is an equivalent, but simpler
+ definition, some problems were encountered with it in practice. The
+ simplifier restructures some (stateful) functions in a way the normalizer
+ and the \VHDL\ generation cannot handle, leading to uncompilable programs
+ (whereas the non-simplified version more closely resembles the original
+ program, allowing the original to be written in a way that can be
+ handled). This problem is further discussed in
+ \in{section}[sec:normalization:stateproblems].
+
+ The final prototype roughly consists of three steps:
+
+ \startuseMPgraphic{clash-pipeline}
+ % Create objects
+ save inp, front, norm, vhdl, out;
+ newEmptyBox.inp(0,0);
+ newBox.front(btex \small{GHC} frontend etex);
+ newBox.norm(btex Normalization etex);
+ newBox.vhdl(btex \small{VHDL} generation etex);
+ newEmptyBox.out(0,0);
+
+ % Space the boxes evenly
+ inp.c - front.c = front.c - norm.c = norm.c - vhdl.c
+ = vhdl.c - out.c = (0, 1.5cm);
+ out.c = origin;
+
+ % Draw lines between the boxes. We make these lines "deferred" and give
+ % them a name, so we can use ObjLabel to draw a label beside them.
+ ncline.inp(inp)(front) "name(haskell)";
+ ncline.front(front)(norm) "name(core)";
+ ncline.norm(norm)(vhdl) "name(normal)";
+ ncline.vhdl(vhdl)(out) "name(vhdl)";
+ ObjLabel.inp(btex Haskell source etex) "labpathname(haskell)", "labdir(rt)";
+ ObjLabel.front(btex Core etex) "labpathname(core)", "labdir(rt)";
+ ObjLabel.norm(btex Normalized core etex) "labpathname(normal)", "labdir(rt)";
+ ObjLabel.vhdl(btex \small{VHDL} description etex) "labpathname(vhdl)", "labdir(rt)";
+
+ % Draw the objects (and deferred labels)
+ drawObj (inp, front, norm, vhdl, out);
+ \stopuseMPgraphic
+ \placefigure[right]{Cλash compiler pipeline}{\useMPgraphic{clash-pipeline}}
+
+ \startdesc{Frontend}
+ This is exactly the frontend from the \small{GHC} pipeline, that
+ translates Haskell sources to a typed Core representation.
+ \stopdesc
+ \startdesc{Normalization}
+ This is a step that transforms the core representation into a normal
+ form. This normal form is still expressed in the core language, but has
+ to adhere to an additional set of constraints. This normal form is less
+ expressive than the full core language (e.g., it can have limited
+ higher-order expressions, has a specific structure, etc.), but is
+ also very close to directly describing hardware.
+ \stopdesc
+ \startdesc{\small{VHDL} generation}
+ The last step takes the normal formed core representation and generates
+ \small{VHDL} for it. Since the normal form has a specific, hardware-like
+ structure, this final step is very straightforward.
+ \stopdesc
+
+ The most interesting step in this process is the normalization step. That
+ is where more complicated functional constructs, which have no direct
+ hardware interpretation, are removed and translated into hardware
+ constructs. This step is described in a lot of detail at
+ \in{chapter}[chap:normalization].
+
+
+ \defref{entry function}Translation of a hardware description always
+ starts at a single function, which is referred to as the \emph{entry
+ function}. \VHDL\ is generated for this function first, followed by
+ any functions used by the entry functions (recursively).
+
+ \section[sec:prototype:core]{The Core language}
+ \defreftxt{core}{the Core language}
+ Most of the prototype deals with handling the program in the Core
+ language. In this section we will show what this language looks like and
+ how it works.
+
+ The Core language is a functional language that describes
+ \emph{expressions}. Every identifier used in Core is called a
+ \emph{binder}, since it is bound to a value somewhere. On the highest
+ level, a Core program is a collection of functions, each of which bind a
+ binder (the function name) to an expression (the function value, which has
+ a function type).
+
+ The Core language itself does not prescribe any program structure
+ (like modules, declarations, imports, etc.), only expression
+ structure. In the \small{GHC} compiler, the Haskell module structure
+ is used for the resulting Core code as well. Since this is not so
+ relevant for understanding the Core language or the Normalization
+ process, we will only look at the Core expression language here.
+
+ Each Core expression consists of one of these possible expressions.
+
+ \startdesc{Variable reference}
+ \defref{variable reference}
+ \startlambda
+ bndr :: T
+ \stoplambda
+ This is a reference to a binder. It is written down as the
+ name of the binder that is being referred to along with its type. The
+ binder name should of course be bound in a containing scope
+ (including top level scope, so a reference to a top level function
+ is also a variable reference). Additionally, constructors from
+ algebraic datatypes also become variable references.
+
+ In our examples, binders will commonly consist of a single
+ characters, but they can have any length.
+
+ The value of this expression is the value bound to the given
+ binder.
+
+ Each binder also carries around its type (explicitly shown above), but
+ this is usually not shown in the Core expressions. Only when the type is
+ relevant (when a new binder is introduced, for example) will it be
+ shown. In other cases, the binder is either not relevant, or easily
+ derived from the context of the expression. \todo{Ref sidenote on type
+ annotations}
+ \stopdesc
+
+ \startdesc{Literal}
+ \defref{literal}
+ \startlambda
+ 10
+ \stoplambda
+ This is a literal. Only primitive types are supported, like
+ chars, strings, ints and doubles. The types of these literals are the
+ \quote{primitive}, unboxed versions, like \lam{Char\#} and \lam{Word\#}, not the
+ normal Haskell versions (but there are built-in conversion
+ functions). Without going into detail about these types, note that
+ a few conversion functions exist to convert these to the normal
+ (boxed) Haskell equivalents.
+ \stopdesc
+
+ \startdesc{Application}
+ \defref{application}
+ \startlambda
+ func arg
+ \stoplambda
+ This is function application. Each application consists of two
+ parts: the function part and the argument part. Applications are used
+ for normal function \quote{calls}, but also for applying type
+ abstractions and data constructors.
+
+ In core, there is no distinction between an operator and a
+ function. This means that, for example the addition of two numbers
+ looks like the following in Core:
+
+ \startlambda
+ (+) 1 2
+ \stoplambda
+
+ Where the function \quote{\lam{(+)}} is applied to the numbers 1
+ and 2. However, to increase readability, an application of an
+ operator like \lam{(+)} is sometimes written infix. In this case,
+ the parenthesis are also left out, just like in Haskell. In other
+ words, the following means exactly the same as the addition above:
+
+ \startlambda
+ 1 + 2
+ \stoplambda
+
+ The value of an application is the value of the function part, with the
+ first argument binder bound to the argument part.
+ \stopdesc
+
+ \startdesc{Lambda abstraction}
+ \defref{lambda abstraction}
+ \startlambda
+ λbndr.body
+ \stoplambda
+ This is the basic lambda abstraction, as it occurs in lambda calculus.
+ It consists of a binder part and a body part. A lambda abstraction
+ creates a function, that can be applied to an argument. The binder is
+ usually a value binder, but it can also be a \emph{type binder} (or
+ \emph{type variable}). The latter case introduces a new polymorphic
+ variable, which can be used in types later on. See
+ \in{section}[sec:prototype:coretypes] for details.
+
+ The body of a lambda abstraction extends all the way to the end of
+ the expression, or the closing bracket surrounding the lambda. In
+ other words, the lambda abstraction \quote{operator} has the
+ lowest priority of all.
+
+ The value of an application is the value of the body part, with the
+ binder bound to the value the entire lambda abstraction is applied to.
+ \stopdesc
+
+ \startdesc{Non-recursive let expression}
+ \defref{let expression}
+ \startlambda
+ let bndr = value in body
+ \stoplambda
+ A let expression allows you to bind a binder to some value, while
+ evaluating to some other value (for which that binder is in scope). This
+ allows for sharing of subexpressions (you can use a binder twice) and
+ explicit \quote{naming} of arbitrary expressions. A binder is not
+ in scope in the value bound it is bound to, so it is not possible
+ to make recursive definitions with a non-recursive let expression
+ (see the recursive form below).
+
+ Even though this let expression is an extension on the basic lambda
+ calculus, it is easily translated to a lambda abstraction. The let
+ expression above would then become:
+
+ \startlambda
+ (λbndr.body) value
+ \stoplambda
+
+ This notion might be useful for verifying certain properties on
+ transformations, since a lot of verification work has been done on
+ lambda calculus already.
+
+ The value of a let expression is the value of the body part, with the
+ binder bound to the value.
+ \stopdesc
+
+ \startdesc{Recursive let expression}
+ \startlambda
+ letrec
+ bndr1 = value1
+ \vdots
+ bndrn = valuen
+ in
+ body
+ \stoplambda
+ This is the recursive version of the let expression. In \small{GHC}'s
+ Core implementation, non-recursive and recursive lets are not so
+ distinct as we present them here, but this provides a clearer overview.
+
+ The main difference with the normal let expression is that it can
+ contain multiple bindings (or even none) and each of the binders
+ is in scope in each of the values, in addition to the body. This
+ allows for self-recursive or mutually recursive definitions.
+
+ It is also possible to express a recursive let expression using
+ normal lambda calculus, if we use the \emph{least fixed-point
+ operator}, \lam{Y} (but the details are too complicated to help
+ clarify the let expression, so this will not be explored further).
+ \stopdesc
+
+ \placeintermezzo{}{
+ \startframedtext[width=8cm,background=box,frame=no]
+ \startalignment[center]
+ {\tfa Weak head normal form (\small{WHNF})}
+ \stopalignment
+ \blank[medium]
+ An expression is in weak head normal form if it is either an
+ constructor application or lambda abstraction. \todo{How about
+ atoms?}
+
+ Without going into detail about the differences with head
+ normal form and normal form, note that evaluating the scrutinee
+ of a case expression to normal form (evaluating any function
+ applications, variable references and case expressions) is
+ sufficient to decide which case alternatives should be chosen.
+ \todo{ref?}
+ \stopframedtext
+
+ }
+
+ \startdesc{Case expression}
+ \defref{case expression}
+ \startlambda
+ case scrutinee of bndr
+ DEFAULT -> defaultbody
+ C0 bndr0,0 ... bndr0,m -> body0
+ \vdots
+ Cn bndrn,0 ... bndrn,m -> bodyn
+ \stoplambda
+
+ A case expression is the only way in Core to choose between values. All
+ \hs{if} expressions and pattern matchings from the original Haskell
+ PRogram have been translated to case expressions by the desugarer.
+
+ A case expression evaluates its scrutinee, which should have an
+ algebraic datatype, into weak head normal form (\small{WHNF}) and
+ (optionally) binds it to \lam{bndr}. If bndr is wild, \refdef{wild
+ binders} it is left out. Every alternative lists a single constructor
+ (\lam{C0 ... Cn}). Based on the actual constructor of the scrutinee, the
+ corresponding alternative is chosen. The binders in the chosen
+ alternative (\lam{bndr0,0 .... bndr0,m} are bound to the actual
+ arguments to the constructor in the scrutinee.
+
+ This is best illustrated with an example. Assume
+ there is an algebraic datatype declared as follows\footnote{This
+ datatype is not suported by the current Cλash implementation, but
+ serves well to illustrate the case expression}:
+
+ \starthaskell
+ data D = A Word | B Bit
+ \stophaskell
+
+ This is an algebraic datatype with two constructors, each getting
+ a single argument. A case expression scrutinizing this datatype
+ could look like the following:
+
+ \startlambda
+ case s of
+ A word -> High
+ B bit -> bit
+ \stoplambda
+
+ What this expression does is check the constructor of the
+ scrutinee \lam{s}. If it is \lam{A}, it always evaluates to
+ \lam{High}. If the constructor is \lam{B}, the binder \lam{bit} is
+ bound to the argument passed to \lam{B} and the case expression
+ evaluates to this bit.
+
+ If none of the alternatives match, the \lam{DEFAULT} alternative
+ is chosen. A case expression must always be exhaustive, \ie\ it
+ must cover all possible constructors that the scrutinee can have
+ (if all of them are covered explicitly, the \lam{DEFAULT}
+ alternative can be left out).
+
+ Since we can only match the top level constructor, there can be no overlap
+ in the alternatives and thus order of alternatives is not relevant (though
+ the \lam{DEFAULT} alternative must appear first for implementation
+ efficiency).
+
+ To support strictness, the scrutinee is always evaluated into
+ \small{WHNF}, even when there is only a \lam{DEFAULT} alternative. This
+ allows aplication of the strict function \lam{f} to the argument \lam{a}
+ to be written like:
+
+ \startlambda
+ f (case a of arg DEFAULT -> arg)
+ \stoplambda
+
+ According to the \GHC\ documentation, this is the only use for the extra
+ binder to which the scrutinee is bound. When not using strictness
+ annotations (which is rather pointless in hardware descriptions),
+ \small{GHC} seems to never generate any code making use of this binder.
+ In fact, \GHC\ has never been observed to generate code using this
+ binder, even when strictness was involved. Nonetheless, the prototype
+ handles this binder as expected.
+
+ Note that these case expressions are less powerful than the full Haskell
+ case expressions. In particular, they do not support complex patterns like
+ in Haskell. Only the constructor of an expression can be matched,
+ complex patterns are implemented using multiple nested case expressions.
+
+ Case expressions are also used for unpacking of algebraic datatypes, even
+ when there is only a single constructor. For examples, to add the elements
+ of a tuple, the following Core is generated:
+
+ \startlambda
+ sum = λtuple.case tuple of
+ (,) a b -> a + b
+ \stoplambda
+
+ Here, there is only a single alternative (but no \lam{DEFAULT}
+ alternative, since the single alternative is already exhaustive). When
+ its body is evaluated, the arguments to the tuple constructor \lam{(,)}
+ (\eg, the elements of the tuple) are bound to \lam{a} and \lam{b}.
+ \stopdesc
+
+ \startdesc{Cast expression}
+ \defref{cast expression}
+ \startlambda
+ body ▶ targettype
+ \stoplambda
+ A cast expression allows you to change the type of an expression to an
+ equivalent type. Note that this is not meant to do any actual work, like
+ conversion of data from one format to another, or force a complete type
+ change. Instead, it is meant to change between different representations
+ of the same type, \eg\ switch between types that are provably equal (but
+ look different).
+
+ In our hardware descriptions, we typically see casts to change between a
+ Haskell newtype and its contained type, since those are effectively
+ different types (so a cast is needed) with the same representation (but
+ no work is done by the cast).
+
+ More complex are types that are proven to be equal by the typechecker,
+ but look different at first glance. To ensure that, once the typechecker
+ has proven equality, this information sticks around, explicit casts are
+ added. In our notation we only write the target type, but in reality a
+ cast expressions carries around a \emph{coercion}, which can be seen as a
+ proof of equality. \todo{Example}
+
+ The value of a cast is the value of its body, unchanged. The type of this
+ value is equal to the target type, not the type of its body.
+ \stopdesc
+
+ \startdesc{Note}
+ The Core language in \small{GHC} allows adding \emph{notes}, which serve
+ as hints to the inliner or add custom (string) annotations to a core
+ expression. These should not be generated normally, so these are not
+ handled in any way in the prototype.
+ \stopdesc
+
+ \startdesc{Type}
+ \defref{type expression}
+ \startlambda
+ @T
+ \stoplambda
+ It is possibly to use a Core type as a Core expression. To prevent
+ confusion between types and values, the \lam{@} sign is used to
+ explicitly mark a type that is used in a Core expression.
+
+ For the actual types supported by Core, see
+ \in{section}[sec:prototype:coretypes]. This \quote{lifting} of a
+ type into the value domain is done to allow for type abstractions
+ and applications to be handled as normal lambda abstractions and
+ applications above. This means that a type expression in Core can
+ only ever occur in the argument position of an application, and
+ only if the type of the function that is applied to expects a type
+ as the first argument. This happens in applications of all
+ polymorphic functions. Consider the \lam{fst} function:
+
+ \startlambda
+ fst :: \forall t1. \forall t2. (t1, t2) ->t1
+ fst = λt1.λt2.λ(tup :: (t1, t2)). case tup of (,) a b -> a
+
+ fstint :: (Int, Int) -> Int
+ fstint = λa.λb.fst @Int @Int a b
+ \stoplambda
+
+ The type of \lam{fst} has two universally quantified type variables. When
+ \lam{fst} is applied in \lam{fstint}, it is first applied to two types.
+ (which are substitued for \lam{t1} and \lam{t2} in the type of \lam{fst}, so
+ the actual type of arguments and result of \lam{fst} can be found:
+ \lam{fst @Int @Int :: (Int, Int) -> Int}).
+ \stopdesc
+
+ \subsection[sec:prototype:coretypes]{Core type system}
+ Whereas the expression syntax of Core is very simple, its type system is
+ a bit more complicated. It turns out it is harder to \quote{desugar}
+ Haskell's complex type system into something more simple. Most of the
+ type system is thus very similar to that of Haskell.
+
+ We will slightly limit our view on Core's type system, since the more
+ complicated parts of it are only meant to support Haskell's (or rather,
+ \GHC's) type extensions, such as existential types, \small{GADT}s, type
+ families and other non-standard Haskell stuff which we do not (plan to)
+ support.
+
+ \placeintermezzo{}{
+ \startframedtext[width=8cm,background=box,frame=no]
+ \startalignment[center]
+ {\tfa The \hs{id} function}
+ \stopalignment
+ \blank[medium]
+ A function that is probably present in every functional language, is
+ the \emph{identity} function. This is the function that takes a
+ single argument and simply returns it unmodified. In Haskell this
+ function is called \hs{id} and can take an argument of any type
+ (\ie, it is polymorphic).
+
+ The \hs{id} function will be used in the examples every now and
+ then.
+ \stopframedtext
+ }
+ In Core, every expression is typed. The translation to Core happens
+ after the typechecker, so types in Core are always correct as well
+ (though you could of course construct invalidly typed expressions
+ through the \GHC\ API).
+
+ Any type in core is one of the following:
+
+ \startdesc{A type variable}
+ \startlambda
+ t
+ \stoplambda
+
+ This is a reference to a type defined elsewhere. This can either be a
+ polymorphic type (like the latter two \lam{t}'s in \lam{id :: \forall t.
+ t -> t}), or a type constructor (like \lam{Bool} in \lam{not :: Bool ->
+ Bool}). Like in Haskell, polymorphic type variables always
+ start with a lowercase letter, while type constructors always start
+ with an uppercase letter.
+
+ \todo{How to define (new) type constructors?}
+
+ A special case of a type constructor is the \emph{function type
+ constructor}, \lam{->}. This is a type constructor taking two arguments
+ (using application below). The function type constructor is commonly
+ written inline, so we write \lam{a -> b} when we really mean \lam{-> a
+ b}, the function type constructor applied to \lam{a} and \lam{b}.
+
+ Polymorphic type variables can only be defined by a lambda
+ abstraction, see the forall type below.
+ \stopdesc
+
+ \startdesc{A type application}
+ \startlambda
+ Maybe Int
+ \stoplambda
+
+ This applies some type to another type. This is particularly used to
+ apply type variables (type constructors) to their arguments.
+
+ As mentioned above, applications of some type constructors have
+ special notation. In particular, these are applications of the
+ \emph{function type constructor} and \emph{tuple type constructors}:
+ \startlambda
+ foo :: t1 -> t2
+ foo' :: -> t1 t2
+ bar :: (t1, t2, t3)
+ bar' :: (,,) t1 t2 t3
+ \stoplambda
+ \stopdesc
+
+ \startdesc{The forall type}
+ \startlambda
+ id :: \forall t. t -> t
+ \stoplambda
+ The forall type introduces polymorphism. It is the only way to
+ introduce new type variables, which are completely unconstrained (Any
+ possible type can be assigned to it). Constraints can be added later
+ using predicate types, see below.
+
+ A forall type is always (and only) introduced by a type lambda
+ expression. For example, the Core translation of the
+ id function is:
+ \startlambda
+ id = λt.λ(x :: t).x
+ \stoplambda
+
+ Here, the type of the binder \lam{x} is \lam{t}, referring to the
+ binder in the topmost lambda.
+
+ When using a value with a forall type, the actual type
+ used must be applied first. For example Haskell expression \hs{id
+ True} (the function \hs{id} appleid to the dataconstructor \hs{True})
+ translates to the following Core:
+
+ \startlambda
+ id @Bool True
+ \stoplambda
+
+ Here, id is first applied to the type to work with. Note that the type
+ then changes from \lam{id :: \forall t. t -> t} to \lam{id @Bool ::
+ Bool -> Bool}. Note that the type variable \lam{a} has been
+ substituted with the actual type.
+
+ In Haskell, forall types are usually not explicitly specified (The use
+ of a lowercase type variable implicitly introduces a forall type for
+ that variable). In fact, in standard Haskell there is no way to
+ explicitly specify forall types. Through a language extension, the
+ \hs{forall} keyword is available, but still optional for normal forall
+ types (it is needed for \emph{existentially quantified types}, which
+ Cλash does not support).
+ \stopdesc
+
+ \startdesc{Predicate type}
+ \startlambda
+ show :: \forall t. Show t ⇒ t → String
+ \stoplambda
+
+ \todo{Sidenote: type classes?}
+
+ A predicate type introduces a constraint on a type variable introduced
+ by a forall type (or type lambda). In the example above, the type
+ variable \lam{t} can only contain types that are an \emph{instance} of
+ the \emph{type class} \lam{Show}. \refdef{type class}
+
+ There are other sorts of predicate types, used for the type families
+ extension, which we will not discuss here.
+
+ A predicate type is introduced by a lambda abstraction. Unlike with
+ the forall type, this is a value lambda abstraction, that must be
+ applied to a value. We call this value a \emph{dictionary}.
+
+ Without going into the implementation details, a dictionary can be
+ seen as a lookup table all the methods for a given (single) type class
+ instance. This means that all the dictionaries for the same type class
+ look the same (\eg\ contain methods with the same names). However,
+ dictionaries for different instances of the same class contain
+ different methods, of course.
+
+ A dictionary is introduced by \small{GHC} whenever it encounters an
+ instance declaration. This dictionary, as well as the binder
+ introduced by a lambda that introduces a dictionary, have the
+ predicate type as their type. These binders are usually named starting
+ with a \lam{\$}. Usually the name of the type concerned is not
+ reflected in the name of the dictionary, but the name of the type
+ class is. The Haskell expression \hs{show True} thus becomes:
+
+ \startlambda
+ show @Bool \$dShow True
+ \stoplambda
+ \stopdesc
+
+ Using this set of types, all types in basic Haskell can be represented.
+
+ \todo{Overview of polymorphism with more examples (or move examples
+ here)}.
+
+ \section[sec:prototype:statetype]{State annotations in Haskell}
+ As noted in \in{section}[sec:description:stateann], Cλash needs some
+ way to let the programmer explicitly specify which of a function's
+ arguments and which part of a function's result represent the
+ function's state.
+
+ Using the Haskell type systems, there are a few ways we can tackle this.
+
+ \subsection{Type synonyms}
+ Haskell provides type synonyms as a way to declare a new type that is
+ equal to an existing type (or rather, a new name for an existing type).
+ This allows both the original type and the synonym to be used
+ interchangedly in a Haskell program. This means no explicit conversion
+ is needed either. For example, a simple accumulator would become:
+
+ \starthaskell
+ type State s = s
+ acc :: Word -> State Word -> (State Word, Word)
+ acc i s = let sum = s + i in (sum, sum)
+ \stophaskell
+
+ This looks nice in Haskell, but turns out to be hard to implement. There
+ are no explicit conversion in Haskell, but not in Core either. This
+ means the type of a value might be show as \hs{AccState} in some places,
+ but \hs{Word} in others (and this can even change due to
+ transformations). Since every binder has an explicit type associated
+ with it, the type of every function type will be properly preserved and
+ could be used to track down the statefulness of each value by the
+ compiler. However, this makes the implementation a lot more complicated
+ than it currently is using \hs{newtypes}.
+
+ % Use \type instead of \hs here, since the latter breaks inside
+ % section headings.
+ \subsection{Type renaming (\type{newtype})}
+ Haskell also supports type renamings as a way to declare a new type that
+ has the same (runtime) representation as an existing type (but is in
+ fact a different type to the typechecker). With type renaming, an
+ explicit conversion between values of the two types is needed. The
+ accumulator would then become:
+
+ \starthaskell
+ newtype State s = State s
+ acc :: Word -> State Word -> (State Word, Word)
+ acc i (State s) = let sum = s + i in (State sum, sum)
+ \stophaskell
+
+ The \hs{newtype} line declares a new type \hs{State} that has one type
+ argument, \hs{s}. This type contains one \quote{constructor} \hs{State}
+ with a single argument of type \hs{s}. It is customary to name the
+ constructor the same as the type, which is allowed (since types can
+ never cause name collisions with values). The difference with the type
+ synonym example is in the explicit conversion between the \hs{State
+ Word} and \hs{Word} types by pattern matching and by using the explicit
+ the \hs{State constructor}.
+
+ This explicit conversion makes the \VHDL\ generation easier: whenever we
+ remove (unpack) the \hs{State} type, this means we are accessing the
+ current state (\eg, accessing the register output). Whenever we are a
+ adding (packing) the \hs{State} type, we are producing a new value for
+ the state (\eg, providing the register input).
+
+ When dealing with nested states (a stateful function that calls stateful
+ functions, which might call stateful functions, etc.) the state type
+ could quickly grow complex because of all the \hs{State} type constructors
+ needed. For example, consider the following state type (this is just the
+ state type, not the entire function type):
+
+ \starttyping
+ State (State Bit, State (State Word, Bit), Word)
+ \stoptyping
+
+ We cannot leave all these \hs{State} type constructors out, since that
+ would change the type (unlike when using type synonyms). However, when
+ using type synonyms to hide away substates (see
+ \in{section}[sec:prototype:substatesynonyms] below), this
+ disadvantage should be limited.
+
+ \subsubsection{Different input and output types}
+ An alternative could be to use different types for input and output
+ state (\ie\ current and updated state). The accumulator example would
+ then become something like:
+
+ \starthaskell
+ newtype StateIn s = StateIn s
+ newtype StateOut s = StateOut s
+ acc :: Word -> StateIn Word -> (StateIn Word, Word)
+ acc i (StateIn s) = let sum = s + i in (StateIn sum, sum)
+ \stophaskell
+
+ This could make the implementation easier and the hardware
+ descriptions less errorprone (you can no longer \quote{forget} to
+ unpack and repack a state variable and just return it directly, which
+ can be a problem in the current prototype). However, it also means we
+ need twice as many type synonyms to hide away substates, making this
+ approach a bit cumbersome. It also makes it harder to copmare input
+ and output state types, possible reducing the type safety of the
+ descriptions.
+
+ \subsection[sec:prototype:substatesynonyms]{Type synonyms for substates}
+ As noted above, when using nested (hierarchical) states, the state types
+ of the \quote{upper} functions (those that call other functions, which
+ call other functions, etc.) quickly becomes complicated. Also, when the
+ state type of one of the \quote{lower} functions changes, the state
+ types of all the upper functions changes as well. If the state type for
+ each function is explicitly and completely specified, this means that a
+ lot of code needs updating whenever a state type changes.
+
+ To prevent this, it is recommended (but not enforced) to use a type
+ synonym for the state type of every function. Every function calling
+ other functions will then use the state type synonym of the called
+ functions in its own type, requiring no code changes when the state type
+ of a called function changes. This approach is used in
+ \in{example}[ex:AvgState] below. The \hs{AccState} and \hs{AvgState}
+ are examples of such state type synonyms.
+
+ \subsection{Chosen approach}
+ To keep implementation simple, the current prototype uses the type
+ renaming approach, with a single type for both input and output
+ states. In the future, it might be worthwhile to revisit this
+ approach if more complicated flow analysis is implemented for
+ state variables. This analysis is needed to add proper error
+ checking anyway and might allow the use of type synonyms without
+ losing any expressivity.
+
+ \subsubsection{Example}
+ As an example of the used approach, there is a simple averaging circuit in
+ \in{example}[ex:AvgState]. This circuit lets the accumulation of the
+ inputs be done by a subcomponent, \hs{acc}, but keeps a count of value
+ accumulated in its own state.\footnote{Currently, the prototype
+ is not able to compile this example, since the built-in function
+ for division has not been added.}
+
+ \startbuffer[AvgState]
+ -- The state type annotation
+ newtype State s = State s
+
+ -- The accumulator state type
+ type AccState = State Word
+ -- The accumulator
+ acc :: Word -> AccState -> (AccState, Word)
+ acc i (State s) = let sum = s + i in (State sum, sum)
+
+ -- The averaging circuit state type
+ type AvgState = State (AccState, Word)
+ -- The averaging circuit
+ avg :: Word -> AvgState -> (AvgState, Word)
+ avg i (State s) = (State s', o)
+ where
+ (accs, count) = s
+ -- Pass our input through the accumulator, which outputs a sum
+ (accs', sum) = acc i accs
+ -- Increment the count (which will be our new state)
+ count' = count + 1
+ -- Compute the average
+ o = sum / count'
+ s' = (accs', count')
+ \stopbuffer
+
+ \placeexample[here][ex:AvgState]{Simple stateful averaging circuit.}
+ %\startcombination[2*1]
+ {\typebufferhs{AvgState}}%{Haskell description using function applications.}
+ % {\boxedgraphic{AvgState}}{The architecture described by the Haskell description.}
+ %\stopcombination
+ \todo{Picture}
+
+ \section{Implementing state}
+ Now its clear how to put state annotations in the Haskell source,
+ there is the question of how to implement this state translation. As
+ we have seen in \in{section}[sec:prototype:design], the translation to
+ \VHDL\ happens as a simple, final step in the compilation process.
+ This step works on a core expression in normal form. The specifics
+ of normal form will be explained in
+ \in{chapter}[chap:normalization], but the examples given should be
+ easy to understand using the definitin of Core given above.
+
+ \startbuffer[AvgStateNormal]
+ acc = λi.λspacked.
+ let
+ -- Remove the State newtype
+ s = spacked ▶ Word
+ s' = s + i
+ o = s + i
+ -- Add the State newtype again
+ spacked' = s' ▶ State Word
+ res = (spacked', o)
+ in
+ res
+
+ avg = λi.λspacked.
+ let
+ s = spacked ▶ (AccState, Word)
+ accs = case s of (accs, _) -> accs
+ count = case s of (_, count) -> count
+ accres = acc i accs
+ accs' = case accres of (accs', _) -> accs'
+ sum = case accres of (_, sum) -> sum
+ count' = count + 1
+ o = sum / count'
+ s' = (accs', count')
+ spacked' = s' ▶ State (AccState, Word)
+ res = (spacked', o)
+ in
+ res
+ \stopbuffer
+
+ \placeexample[here][ex:AvgStateNormal]{Normalized version of \in{example}[ex:AvgState]}
+ {\typebufferlam{AvgStateNormal}}
+
+ \subsection[sec:prototype:statelimits]{State in normal form}
+ Before describing how to translate state from normal form to
+ \VHDL, we will first see how state handling looks in normal form.
+ What limitations are there on their use to guarantee that proper
+ \VHDL\ can be generated?
+
+ We will try to formulate a number of rules about what operations are
+ allowed with state variables. These rules apply to the normalized Core
+ representation, but will in practice apply to the original Haskell
+ hardware description as well. Ideally, these rules would become part
+ of the intended normal form definition \refdef{intended normal form
+ definition}, but this is not the case right now. This can cause some
+ problems, which are detailed in
+ \in{section}[sec:normalization:stateproblems].
+
+ In these rules we use the terms \emph{state variable} to refer to any
+ variable that has a \lam{State} type. A \emph{state-containing
+ variable} is any variable whose type contains a \lam{State} type,
+ but is not one itself (like \lam{(AccState, Word)} in the example,
+ which is a tuple type, but contains \lam{AccState}, which is again
+ equal to \lam{State Word}).
+
+ We also use a distinction between \emph{input} and \emph{output
+ (state) variables} and \emph{substate variables}, which will be
+ defined in the rules themselves.
+
+ \startdesc{State variables can appear as an argument.}
+ \startlambda
+ avg = λi.λspacked. ...
+ \stoplambda
+
+ Any lambda that binds a variable with a state type, creates a new
+ input state variable.
+ \stopdesc
+
+ \startdesc{Input state variables can be unpacked.}
+ \startlambda
+ s = spacked ▶ (AccState, Word)
+ \stoplambda
+
+ An input state variable may be unpacked using a cast operation. This
+ removes the \lam{State} type renaming and the result has no longer a
+ \lam{State} type.
+
+ If the result of this unpacking does not have a state type and does
+ not contain state variables, there are no limitations on its use.
+ Otherwise if it does not have a state type but does contain
+ substates, we refer to it as a \emph{state-containing input
+ variable} and the limitations below apply. If it has a state type
+ itself, we refer to it as an \emph{input substate variable} and the
+ below limitations apply as well.
+
+ It may seem strange to consider a variable that still has a state
+ type directly after unpacking, but consider the case where a
+ function does not have any state of its own, but does call a single
+ stateful function. This means it must have a state argument that
+ contains just a substate. The function signature of such a function
+ could look like:
+
+ \starthaskell
+ type FooState = State AccState
+ \stophaskell
+
+ Which is of course equivalent to \lam{State (State Word)}.
+ \stopdesc
+
+ \startdesc{Variables can be extracted from state-containing input variables.}
+ \startlambda
+ accs = case s of (accs, _) -> accs
+ \stoplambda
+
+ A state-containing input variable is typically a tuple containing
+ multiple elements (like the current function's state, substates or
+ more tuples containing substates). All of these can be extracted
+ from an input variable using an extractor case (or possibly
+ multiple, when the input variable is nested).
+
+ If the result has no state type and does not contain any state
+ variables either, there are no further limitations on its use. If
+ the result has no state type but does contain state variables we
+ refer to it as a \emph{state-containing input variable} and this
+ limitation keeps applying. If the variable has a state type itself,
+ we refer to it as an \emph{input substate variable} and below
+ limitations apply.
+
+ \startdesc{Input substate variables can be passed to functions.}
+ \startlambda
+ accres = acc i accs
+ accs' = case accres of (accs', _) -> accs'
+ \stoplambda
+
+ An input substate variable can (only) be passed to a function.
+ Additionally, every input substate variable must be used in exactly
+ \emph{one} application, no more and no less.
+
+ The function result should contain exactly one state variable, which
+ can be extracted using (multiple) case expressions. The extracted
+ state variable is referred to the \emph{output substate}
+
+ The type of this output substate must be identical to the type of
+ the input substate passed to the function.
+ \stopdesc
+
+ \startdesc{Variables can be inserted into a state-containing output variable.}
+ \startlambda
+ s' = (accs', count')
+ \stoplambda
+
+ A function's output state is usually a tuple containing its own
+ updated state variables and all output substates. This result is
+ built up using any single-constructor algebraic datatype.
+
+ The result of these expressions is referred to as a
+ \emph{state-containing output variable}, which are subject to these
+ limitations.
+ \stopdesc
+
+ \startdesc{State containing output variables can be packed.}
+ \startlambda
+ spacked' = s' ▶ State (AccState, Word)
+ \stoplambda
+
+ As soon as all a functions own update state and output substate
+ variables have been joined together, the resulting
+ state-containing output variable can be packed into an output
+ state variable. Packing is done by casting into a state type.
+ \stopdesc
+
+ \startdesc{Output state variables can appear as (part of) a function result.}
+ \startlambda
+ avg = λi.λspacked.
+ let
+ \vdots
+ res = (spacked', o)
+ in
+ res
+ \stoplambda
+ When the output state is packed, it can be returned as a part
+ of the function result. Nothing else can be done with this
+ value (or any value that contains it).
+ \stopdesc
+
+ There is one final limitation that is hard to express in the above
+ itemization. Whenever substates are extracted from the input state
+ to be passed to functions, the corresponding output substates
+ should be inserted into the output state in the same way. In other
+ words, each pair of corresponding substates in the input and
+ output states should be passed / returned from the same called
+ function.
+
+ The prototype currently does not check much of the above
+ conditions. This means that if the conditions are violated,
+ sometimes a compile error is generated, but in other cases output
+ can be generated that is not valid \VHDL\ or at the very least does
+ not correspond to the input.
+
+ \subsection{Translating to \VHDL}
+ As noted above, the basic approach when generating \VHDL\ for stateful
+ functions is to generate a single register for every stateful function.
+ We look around the normal form to find the let binding that removes the
+ \lam{State} newtype (using a cast). We also find the let binding that
+ adds a \lam{State} type. These are connected to the output and the input
+ of the generated let binding respectively. This means that there can
+ only be one let binding that adds and one that removes the \lam{State}
+ type. It is easy to violate this constraint. This problem is detailed in
+ \in{section}[sec:normalization:stateproblems].
+
+ This approach seems simple enough, but will this also work for more
+ complex stateful functions involving substates? Observe that any
+ component of a function's state that is a substate, \ie\ passed on as
+ the state of another function, should have no influence on the
+ hardware generated for the calling function. Any state-specific
+ \small{VHDL} for this component can be generated entirely within the
+ called function. So, we can completely ignore substates when
+ generating \VHDL\ for a function.
+
+ From this observation it might seem logical to remove the
+ substates from a function's states altogether and leave only the
+ state components which are actual states of the current function.
+ While doing this would not remove any information needed to
+ generate \small{VHDL} from the function, it would cause the
+ function definition to become invalid (since we will not have any
+ substate to pass to the functions anymore). We could solve the
+ syntactic problems by passing \type{undefined} for state
+ variables, but that would still break the code on the semantic
+ level (\ie, the function would no longer be semantically
+ equivalent to the original input).
+
+ To keep the function definition correct until the very end of the
+ process, we will not deal with (sub)states until we get to the
+ \small{VHDL} generation. Then, we are translating from Core to
+ \small{VHDL}, and we can simply ignore substates, effectively removing
+ the substate components altogether.
+
+ But, how will we know what exactly is a substate? Since any state
+ argument or return value that represents state must be of the
+ \type{State} type, we can look at the type of a value. However, we
+ must be careful to ignore only \emph{substates}, and not a
+ function's own state.
+
+ In \in{example}[ex:AvgStateNorm] above, we should generate a register
+ connected with its output connected to \lam{s} and its input connected
+ to \lam{s'}. However, \lam{s'} is build up from both \lam{accs'} and
+ \lam{count'}, while only \lam{count'} should end up in the register.
+ \lam{accs'} is a substate for the \lam{acc} function, for which a
+ register will be created when generating \VHDL\ for the \lam{acc}
+ function.
+
+ Fortunately, the \lam{accs'} variable (and any other substate) has a
+ property that we can easily check: it has a \lam{State} type
+ annotation. This means that whenever \VHDL\ is generated for a tuple
+ (or other algebraic type), we can simply leave out all elements that
+ have a \lam{State} type. This will leave just the parts of the state
+ that do not have a \lam{State} type themselves, like \lam{count'},
+ which is exactly a function's own state. This approach also means that
+ the state part of the result is automatically excluded when generating
+ the output port, which is also required.
+
+ We can formalize this translation a bit, using the following
+ rules.
+
+ \startitemize
+ \item A state unpack operation should not generate any \small{VHDL}.
+ The binder to which the unpacked state is bound should still be
+ declared, this signal will become the register and will hold the
+ current state.
+ \item A state pack operation should not generate any \small{VHDL}.
+ The binder to which the packed state is bound should not be
+ declared. The binder that is packed is the signal that will hold the
+ new state.
+ \item Any values of a State type should not be translated to
+ \small{VHDL}. In particular, State elements should be removed from
+ tuples (and other datatypes) and arguments with a state type should
+ not generate ports.
+ \item To make the state actually work, a simple \small{VHDL}
+ (sequential) process should be generated. This process updates
+ the state at every clockcycle, by assigning the new state to the
+ current state. This will be recognized by synthesis tools as a
+ register specification.
+ \stopitemize
+
+ When applying these rules to the description in
+ \in{example}[ex:AvgStateNormal], we be left with the description
+ in \in{example}[ex:AvgStateRemoved]. All the parts that do not
+ generate any \VHDL\ directly are crossed out, leaving just the
+ actual flow of values in the final hardware.
+
+ \startlambda
+ avg = iλ.λ--spacked.--
+ let
+ s = --spacked ▶ (AccState, Word)--
+ --accs = case s of (accs, _) -> accs--
+ count = case s of (--_,-- count) -> count
+ accres = acc i --accs--
+ --accs' = case accres of (accs', _) -> accs'--
+ sum = case accres of (--_,-- sum) -> sum
+ count' = count + 1
+ o = sum / count'
+ s' = (--accs',-- count')
+ --spacked' = s' ▶ State (AccState, Word)--
+ res = (--spacked',-- o)
+ in
+ res
+ \stoplambda
+
+ When we would really leave out the crossed out parts, we get a slightly
+ weird program: there is a variable \lam{s} which has no value, and there
+ is a variable \lam{s'} that is never used. Together, these two will form
+ the state process of the function. \lam{s} contains the "current" state,
+ \lam{s'} is assigned the "next" state. So, at the end of each clock
+ cycle, \lam{s'} should be assigned to \lam{s}.
+
+ In the example the definition of \lam{s'} is still present, since
+ it does not have a state type. The \lam{accums'} substate has been
+ removed, leaving us just with the state of \lam{avg} itself.
+
+ As an illustration of the result of this function,
+ \in{example}[ex:AccStateVHDL] and \in{example}[ex:AvgStateVHDL] show the the \VHDL\ that is
+ generated from the examples is this section.
+
+ \startbuffer[AvgStateVHDL]
+ entity avgComponent_0 is
+ port (\izAlE2\ : in \unsigned_31\;
+ \foozAo1zAo12\ : out \(,)unsigned_31\;
+ clock : in std_logic;
+ resetn : in std_logic);
+ end entity avgComponent_0;
+
+
+ architecture structural of avgComponent_0 is
+ signal \szAlG2\ : \(,)unsigned_31\;
+ signal \countzAlW2\ : \unsigned_31\;
+ signal \dszAm62\ : \(,)unsigned_31\;
+ signal \sumzAmk3\ : \unsigned_31\;
+ signal \reszAnCzAnM2\ : \unsigned_31\;
+ signal \foozAnZzAnZ2\ : \unsigned_31\;
+ signal \reszAnfzAnj3\ : \unsigned_31\;
+ signal \s'zAmC2\ : \(,)unsigned_31\;
+ begin
+ \countzAlW2\ <= \szAlG2\.A;
+
+ \comp_ins_dszAm62\ : entity accComponent_1
+ port map (\izAob3\ => \izAlE2\,
+ \foozAoBzAoB2\ => \dszAm62\,
+ clock => clock,
+ resetn => resetn);
+
+ \sumzAmk3\ <= \dszAm62\.A;
+
+ \reszAnCzAnM2\ <= to_unsigned(1, 32);
+
+ \foozAnZzAnZ2\ <= \countzAlW2\ + \reszAnCzAnM2\;
+
+ \reszAnfzAnj3\ <= \sumzAmk3\ * \foozAnZzAnZ2\;
+
+ \s'zAmC2\.A <= \foozAnZzAnZ2\;
+
+ \foozAo1zAo12\.A <= \reszAnfzAnj3\;
+
+ state : process (clock, resetn)
+ begin
+ if resetn = '0' then
+ elseif rising_edge(clock) then
+ \szAlG2\ <= \s'zAmC2\;
+ end if;
+ end process state;
+ end architecture structural;
+ \stopbuffer
+ \startbuffer[AccStateVHDL]
+ entity accComponent_1 is
+ port (\izAob3\ : in \unsigned_31\;
+ \foozAoBzAoB2\ : out \(,)unsigned_31\;
+ clock : in std_logic;
+ resetn : in std_logic);
+ end entity accComponent_1;
+
+
+ architecture structural of accComponent_1 is
+ signal \szAod3\ : \unsigned_31\;
+ signal \reszAonzAor3\ : \unsigned_31\;
+ begin
+ \reszAonzAor3\ <= \szAod3\ + \izAob3\;
+
+ \foozAoBzAoB2\.A <= \reszAonzAor3\;
+
+ state : process (clock, resetn)
+ begin
+ if resetn = '0' then
+ elseif rising_edge(clock) then
+ \szAod3\ <= \reszAonzAor3\;
+ end if;
+ end process state;
+ end architecture structural;
+ \stopbuffer
+
+ \placeexample[][ex:AccStateVHDL]{\VHDL\ generated for acc from \in{example}[ex:AvgState]}
+ {\typebuffer[AccStateVHDL]}
+ \placeexample[][ex:AvgStateVHDL]{\VHDL\ generated for avg from \in{example}[ex:AvgState]}
+ {\typebuffer[AvgStateVHDL]}
+% \subsection{Initial state}
+% How to specify the initial state? Cannot be done inside a hardware
+% function, since the initial state is its own state argument for the first
+% call (unless you add an explicit, synchronous reset port).
+%
+% External init state is natural for simulation.
+%
+% External init state works for hardware generation as well.
+%
+% Implementation issues: state splitting, linking input to output state,
+% checking usage constraints on state variables.
+%
+%
+% vim: set sw=2 sts=2 expandtab:
projects / matthijs / master-project / report.git / blobdiff