Finalize section on state in prototype chapter.
[matthijs/master-project/report.git] / Chapters / Prototype.tex
index 794aa347b1ffc065688dc60f9f122dde642b0bee..3be5e3a64dc664aa7c40b6d2c09c5e50408c93e9 100644 (file)
@@ -98,7 +98,7 @@
     switch to \small{EDIF} in the future, with minimal changes to the
     prototype.
 
-  \section{Prototype design}
+  \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. It's
       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}.
-    \subsection{Type renaming (\hs{newtype})}
+
+    % 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
 
       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, \todo{see below} this
+      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}
         and output state types, possible reducing the type safety of the
         descriptions.
 
-    \subsection{Type synonyms for substates}
+    \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
 
     \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.
-      \todo{}
+      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.
-        
+        accumulated in its own state.\footnote{Currently, the prototype
+        is not able to compile this example, since the builtin 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 Bit
+          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 = (AccState, Word)
+          type AvgState = State (AccState, Word)
           -- The averaging circuit
           avg :: Word -> AvgState -> (AvgState, Word)
           avg i (State s) = (State s', o)
           %\stopcombination
         \todo{Picture}
 
-        And the normalized, core-like versions:
+  \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've 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.
 
         \placeexample[here][ex:AvgStateNormal]{Normalized version of \in{example}[ex:AvgState]}
             {\typebufferlam{AvgStateNormal}}
-      
-      \subsection{What can you do with state?}
-        Now that we've seen how state variables are typically used, the
-        question rises of what can be done with these state variables exactly?
-        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 state variable to refer to any
-        variable that has a \lam{State} type. A 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 input and output (state) variables,
-        which will be defined in the rules themselves.
-
-        \startdesc{State variables can appear as an argument.}
-          \startlam
-            λspacked. ...
-          \stoplam
-
-          Any lambda that binds a variable with a state type, creates a new
-          input state variable.
-        \stopdesc
-
-        \startdesc{Input state variables can be unpacked.}
-          \startlam
-            s = spacked ▶ (AccState, Word)
-          \stoplam
-
-          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.}
-          \startlam
-            accs = case s of (accs, _) -> accs
-          \stoplam
-
-          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.} 
-          \startlam
-            accres = acc i accs
-            accs' = case accres of (accs', _) -> accs'
-          \stoplam
-          
-          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 statements. 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 state-containing output variables.}
-          \startlam
-            s' = (accs', count')
-          \stoplam
-          
-          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}
-          As soon as all a functions own update state and output substate
-          variables have been joined together, the va...
-          todo{}
-              spacked' = s' ▶ State (AccState, Word)
 
-        \desc{State variables can appear as (part of) a function result.} When
-        generating \small{VHDL}, we can completely ignore any part of a
-        function result that has a state type. If the entire result is a state
-        type, this will mean the entity will not have an output port.
-        Otherwise, the state elements will be removed from the type of the
-        output port.
-
-      \subsection{Translating to \VHDL}
-        \in{Example}[ex:AvgStateNormal] shows the normalized Core version of the
-        same description (note that _ is a wild binder). \refdef{wild binder}
-        The normal form is used to translated 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, we might think to remove the substates from a
-        function's states alltogether, 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 won't 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 alltogether.
-
-        There are a few important points when ignoring substates.
-
-        First, we have to have some definition of "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.
-
-
-
-
-
-
-
-
-
-
-        Now, we know how to handle each use of a state variable separately. If we
-        look at the whole, we can conclude the following:
-
-        \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} proc
-          should be generated. This proc 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 example program (in normal form), we will
-        get the following result. All the parts that don't generate any value are
-        crossed out, leaving some very boring assignments here and there.
-        
-      
+    \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
-          avg i --spacked-- = res
-            where
-              s = --case spacked of (State s) -> s--
-              --accums = case s of (accums, \_) -> accums--
-              count = case s of (--\_,-- count) -> count
-              accumres = accum i --accums--
-              --accums' = case accumres of (accums', \_) -> accums'--
-              sum = case accumres of (--\_,-- sum) -> sum
-              count' = count + 1
-              o = sum / count'
-              s' = (--accums',-- count')
-              --spacked' = State s'--
-              res = (--spacked',-- o)
+          type FooState = State AccState
         \stophaskell
-                
-        When we would really leave out the crossed out parts, we get a slightly
-        weird program: There is a variable \type{s} which has no value, and there
-        is a variable \type{s'} that is never used. Together, these two will form
-        the state proc of the function. \type{s} contains the "current" state,
-        \type{s'} is assigned the "next" state. So, at the end of each clock
-        cycle, \type{s'} should be assigned to \type{s}.
-
-        Note that the definition of \type{s'} is not removed, even though one
-        might think it as having a state type. Since the state type has a single
-        argument constructor \type{State}, some type that should be the resulting
-        state should always be explicitly packed with the State constructor,
-        allowing us to remove the packed version, but still generate \small{VHDL} for the
-        unpacked version (of course with any substates removed).
+
+        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
         
-        As you can see, the definition of \type{s'} is still present, since it
-        does not have a state type (The State constructor. The \type{accums'} substate has been removed,
-        leaving us just with the state of \type{avg} itself.
-    \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).
+        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.
 
-      External init state is natural for simulation.
+        The function result should contain exactly one state variable, which
+        can be extracted using (multiple) case statements. The extracted
+        state variable is referred to the \emph{output substate}
 
-      External init state works for hardware generation as well.
+        The type of this output substate must be identical to the type of
+        the input substate passed to the function.
+      \stopdesc
 
-      Implementation issues: state splitting, linking input to output state,
-      checking usage constraints on state variables.
+      \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
 
-      \todo{Implementation issues: Separate compilation, simplified core.}
+      \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, we might think to remove the substates from a
+      function's states alltogether, 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 won't 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 alltogether.
+
+      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} proc
+        should be generated. This proc 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 don't
+      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 proc 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}.
+
+      As you can see, 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.
+%
+%      \todo{Implementation issues: Separate compilation, simplified core.}
+%
 % vim: set sw=2 sts=2 expandtab: