%% \stopcombination
%}
-The first step in the core to VHDL translation process, is normalization. We
+The first step in the core to \small{VHDL} translation process, is normalization. We
aim to bring the core description into a simpler form, which we can
-subsequently translate into VHDL easily. This normal form is needed because
-the full core language is more expressive than VHDL in some areas and because
+subsequently translate into \small{VHDL} easily. This normal form is needed because
+the full core language is more expressive than \small{VHDL} in some areas and because
core can describe expressions that do not have a direct hardware
interpretation.
-TODO: Describe core properties not supported in VHDL, and describe how the
-VHDL we want to generate should look like.
+TODO: Describe core properties not supported in \small{VHDL}, and describe how the
+\small{VHDL} we want to generate should look like.
-\section{Goal}
+\section{Normal form}
The transformations described here have a well-defined goal: To bring the
program in a well-defined form that is directly translatable to hardware,
-while fully preserving the semantics of the program.
+while fully preserving the semantics of the program. We refer to this form as
+the \emph{normal form} of the program. The formal definition of this normal
+form is quite simple:
-This {\em normal form} is again a Core program, but with a very specific
-structure. A function in normal form has nested lambda's at the top, which
-produce a number of nested let expressions. These let expressions binds a
-number of simple expressions in the function and produces a simple identifier.
-Every bound value in the let expression is either a simple function
-application, a case expression to extract a single element from a tuple
-returned by a function or a case expression to choose between two signals
-based on some other signal.
+\placedefinition{}{A program is in \emph{normal form} if none of the
+transformations from this chapter apply.}
-This structure is easy to translate to VHDL, since each top level lambda will
-be an input port, every bound value will become a concurrent statement (such
-as a component instantiation or conditional signal assignment) and the result
-variable will become the output port.
+Of course, this is an \quote{easy} definition of the normal form, since our
+program will end up in normal form automatically. The more interesting part is
+to see if this normal form actually has the properties we would like it to
+have.
-An example of a program in canonical form would be:
+But, before getting into more definitions and details about this normal form,
+let's try to get a feeling for it first. The easiest way to do this is by
+describing the things we want to not have in a normal form.
+
+\startitemize
+ \item Any \emph{polymorphism} must be removed. When laying down hardware, we
+ can't generate any signals that can have multiple types. All types must be
+ completely known to generate hardware.
+
+ \item Any \emph{higher order} constructions must be removed. We can't
+ generate a hardware signal that contains a function, so all values,
+ arguments and returns values used must be first order.
+
+ \item Any complex \emph{nested scopes} must be removed. In the \small{VHDL}
+ description, every signal is in a single scope. Also, full expressions are
+ not supported everywhere (in particular port maps can only map signal names,
+ not expressions). To make the \small{VHDL} generation easy, all values must be bound
+ on the \quote{top level}.
+\stopitemize
+
+TODO: Intermezzo: functions vs plain values
+
+A very simple example of a program in normal form is given in
+\in{example}[ex:MulSum]. As you can see, all arguments to the function (which
+will become input ports in the final hardware) are at the top. This means that
+the body of the final lambda abstraction is never a function, but always a
+plain value.
+
+After the lambda abstractions, we see a single let expression, that binds two
+variables (\lam{mul} and \lam{sum}). These variables will be signals in the
+final hardware, bound to the output port of the \lam{*} and \lam{+}
+components.
+
+The final line (the \quote{return value} of the function) selects the
+\lam{sum} signal to be the output port of the function. This \quote{return
+value} can always only be a variable reference, never a more complex
+expression.
+
+\startbuffer[MulSum]
+alu :: Bit -> Word -> Word -> Word
+alu = λa.λb.λc.
+ let
+ mul = (*) a b
+ sum = (+) mul c
+ in
+ sum
+\stopbuffer
+
+\startuseMPgraphic{MulSum}
+ save a, b, c, mul, add, sum;
+
+ % I/O ports
+ newCircle.a(btex $a$ etex) "framed(false)";
+ newCircle.b(btex $b$ etex) "framed(false)";
+ newCircle.c(btex $c$ etex) "framed(false)";
+ newCircle.sum(btex $res$ etex) "framed(false)";
+
+ % Components
+ newCircle.mul(btex - etex);
+ newCircle.add(btex + etex);
+
+ a.c - b.c = (0cm, 2cm);
+ b.c - c.c = (0cm, 2cm);
+ add.c = c.c + (2cm, 0cm);
+ mul.c = midpoint(a.c, b.c) + (2cm, 0cm);
+ sum.c = add.c + (2cm, 0cm);
+ c.c = origin;
+
+ % Draw objects and lines
+ drawObj(a, b, c, mul, add, sum);
+
+ ncarc(a)(mul) "arcangle(15)";
+ ncarc(b)(mul) "arcangle(-15)";
+ ncline(c)(add);
+ ncline(mul)(add);
+ ncline(add)(sum);
+\stopuseMPgraphic
+
+\placeexample[here][ex:MulSum]{Simple architecture consisting of an adder and a
+subtractor.}
+ \startcombination[2*1]
+ {\typebufferlam{MulSum}}{Core description in normal form.}
+ {\boxedgraphic{MulSum}}{The architecture described by the normal form.}
+ \stopcombination
+
+The previous example described composing an architecture by calling other
+functions (operators), resulting in a simple architecture with component and
+connection. There is of course also some mechanism for choice in the normal
+form. In a normal Core program, the \emph{case} expression can be used in a
+few different ways to describe choice. In normal form, this is limited to a
+very specific form.
+
+\in{Example}[ex:AddSubAlu] shows an example describing a
+simple \small{ALU}, which chooses between two operations based on an opcode
+bit. The main structure is the same as in \in{example}[ex:MulSum], but this
+time the \lam{res} variable is bound to a case expression. This case
+expression scrutinizes the variable \lam{opcode} (and scrutinizing more
+complex expressions is not supported). The case expression can select a
+different variable based on the constructor of \lam{opcode}.
+
+\startbuffer[AddSubAlu]
+alu :: Bit -> Word -> Word -> Word
+alu = λopcode.λa.λb.
+ let
+ res1 = (+) a b
+ res2 = (-) a b
+ res = case opcode of
+ Low -> res1
+ High -> res2
+ in
+ res
+\stopbuffer
+
+\startuseMPgraphic{AddSubAlu}
+ save opcode, a, b, add, sub, mux, res;
+
+ % I/O ports
+ newCircle.opcode(btex $opcode$ etex) "framed(false)";
+ newCircle.a(btex $a$ etex) "framed(false)";
+ newCircle.b(btex $b$ etex) "framed(false)";
+ newCircle.res(btex $res$ etex) "framed(false)";
+ % Components
+ newCircle.add(btex + etex);
+ newCircle.sub(btex - etex);
+ newMux.mux;
+
+ opcode.c - a.c = (0cm, 2cm);
+ add.c - a.c = (4cm, 0cm);
+ sub.c - b.c = (4cm, 0cm);
+ a.c - b.c = (0cm, 3cm);
+ mux.c = midpoint(add.c, sub.c) + (1.5cm, 0cm);
+ res.c - mux.c = (1.5cm, 0cm);
+ b.c = origin;
+
+ % Draw objects and lines
+ drawObj(opcode, a, b, res, add, sub, mux);
+
+ ncline(a)(add) "posA(e)";
+ ncline(b)(sub) "posA(e)";
+ nccurve(a)(sub) "posA(e)", "angleA(0)";
+ nccurve(b)(add) "posA(e)", "angleA(0)";
+ nccurve(add)(mux) "posB(inpa)", "angleB(0)";
+ nccurve(sub)(mux) "posB(inpb)", "angleB(0)";
+ nccurve(opcode)(mux) "posB(n)", "angleA(0)", "angleB(-90)";
+ ncline(mux)(res) "posA(out)";
+\stopuseMPgraphic
+
+\placeexample[here][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.}
+ \startcombination[2*1]
+ {\typebufferlam{AddSubAlu}}{Core description in normal form.}
+ {\boxedgraphic{AddSubAlu}}{The architecture described by the normal form.}
+ \stopcombination
+
+As a more complete example, consider \in{example}[ex:NormalComplete]. This
+example contains everything that is supported in normal form, with the
+exception of builtin higher order functions.
+
+\startbuffer[NormalComplete]
+ regbank :: Bit
+ -> Word
+ -> State (Word, Word)
+ -> (State (Word, Word), Word)
-\startlambda
-- All arguments are an inital lambda
- λa.λd.λsp.
+ regbank = λa.λd.λsp.
-- There are nested let expressions at top level
let
- -- Unpack the state by coercion
+ -- Unpack the state by coercion (\eg, cast from
+ -- State (Word, Word) to (Word, Word))
s = sp :: (Word, Word)
-- Extract both registers from the state
r1 = case s of (fst, snd) -> fst
High -> r1
Low -> r2
r1' = case a of
- High -> d
+ High -> d'
Low -> r1
r2' = case a of
High -> r2
- Low -> d
+ Low -> d'
-- Packing a tuple
s' = (,) r1' r2'
- -- Packing the state by coercion
+ -- pack the state by coercion (\eg, cast from
+ -- (Word, Word) to State (Word, Word))
sp' = s' :: State (Word, Word)
-- Pack our return value
res = (,) sp' out
in
-- The actual result
res
+\stopbuffer
+
+\startuseMPgraphic{NormalComplete}
+ save a, d, r, foo, muxr, muxout, out;
+
+ % I/O ports
+ newCircle.a(btex \lam{a} etex) "framed(false)";
+ newCircle.d(btex \lam{d} etex) "framed(false)";
+ newCircle.out(btex \lam{out} etex) "framed(false)";
+ % Components
+ %newCircle.add(btex + etex);
+ newBox.foo(btex \lam{foo} etex);
+ newReg.r1(btex $\lam{r1}$ etex) "dx(4mm)", "dy(6mm)";
+ newReg.r2(btex $\lam{r2}$ etex) "dx(4mm)", "dy(6mm)", "reflect(true)";
+ newMux.muxr1;
+ % Reflect over the vertical axis
+ reflectObj(muxr1)((0,0), (0,1));
+ newMux.muxr2;
+ newMux.muxout;
+ rotateObj(muxout)(-90);
+
+ d.c = foo.c + (0cm, 1.5cm);
+ a.c = (xpart r2.c + 2cm, ypart d.c - 0.5cm);
+ foo.c = midpoint(muxr1.c, muxr2.c) + (0cm, 2cm);
+ muxr1.c = r1.c + (0cm, 2cm);
+ muxr2.c = r2.c + (0cm, 2cm);
+ r2.c = r1.c + (4cm, 0cm);
+ r1.c = origin;
+ muxout.c = midpoint(r1.c, r2.c) - (0cm, 2cm);
+ out.c = muxout.c - (0cm, 1.5cm);
+
+% % Draw objects and lines
+ drawObj(a, d, foo, r1, r2, muxr1, muxr2, muxout, out);
+
+ ncline(d)(foo);
+ nccurve(foo)(muxr1) "angleA(-90)", "posB(inpa)", "angleB(180)";
+ nccurve(foo)(muxr2) "angleA(-90)", "posB(inpb)", "angleB(0)";
+ nccurve(muxr1)(r1) "posA(out)", "angleA(180)", "posB(d)", "angleB(0)";
+ nccurve(r1)(muxr1) "posA(out)", "angleA(0)", "posB(inpb)", "angleB(180)";
+ nccurve(muxr2)(r2) "posA(out)", "angleA(0)", "posB(d)", "angleB(180)";
+ nccurve(r2)(muxr2) "posA(out)", "angleA(180)", "posB(inpa)", "angleB(0)";
+ nccurve(r1)(muxout) "posA(out)", "angleA(0)", "posB(inpb)", "angleB(-90)";
+ nccurve(r2)(muxout) "posA(out)", "angleA(180)", "posB(inpa)", "angleB(-90)";
+ % Connect port a
+ nccurve(a)(muxout) "angleA(-90)", "angleB(180)", "posB(sel)";
+ nccurve(a)(muxr1) "angleA(180)", "angleB(-90)", "posB(sel)";
+ nccurve(a)(muxr2) "angleA(180)", "angleB(-90)", "posB(sel)";
+ ncline(muxout)(out) "posA(out)";
+\stopuseMPgraphic
+
+\placeexample[here][ex:NormalComplete]{Simple architecture consisting of an adder and a
+subtractor.}
+ \startcombination[2*1]
+ {\typebufferlam{NormalComplete}}{Core description in normal form.}
+ {\boxedgraphic{NormalComplete}}{The architecture described by the normal form.}
+ \stopcombination
+
+\subsection{Normal form definition}
+Now we have some intuition for the normal form, we can describe how we want
+the normal form to look like in a slightly more formal manner. The following
+EBNF-like description completely captures the intended structure (and
+generates a subset of GHC's core format).
+
+Some clauses have an expression listed in parentheses. These are conditions
+that need to apply to the clause.
+
+\startlambda
+\italic{normal} = \italic{lambda}
+\italic{lambda} = λvar.\italic{lambda} (representable(var))
+ | \italic{toplet}
+\italic{toplet} = let \italic{binding} in \italic{toplet}
+ | letrec [\italic{binding}] in \italic{toplet}
+ | var (representable(varvar))
+\italic{binding} = var = \italic{rhs} (representable(rhs))
+ -- State packing and unpacking by coercion
+ | var0 = var1 :: State ty (lvar(var1))
+ | var0 = var1 :: ty (var0 :: State ty) (lvar(var1))
+\italic{rhs} = userapp
+ | builtinapp
+ -- Extractor case
+ | case var of C a0 ... an -> ai (lvar(var))
+ -- Selector case
+ | case var of (lvar(var))
+ DEFAULT -> var0 (lvar(var0))
+ C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, lvar(resvar))
+\italic{userapp} = \italic{userfunc}
+ | \italic{userapp} {userarg}
+\italic{userfunc} = var (gvar(var))
+\italic{userarg} = var (lvar(var))
+\italic{builtinapp} = \italic{builtinfunc}
+ | \italic{builtinapp} \italic{builtinarg}
+\italic{builtinfunc} = var (bvar(var))
+\italic{builtinarg} = \italic{coreexpr}
\stoplambda
+-- TODO: Limit builtinarg further
+
+-- TODO: There can still be other casts around (which the code can handle,
+e.g., ignore), which still need to be documented here.
+
+-- TODO: Note about the selector case. It just supports Bit and Bool
+currently, perhaps it should be generalized in the normal form?
+
+When looking at such a program from a hardware perspective, the top level
+lambda's define the input ports. The value produced by the let expression is
+the output port. Most function applications bound by the let expression
+define a component instantiation, where the input and output ports are mapped
+to local signals or arguments. Some of the others use a builtin
+construction (\eg the \lam{case} statement) or call a builtin function
+(\eg \lam{add} or \lam{sub}). For these, a hardcoded \small{VHDL} translation is
+available.
+
\subsection{Definitions}
In the following sections, we will be using a number of functions and
notations, which we will define here.
\emph{representable(expr)} or \emph{representable(var)} is true when
\emph{expr} or \emph{var} has a type that is representable at runtime.
-\subsection{Normal form definition}
-We can describe this normal form in a slightly more formal manner. The
-following EBNF-like description completely captures the intended structure
-(and generates a subset of GHC's core format).
-
-Some clauses have an expression listed in parentheses. These are conditions
-that need to apply to the clause.
-
-\startlambda
-\italic{normal} = \italic{lambda}
-\italic{lambda} = λvar.\italic{lambda} (representable(var))
- | \italic{toplet}
-\italic{toplet} = let \italic{binding} in \italic{toplet}
- | letrec [\italic{binding}] in \italic{toplet}
- | var (representable(varvar))
-\italic{binding} = var = \italic{rhs} (representable(rhs))
- -- State packing and unpacking by coercion
- | var0 = var1 :: State ty (lvar(var1))
- | var0 = var1 :: ty (var0 :: State ty) (lvar(var1))
-\italic{rhs} = userapp
- | builtinapp
- -- Extractor case
- | case var of C a0 ... an -> ai (lvar(var))
- -- Selector case
- | case var of (lvar(var))
- DEFAULT -> var0 (lvar(var0))
- C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, lvar(resvar))
-\italic{userapp} = \italic{userfunc}
- | \italic{userapp} {userarg}
-\italic{userfunc} = var (gvar(var))
-\italic{userarg} = var (lvar(var))
-\italic{builtinapp} = \italic{builtinfunc}
- | \italic{builtinapp} \italic{builtinarg}
-\italic{builtinfunc} = var (bvar(var))
-\italic{builtinarg} = \italic{coreexpr}
-\stoplambda
-
--- TODO: Limit builtinarg further
-
--- TODO: There can still be other casts around (which the code can handle,
-e.g., ignore), which still need to be documented here.
-
--- TODO: Note about the selector case. It just supports Bit and Bool
-currently, perhaps it should be generalized in the normal form?
-
-When looking at such a program from a hardware perspective, the top level
-lambda's define the input ports. The value produced by the let expression is
-the output port. Most function applications bound by the let expression
-define a component instantiation, where the input and output ports are mapped
-to local signals or arguments. Some of the others use a builtin
-construction (\eg the \lam{case} statement) or call a builtin function
-(\eg \lam{add} or \lam{sub}). For these, a hardcoded VHDL translation is
-available.
-
\section{Transform passes}
In this section we describe the actual transforms. Here we're using
the core language in a notation that resembles lambda calculus.
Each of these transforms is meant to be applied to every (sub)expression
in a program, for as long as it applies. Only when none of the
-expressions can be applied anymore, the program is in normal form. We
-hope to be able to prove that this form will obey all of the constraints
-defined above, but this has yet to happen (though it seems likely that
-it will).
+transformations can be applied anymore, the program is in normal form (by
+definition). We hope to be able to prove that this form will obey all of the
+constraints defined above, but this has yet to happen (though it seems likely
+that it will).
Each of the transforms will be described informally first, explaining
the need for and goal of the transform. Then, a formal definition is
This transformation inlines simple let bindings (\eg a = b).
This transformation is not needed to get into normal form, but makes the
-resulting VHDL a lot shorter.
+resulting \small{VHDL} a lot shorter.
\starttrans
letnonrec
(since ununsed bindings are not forbidden by the normal form), but in practice
the desugarer or simplifier emits some unused bindings that cannot be
normalized (e.g., calls to a \type{PatError} (TODO: Check this name)). Also,
-this transformation makes the resulting VHDL a lot shorter.
+this transformation makes the resulting \small{VHDL} a lot shorter.
\starttrans
let a = E in M
When looking at the arguments of a user-defined function, we can
divide them into two categories:
\startitemize
- \item Arguments with a runtime representable type (\eg bits or vectors).
+ \item Arguments of a runtime representable type (\eg bits or vectors).
These arguments can be preserved in the program, since they can
be translated to input ports later on. However, since we can
These arguments cannot be preserved in the program, since we
cannot represent them as input or output ports in the resulting
- VHDL. To remove them, we create a specialized version of the
+ \small{VHDL}. To remove them, we create a specialized version of the
called function with these arguments filled in. This is done by
the argument propagation transform.
into categories:
\startitemize
- \item Arguments with a runtime representable type.
+ \item Arguments of a runtime representable type.
As we have seen with user-defined functions, these arguments can
always be reduced to a simple variable reference, by the
functions can be limited to signal references, instead of
needing to support all possible expressions.
- \item Arguments with a function type.
+ \item Arguments of a function type.
These arguments are functions passed to higher order builtins,
like \lam{map} and \lam{foldl}. Since implementing these
\subsubsection{Argument simplification}
This transform deals with arguments to functions that
are of a runtime representable type. It ensures that they will all become
-references to global variables, or local signals in the resulting VHDL.
+references to global variables, or local signals in the resulting \small{VHDL}.
TODO: It seems we can map an expression to a port, not only a signal.
Perhaps this makes this transformation not needed?
This transformation is useful when applying higher order builtin functions
like \hs{map} to a lambda abstraction, for example. In this case, the code
-that generates VHDL for \hs{map} only needs to handle top level functions and
+that generates \small{VHDL} for \hs{map} only needs to handle top level functions and
partial applications, not any other expression (such as lambda abstractions or
even more complicated expressions).
projects / matthijs / master-project / report.git / blobdiff