+ 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. For example, a simple accumulator would become:
+
+ \starthaskell
+ -- This type synonym would become part of Cλash, it is shown here
+ -- just for clarity.
+ 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
+ is no explicit conversion in Haskell, but not in Core either. This
+ means the type of a value might be shown as \hs{State Word} 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 would make
+ the implementation a lot more complicated than when using type
+ renamings as described in the next section.
+
+ % 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,
+ explicit conversion between values of the two types is needed. The
+ accumulator would then become:
+
+ \starthaskell
+ -- This type renaming would become part of Cλash, it is shown here
+ -- just for clarity.
+ 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 (\ie, accessing the register output). Whenever we are
+ adding (packing) the \hs{State} type, we are producing a new value for
+ the state (\ie, 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):
+
+ \starthaskell
+ State (State Bit, State (State Word, Bit), Word)
+ \stophaskell
+
+ 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
+ -- These type renaminges would become part of Cλash, it is shown
+ -- here just for clarity.
+ 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 error-prone (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 compare 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 become 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, a simple averaging circuit
+ is shown 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 there is no built-in function for division.}
+
+ \startbuffer[AvgState]
+ -- This type renaming would become part of Cλash, it is shown
+ -- here just for clarity
+ 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{\VHDL\ generation for 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 definition of Core given above. The
+ conversion to and from the \hs{State} type is done using the cast
+ operator, \lam{▶}.
+
+ \startbuffer[AvgStateNormal]
+ acc = λi.λspacked.
+ let
+ -- Remove the State newtype
+ s = spacked ▶ Word
+ sum = s + i
+ -- Add the State newtype again
+ spacked' = sum ▶ State Word
+ res = (spacked', sum)
+ in
+ res
+
+ avg = λi.λspacked.
+ let
+ s = spacked ▶ (AccState, Word)
+ accs = case s of (a, b) -> a
+ count = case s of (c, d) -> d
+ accres = acc i accs
+ accs' = case accres of (e, f) -> e
+ sum = case accres of (g, h) -> h
+ 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.
+ How must their use be limited to guarantee that proper \VHDL\ can
+ be generated?
+
+ We will 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.
+
+ These rules describe everything that can be done with state
+ variables and state-containing variables. Everything else is
+ invalid. For every rule, the corresponding part of
+ \in{example}[ex:AvgStateNormal] is shown.
+
+ \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 (this is the function's own state). 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 (a, b) -> a
+ \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
+ (this is the function's own state). 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 (e, f) -> e
+ \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
+ (possibly nested).
+
+ 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 to 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 to / 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} type renaming (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 generate no \VHDL for substates,
+ effectively removing them 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.
+
+ For \in{example}[ex:AvgStateNormal] above, we should generate a register
+ 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. 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 (\eg\ \lam{s'} in \lam{res}) 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 function \lam{avg} from
+ \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. To illustrate the
+ change of the types of \lam{s} and \lam{s'}, their types are also
+ shown.
+
+ \startbuffer[AvgStateRemoved]
+ avg = iλ.λ--spacked.--
+ let
+ s :: (--AccState,-- Word)
+ s = --spacked ▶ (AccState, Word)--
+ --accs = case s of (a, b) -> a--
+ count = case s of (--c,-- d) -> d
+ accres = acc i --accs--
+ --accs' = case accres of (e, f) -> e--
+ sum = case accres of (--g,-- h) -> h
+ count' = count + 1
+ o = sum / count'
+ s' :: (--AccState,-- Word)
+ s' = (--accs',-- count')
+ --spacked' = s' ▶ State (AccState, Word)--
+ res = (--spacked',-- o)
+ in
+ res
+ \stopbuffer
+ \placeexample[here][ex:AvgStateRemoved]{Normalized version of \in{example}[ex:AvgState] with ignored parts crossed out}
+ {\typebufferlam{AvgStatRemoved}}
+
+ When we actually 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. But 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}.
+
+ 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 by Cλash 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[AvgStateTypes]
+ package types is
+ subtype \unsigned_31\ is unsigned (0 to 31);
+
+ type \(,)unsigned_31\ is record
+ A : \unsigned_31\;
+ end record;
+ end package types;
+ \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:AvgStateTypes]{\VHDL\ types generated for \hs{acc} and \hs{avg} from \in{example}[ex:AvgState]}
+ {\typebuffervhdl{AvgStateTypes}}
+ \placeexample[][ex:AccStateVHDL]{\VHDL\ generated for \hs{acc} from \in{example}[ex:AvgState]}
+ {\typebuffervhdl{AccStateVHDL}}
+ \placeexample[][ex:AvgStateVHDL]{\VHDL\ generated for \hs{avg} from \in{example}[ex:AvgState]}
+ {\typebuffervhdl{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: