From: Matthijs Kooijman Date: Mon, 5 Oct 2009 12:17:07 +0000 (+0200) Subject: Restructure the introduction of the Normalization chapter. X-Git-Tag: final-thesis~222 X-Git-Url: https://git.stderr.nl/gitweb?a=commitdiff_plain;h=21c8a86147c874c29156d1859a670c3f7c6df7ee;p=matthijs%2Fmaster-project%2Freport.git Restructure the introduction of the Normalization chapter. It now builds up to the formal definition using smaller examples, which should make the chapter more easy to understand. --- diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 4b3a08c..f64f790 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -45,24 +45,58 @@ interpretation. TODO: Describe core properties not supported in VHDL, and describe how the 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. - -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. - -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. +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: + +\placedefinition{}{A program is in \emph{normal form} if none of the +transformations from this chapter apply.} + +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. + +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 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 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 @@ -104,19 +138,35 @@ alu = λa.λb.λc. ncline(add)(sum); \stopuseMPgraphic -\placeexample[ex:MulSum]{\small{ALU} described in normal form} +\placeexample[here][ex:MulSum]{Simple architecture consisting of an adder and a +subtractor.} \startcombination[2*1] - {\typebufferlam{MulSum}}{Description in normal form} - {\boxedgraphic{MulSum}}{Described architecture} + {\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 op of + res = case opcode of Low -> res1 High -> res2 in @@ -157,18 +207,28 @@ alu = λopcode.λa.λb. ncline(mux)(res) "posA(out)"; \stopuseMPgraphic -\placeexample[ex:AddSubAlu]{\small{ALU} described in normal form} +\placeexample[here][ex:AddSubAlu]{Simple \small{ALU} supporting two operations.} \startcombination[2*1] - {\typebufferlam{AddSubAlu}}{Description in normal form} - {\boxedgraphic{AddSubAlu}}{Described architecture} + {\typebufferlam{AddSubAlu}}{Core description in normal form.} + {\boxedgraphic{AddSubAlu}}{The architecture described by the normal form.} \stopcombination -\startlambda +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) + -- 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 @@ -180,22 +240,133 @@ alu = λopcode.λa.λb. 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 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. @@ -267,60 +438,6 @@ references a local variable, false when it references a global variable. \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.