1 \chapter[chap:prototype]{Prototype}
2 An important step in this research is the creation of a prototype compiler.
3 Having this prototype allows us to apply the ideas from the previous chapter
4 to actual hardware descriptions and evaluate their usefulness. Having a
5 prototype also helps to find new techniques and test possible
8 Obviously the prototype was not created after all research
9 ideas were formed, but its implementation has been interleaved with the
10 research itself. Also, the prototype described here is the final version, it
11 has gone through a number of design iterations which we will not completely
14 \section[sec:prototype:input]{Input language}
15 When implementing this prototype, the first question to ask is: What
16 (functional) language will we use to describe our hardware? (Note that
17 this does not concern the \emph{implementation language} of the compiler,
18 just the language \emph{translated by} the compiler).
20 Initially, we have two choices:
23 \item Create a new functional language from scratch. This has the
24 advantage of having a language that contains exactly those elements that
25 are convenient for describing hardware and can contain special
26 constructs that allows our hardware descriptions to be more powerful or
28 \item Use an existing language and create a new backend for it. This has
29 the advantage that existing tools can be reused, which will speed up
35 \startframedtext[width=8cm,background=box,frame=no]
36 \startalignment[center]
37 {\tfa No \small{EDSL} or Template Haskell}
41 Note that in this consideration, embedded domain-specific
42 languages (\small{EDSL}) and Template Haskell (\small{TH})
43 approaches have not been included. As we've seen in
44 \in{section}[sec:context:fhdls], these approaches have all kinds
45 of limitations on the description language that we would like to
49 Considering that we required a prototype which should be working quickly,
50 and that implementing parsers, semantic checkers and especially
51 typcheckers is not exactly the core of this research (but it is lots and
52 lots of work!), using an existing language is the obvious choice. This
53 also has the advantage that a large set of language features is available
54 to experiment with and it is easy to find which features apply well and
55 which don't. A possible second prototype could use a custom language with
56 just the useful features (and possibly extra features that are specific to
57 the domain of hardware description as well).
59 The second choice is which of the many existing languages to use. As
60 mentioned before, the chosen language is Haskell. This choice has not been the
61 result of a thorough comparison of languages, for the simple reason that
62 the requirements on the language were completely unclear at the start of
63 this research. The fact that Haskell is a language with a broad spectrum
64 of features, that it is commonly used in research projects and that the
65 primary compiler, \GHC, provides a high level API to its internals, made
66 Haskell an obvious choice.
68 \section[sec:prototype:output]{Output format}
69 The second important question is: What will be our output format? Since
70 our prototype won't be able to program FPGA's directly, we'll have to have
71 output our hardware in some format that can be later processed and
72 programmed by other tools.
74 Looking at other tools in the industry, the Electronic Design Interchange
75 Format (\small{EDIF}) is commonly used for storing intermediate
76 \emph{netlists} (lists of components and connections between these
77 components) and is commonly the target for \small{VHDL} and Verilog
80 However, \small{EDIF} is not completely tool-independent. It specifies a
81 meta-format, but the hardware components that can be used vary between
82 various tool and hardware vendors, as well as the interpretation of the
83 \small{EDIF} standard. \todo{Is this still true? Reference:
84 http://delivery.acm.org/10.1145/80000/74534/p803-li.pdf?key1=74534\&key2=8370537521\&coll=GUIDE\&dl=GUIDE\&CFID=61207158\&CFTOKEN=61908473}
86 This means that when working with \small{EDIF}, our prototype would become
87 technology dependent (\eg only work with \small{FPGA}s of a specific
88 vendor, or even only with specific chips). This limits the applicability
89 of our prototype. Also, the tools we'd like to use for verifying,
90 simulating and draw pretty pictures of our output (like Precision, or
91 QuestaSim) are designed for \small{VHDL} or Verilog input.
93 For these reasons, we will not use \small{EDIF}, but \small{VHDL} as our
94 output language. We choose \VHDL over Verilog simply because we are
95 familiar with \small{VHDL} already. The differences between \small{VHDL}
96 and Verilog are on the higher level, while we will be using \small{VHDL}
97 mainly to write low level, netlist-like descriptions anyway.
99 An added advantage of using VHDL is that we can profit from existing
100 optimizations in VHDL synthesizers. A lot of optimizations are done on the
101 VHDL level by existing tools. These tools have years of experience in this
102 field, so it would not be reasonable to assume we could achieve a similar
103 amount of optimization in our prototype (nor should it be a goal,
104 considering this is just a prototype).
106 Note that we will be using \small{VHDL} as our output language, but will
107 not use its full expressive power. Our output will be limited to using
108 simple, structural descriptions, without any behavioural descriptions
109 (which might not be supported by all tools). This ensures that any tool
110 that works with \VHDL will understand our output (most tools don't support
111 synthesis of more complex \VHDL). This also leaves open the option to
112 switch to \small{EDIF} in the future, with minimal changes to the
115 \section[sec:prototype:design]{Prototype design}
116 As suggested above, we will use the Glasgow Haskell Compiler (\small{GHC}) to
117 implement our prototype compiler. To understand the design of the
118 compiler, we will first dive into the \small{GHC} compiler a bit. It's
119 compilation consists of the following steps (slightly simplified):
121 \startuseMPgraphic{ghc-pipeline}
123 save inp, front, desugar, simpl, back, out;
124 newEmptyBox.inp(0,0);
125 newBox.front(btex Fronted etex);
126 newBox.desugar(btex Desugarer etex);
127 newBox.simpl(btex Simplifier etex);
128 newBox.back(btex Backend etex);
129 newEmptyBox.out(0,0);
131 % Space the boxes evenly
132 inp.c - front.c = front.c - desugar.c = desugar.c - simpl.c
133 = simpl.c - back.c = back.c - out.c = (0, 1.5cm);
136 % Draw lines between the boxes. We make these lines "deferred" and give
137 % them a name, so we can use ObjLabel to draw a label beside them.
138 ncline.inp(inp)(front) "name(haskell)";
139 ncline.front(front)(desugar) "name(ast)";
140 ncline.desugar(desugar)(simpl) "name(core)";
141 ncline.simpl(simpl)(back) "name(simplcore)";
142 ncline.back(back)(out) "name(native)";
143 ObjLabel.inp(btex Haskell source etex) "labpathname(haskell)", "labdir(rt)";
144 ObjLabel.front(btex Haskell AST etex) "labpathname(ast)", "labdir(rt)";
145 ObjLabel.desugar(btex Core etex) "labpathname(core)", "labdir(rt)";
146 ObjLabel.simpl(btex Simplified core etex) "labpathname(simplcore)", "labdir(rt)";
147 ObjLabel.back(btex Native code etex) "labpathname(native)", "labdir(rt)";
149 % Draw the objects (and deferred labels)
150 drawObj (inp, front, desugar, simpl, back, out);
152 \placefigure[right]{GHC compiler pipeline}{\useMPgraphic{ghc-pipeline}}
155 This step takes the Haskell source files and parses them into an
156 abstract syntax tree (\small{AST}). This \small{AST} can express the
157 complete Haskell language and is thus a very complex one (in contrast
158 with the Core \small{AST}, later on). All identifiers in this
159 \small{AST} are resolved by the renamer and all types are checked by the
162 \startdesc{Desugaring}
163 This steps takes the full \small{AST} and translates it to the
164 \emph{Core} language. Core is a very small functional language with lazy
165 semantics, that can still express everything Haskell can express. Its
166 simpleness makes Core very suitable for further simplification and
167 translation. Core is the language we will be working with as well.
169 \startdesc{Simplification}
170 Through a number of simplification steps (such as inlining, common
171 subexpression elimination, etc.) the Core program is simplified to make
172 it faster or easier to process further.
175 This step takes the simplified Core program and generates an actual
176 runnable program for it. This is a big and complicated step we will not
177 discuss it any further, since it is not required for our prototype.
180 In this process, there a number of places where we can start our work.
181 Assuming that we don't want to deal with (or modify) parsing, typechecking
182 and other frontend business and that native code isn't really a useful
183 format anymore, we are left with the choice between the full Haskell
184 \small{AST}, or the smaller (simplified) core representation.
186 The advantage of taking the full \small{AST} is that the exact structure
187 of the source program is preserved. We can see exactly what the hardware
188 descriiption looks like and which syntax constructs were used. However,
189 the full \small{AST} is a very complicated datastructure. If we are to
190 handle everything it offers, we will quickly get a big compiler.
192 Using the core representation gives us a much more compact datastructure
193 (a core expression only uses 9 constructors). Note that this does not mean
194 that the core representation itself is smaller, on the contrary. Since the
195 core language has less constructs, a lot of things will take a larger
196 expression to express.
198 However, the fact that the core language is so much smaller, means it is a
199 lot easier to analyze and translate it into something else. For the same
200 reason, \small{GHC} runs its simplifications and optimizations on the core
201 representation as well.
203 However, we will use the normal core representation, not the simplified
204 core. Reasons for this are detailed below. \todo{Ref}
206 The final prototype roughly consists of three steps:
208 \startuseMPgraphic{clash-pipeline}
210 save inp, front, norm, vhdl, out;
211 newEmptyBox.inp(0,0);
212 newBox.front(btex \small{GHC} frontend + desugarer etex);
213 newBox.norm(btex Normalization etex);
214 newBox.vhdl(btex \small{VHDL} generation etex);
215 newEmptyBox.out(0,0);
217 % Space the boxes evenly
218 inp.c - front.c = front.c - norm.c = norm.c - vhdl.c
219 = vhdl.c - out.c = (0, 1.5cm);
222 % Draw lines between the boxes. We make these lines "deferred" and give
223 % them a name, so we can use ObjLabel to draw a label beside them.
224 ncline.inp(inp)(front) "name(haskell)";
225 ncline.front(front)(norm) "name(core)";
226 ncline.norm(norm)(vhdl) "name(normal)";
227 ncline.vhdl(vhdl)(out) "name(vhdl)";
228 ObjLabel.inp(btex Haskell source etex) "labpathname(haskell)", "labdir(rt)";
229 ObjLabel.front(btex Core etex) "labpathname(core)", "labdir(rt)";
230 ObjLabel.norm(btex Normalized core etex) "labpathname(normal)", "labdir(rt)";
231 ObjLabel.vhdl(btex \small{VHDL} description etex) "labpathname(vhdl)", "labdir(rt)";
233 % Draw the objects (and deferred labels)
234 drawObj (inp, front, norm, vhdl, out);
236 \placefigure[right]{Cλash compiler pipeline}{\useMPgraphic{clash-pipeline}}
239 This is exactly the frontend and desugarer from the \small{GHC}
240 pipeline, that translates Haskell sources to a core representation.
242 \startdesc{Normalization}
243 This is a step that transforms the core representation into a normal
244 form. This normal form is still expressed in the core language, but has
245 to adhere to an extra set of constraints. This normal form is less
246 expressive than the full core language (e.g., it can have limited higher
247 order expressions, has a specific structure, etc.), but is also very
248 close to directly describing hardware.
250 \startdesc{\small{VHDL} generation}
251 The last step takes the normal formed core representation and generates
252 \small{VHDL} for it. Since the normal form has a specific, hardware-like
253 structure, this final step is very straightforward.
256 The most interesting step in this process is the normalization step. That
257 is where more complicated functional constructs, which have no direct
258 hardware interpretation, are removed and translated into hardware
259 constructs. This step is described in a lot of detail at
260 \in{chapter}[chap:normalization].
262 \section{The Core language}
263 \defreftxt{core}{the Core language}
264 Most of the prototype deals with handling the program in the Core
265 language. In this section we will show what this language looks like and
268 The Core language is a functional language that describes
269 \emph{expressions}. Every identifier used in Core is called a
270 \emph{binder}, since it is bound to a value somewhere. On the highest
271 level, a Core program is a collection of functions, each of which bind a
272 binder (the function name) to an expression (the function value, which has
275 The Core language itself does not prescribe any program structure, only
276 expression structure. In the \small{GHC} compiler, the Haskell module
277 structure is used for the resulting Core code as well. Since this is not
278 so relevant for understanding the Core language or the Normalization
279 process, we'll only look at the Core expression language here.
281 Each Core expression consists of one of these possible expressions.
283 \startdesc{Variable reference}
284 \defref{variable reference}
288 This is a reference to a binder. It's written down as the
289 name of the binder that is being referred to along with its type. The
290 binder name should of course be bound in a containing scope (including
291 top level scope, so a reference to a top level function is also a
292 variable reference). Additionally, constructors from algebraic datatypes
293 also become variable references.
295 The value of this expression is the value bound to the given binder.
297 Each binder also carries around its type (explicitly shown above), but
298 this is usually not shown in the Core expressions. Only when the type is
299 relevant (when a new binder is introduced, for example) will it be
300 shown. In other cases, the binder is either not relevant, or easily
301 derived from the context of the expression. \todo{Ref sidenote on type
310 This is a literal. Only primitive types are supported, like
311 chars, strings, ints and doubles. The types of these literals are the
312 \quote{primitive} versions, like \lam{Char\#} and \lam{Word\#}, not the
313 normal Haskell versions (but there are builtin conversion functions).
316 \startdesc{Application}
321 This is function application. Each application consists of two
322 parts: The function part and the argument part. Applications are used
323 for normal function \quote{calls}, but also for applying type
324 abstractions and data constructors.
326 The value of an application is the value of the function part, with the
327 first argument binder bound to the argument part.
330 \startdesc{Lambda abstraction}
331 \defref{lambda abstraction}
335 This is the basic lambda abstraction, as it occurs in labmda calculus.
336 It consists of a binder part and a body part. A lambda abstraction
337 creates a function, that can be applied to an argument. The binder is
338 usually a value binder, but it can also be a \emph{type binder} (or
339 \emph{type variable}). The latter case introduces a new polymorphic
340 variable, which can be used in types later on. See
341 \in{section}[sec:prototype:coretypes] for details.
343 Note that the body of a lambda abstraction extends all the way to the
344 end of the expression, or the closing bracket surrounding the lambda. In
345 other words, the lambda abstraction \quote{operator} has the lowest
348 The value of an application is the value of the body part, with the
349 binder bound to the value the entire lambda abstraction is applied to.
352 \startdesc{Non-recursive let expression}
353 \defref{let expression}
355 let bndr = value in body
357 A let expression allows you to bind a binder to some value, while
358 evaluating to some other value (where that binder is in scope). This
359 allows for sharing of subexpressions (you can use a binder twice) and
360 explicit \quote{naming} of arbitrary expressions. Note that the binder
361 is not in scope in the value bound to it, so it's not possible to make
362 recursive definitions with the normal form of the let expression (see
363 the recursive form below).
365 Even though this let expression is an extension on the basic lambda
366 calculus, it is easily translated to a lambda abstraction. The let
367 expression above would then become:
373 This notion might be useful for verifying certain properties on
374 transformations, since a lot of verification work has been done on
375 lambda calculus already.
377 The value of a let expression is the value of the body part, with the
378 binder bound to the value.
381 \startdesc{Recursive let expression}
390 This is the recursive version of the let expression. In \small{GHC}'s
391 Core implementation, non-recursive and recursive lets are not so
392 distinct as we present them here, but this provides a clearer overview.
394 The main difference with the normal let expression is that each of the
395 binders is in scope in each of the values, in addition to the body. This
396 allows for self-recursive or mutually recursive definitions.
398 It should also be possible to express a recursive let using normal
399 lambda calculus, if we use the \emph{least fixed-point operator},
400 \lam{Y}. This falls beyond the scope of this report, since it is not
401 needed for this research.
404 \startdesc{Case expression}
405 \defref{case expression}
407 case scrutinee of bndr
408 DEFAULT -> defaultbody
409 C0 bndr0,0 ... bndr0,m -> body0
411 Cn bndrn,0 ... bndrn,m -> bodyn
416 A case expression is the only way in Core to choose between values. All
417 \hs{if} expressions and pattern matchings from the original Haskell
418 PRogram have been translated to case expressions by the desugarer.
420 A case expression evaluates its scrutinee, which should have an
421 algebraic datatype, into weak head normal form (\small{WHNF}) and
422 (optionally) binds it to \lam{bndr}. It then chooses a body depending on
423 the constructor of its scrutinee. If none of the constructors match, the
424 \lam{DEFAULT} alternative is chosen. A case expression must always be
425 exhaustive, \ie it must cover all possible constructors that the
426 scrutinee can have (if all of them are covered explicitly, the
427 \lam{DEFAULT} alternative can be left out).
429 Since we can only match the top level constructor, there can be no overlap
430 in the alternatives and thus order of alternatives is not relevant (though
431 the \lam{DEFAULT} alternative must appear first for implementation
434 Any arguments to the constructor in the scrutinee are bound to each of the
435 binders after the constructor and are in scope only in the corresponding
438 To support strictness, the scrutinee is always evaluated into
439 \small{WHNF}, even when there is only a \lam{DEFAULT} alternative. This
440 allows aplication of the strict function \lam{f} to the argument \lam{a}
444 f (case a of arg DEFAULT -> arg)
447 According to the \GHC documentation, this is the only use for the extra
448 binder to which the scrutinee is bound. When not using strictness
449 annotations (which is rather pointless in hardware descriptions),
450 \small{GHC} seems to never generate any code making use of this binder.
451 In fact, \GHC has never been observed to generate code using this
452 binder, even when strictness was involved. Nonetheless, the prototype
453 handles this binder as expected.
455 Note that these case statements are less powerful than the full Haskell
456 case statements. In particular, they do not support complex patterns like
457 in Haskell. Only the constructor of an expression can be matched,
458 complex patterns are implemented using multiple nested case expressions.
460 Case statements are also used for unpacking of algebraic datatypes, even
461 when there is only a single constructor. For examples, to add the elements
462 of a tuple, the following Core is generated:
465 sum = λtuple.case tuple of
469 Here, there is only a single alternative (but no \lam{DEFAULT}
470 alternative, since the single alternative is already exhaustive). When
471 it's body is evaluated, the arguments to the tuple constructor \lam{(,)}
472 (\eg, the elements of the tuple) are bound to \lam{a} and \lam{b}.
475 \startdesc{Cast expression}
476 \defref{cast expression}
480 A cast expression allows you to change the type of an expression to an
481 equivalent type. Note that this is not meant to do any actual work, like
482 conversion of data from one format to another, or force a complete type
483 change. Instead, it is meant to change between different representations
484 of the same type, \eg switch between types that are provably equal (but
487 In our hardware descriptions, we typically see casts to change between a
488 Haskell newtype and its contained type, since those are effectively
489 different types (so a cast is needed) with the same representation (but
490 no work is done by the cast).
492 More complex are types that are proven to be equal by the typechecker,
493 but look different at first glance. To ensure that, once the typechecker
494 has proven equality, this information sticks around, explicit casts are
495 added. In our notation we only write the target type, but in reality a
496 cast expressions carries around a \emph{coercion}, which can be seen as a
497 proof of equality. \todo{Example}
499 The value of a cast is the value of its body, unchanged. The type of this
500 value is equal to the target type, not the type of its body.
502 \todo{Move and update this paragraph}
503 Note that this syntax is also used sometimes to indicate that a particular
504 expression has a particular type, even when no cast expression is
505 involved. This is then purely informational, since the only elements that
506 are explicitely typed in the Core language are the binder references and
507 cast expressions, the types of all other elements are determined at
512 The Core language in \small{GHC} allows adding \emph{notes}, which serve
513 as hints to the inliner or add custom (string) annotations to a core
514 expression. These shouldn't be generated normally, so these are not
515 handled in any way in the prototype.
519 \defref{type expression}
523 It is possibly to use a Core type as a Core expression. For the actual
524 types supported by Core, see \in{section}[sec:prototype:coretypes]. This
525 \quote{lifting} of a type into the value domain is done to allow for
526 type abstractions and applications to be handled as normal lambda
527 abstractions and applications above. This means that a type expression
528 in Core can only ever occur in the argument position of an application,
529 and only if the type of the function that is applied to expects a type
530 as the first argument. This happens for all polymorphic functions, for
531 example, the \lam{fst} function:
534 fst :: \forall a. \forall b. (a, b) -> a
535 fst = λtup.case tup of (,) a b -> a
537 fstint :: (Int, Int) -> Int
538 fstint = λa.λb.fst @Int @Int a b
541 The type of \lam{fst} has two universally quantified type variables. When
542 \lam{fst} is applied in \lam{fstint}, it is first applied to two types.
543 (which are substitued for \lam{a} and \lam{b} in the type of \lam{fst}, so
544 the type of \lam{fst} actual type of arguments and result can be found:
545 \lam{fst @Int @Int :: (Int, Int) -> Int}).
548 \subsection[sec:prototype:coretypes]{Core type system}
549 Whereas the expression syntax of Core is very simple, its type system is
550 a bit more complicated. It turns out it is harder to \quote{desugar}
551 Haskell's complex type system into something more simple. Most of the
552 type system is thus very similar to that of Haskell.
554 We will slightly limit our view on Core's type system, since the more
555 complicated parts of it are only meant to support Haskell's (or rather,
556 \GHC's) type extensions, such as existential types, \small{GADT}s, type
557 families and other non-standard Haskell stuff which we don't (plan to)
560 In Core, every expression is typed. The translation to Core happens
561 after the typechecker, so types in Core are always correct as well
562 (though you could of course construct invalidly typed expressions).
564 Any type in core is one of the following:
566 \startdesc{A type variable}
571 This is a reference to a type defined elsewhere. This can either be a
572 polymorphic type (like the latter two \lam{t}'s in \lam{id :: \forall t.
573 t -> t}), or a type constructor (like \lam{Bool} in \lam{not :: Bool ->
574 Bool}). Like in Haskell, polymorphic type variables always
575 start with a lowercase letter, while type constructors always start
576 with an uppercase letter.
578 \todo{How to define (new) type constructors?}
580 A special case of a type constructor is the \emph{function type
581 constructor}, \lam{->}. This is a type constructor taking two arguments
582 (using application below). The function type constructor is commonly
583 written inline, so we write \lam{a -> b} when we really mean \lam{-> a
584 b}, the function type constructor applied to \lam{a} and \lam{b}.
586 Polymorphic type variables can only be defined by a lambda
587 abstraction, see the forall type below.
590 \startdesc{A type application}
595 This applies a some type to another type. This is particularly used to
596 apply type variables (type constructors) to their arguments.
598 As mentioned above, applications of some type constructors have
599 special notation. In particular, these are applications of the
600 \emph{function type constructor} and \emph{tuple type constructors}:
609 \startdesc{The forall type}
611 id :: \forall a. a -> a
613 The forall type introduces polymorphism. It is the only way to
614 introduce new type variables, which are completely unconstrained (Any
615 possible type can be assigned to it). Constraints can be added later
616 using predicate types, see below.
618 A forall type is always (and only) introduced by a type lambda
619 expression. For example, the Core translation of the
625 Here, the type of the binder \lam{x} is \lam{a}, referring to the
626 binder in the topmost lambda.
628 When using a value with a forall type, the actual type
629 used must be applied first. For example haskell expression \hs{id
630 True} (the function \hs{id} appleid to the dataconstructor \hs{True})
631 translates to the following Core:
637 Here, id is first applied to the type to work with. Note that the type
638 then changes from \lam{id :: \forall a. a -> a} to \lam{id @Bool ::
639 Bool -> Bool}. Note that the type variable \lam{a} has been
640 substituted with the actual type.
642 In Haskell, forall types are usually not explicitly specified (The use
643 of a lowercase type variable implicitly introduces a forall type for
644 that variable). In fact, in standard Haskell there is no way to
645 explicitly specify forall types. Through a language extension, the
646 \hs{forall} keyword is available, but still optional for normal forall
647 types (it is needed for \emph{existentially quantified types}, which
648 Cλash does not support).
651 \startdesc{Predicate type}
653 show :: \forall a. Show s ⇒ s → String
656 \todo{Sidenote: type classes?}
658 A predicate type introduces a constraint on a type variable introduced
659 by a forall type (or type lambda). In the example above, the type
660 variable \lam{a} can only contain types that are an \emph{instance} of
661 the \emph{type class} \lam{Show}. \refdef{type class}
663 There are other sorts of predicate types, used for the type families
664 extension, which we will not discuss here.
666 A predicate type is introduced by a lambda abstraction. Unlike with
667 the forall type, this is a value lambda abstraction, that must be
668 applied to a value. We call this value a \emph{dictionary}.
670 Without going into the implementation details, a dictionary can be
671 seen as a lookup table all the methods for a given (single) type class
672 instance. This means that all the dictionaries for the same type class
673 look the same (\eg contain methods with the same names). However,
674 dictionaries for different instances of the same class contain
675 different methods, of course.
677 A dictionary is introduced by \small{GHC} whenever it encounters an
678 instance declaration. This dictionary, as well as the binder
679 introduced by a lambda that introduces a dictionary, have the
680 predicate type as their type. These binders are usually named starting
681 with a \lam{\$}. Usually the name of the type concerned is not
682 reflected in the name of the dictionary, but the name of the type
683 class is. The Haskell expression \hs{show True} thus becomes:
686 show @Bool \$dShow True
690 Using this set of types, all types in basic Haskell can be represented.
692 \todo{Overview of polymorphism with more examples (or move examples
695 \section[sec:prototype:statetype]{State annotations in Haskell}
696 As noted in \in{section}[sec:description:stateann], Cλash needs some
697 way to let the programmer explicitly specify which of a function's
698 arguments and which part of a function's result represent the
701 Using the Haskell type systems, there are a few ways we can tackle this.
703 \subsection{Type synonyms}
704 Haskell provides type synonyms as a way to declare a new type that is
705 equal to an existing type (or rather, a new name for an existing type).
706 This allows both the original type and the synonym to be used
707 interchangedly in a Haskell program. This means no explicit conversion
708 is needed either. For example, a simple accumulator would become:
712 acc :: Word -> State Word -> (State Word, Word)
713 acc i s = let sum = s + i in (sum, sum)
716 This looks nice in Haskell, but turns out to be hard to implement. There
717 are no explicit conversion in Haskell, but not in Core either. This
718 means the type of a value might be show as \hs{AccState} in some places,
719 but \hs{Word} in others (and this can even change due to
720 transformations). Since every binder has an explicit type associated
721 with it, the type of every function type will be properly preserved and
722 could be used to track down the statefulness of each value by the
723 compiler. However, this makes the implementation a lot more complicated
724 than it currently is using \hs{newtypes}.
726 % Use \type instead of \hs here, since the latter breaks inside
728 \subsection{Type renaming (\type{newtype})}
729 Haskell also supports type renamings as a way to declare a new type that
730 has the same (runtime) representation as an existing type (but is in
731 fact a different type to the typechecker). With type renaming, an
732 explicit conversion between values of the two types is needed. The
733 accumulator would then become:
736 newtype State s = State s
737 acc :: Word -> State Word -> (State Word, Word)
738 acc i (State s) = let sum = s + i in (State sum, sum)
741 The \hs{newtype} line declares a new type \hs{State} that has one type
742 argument, \hs{s}. This type contains one \quote{constructor} \hs{State}
743 with a single argument of type \hs{s}. It is customary to name the
744 constructor the same as the type, which is allowed (since types can
745 never cause name collisions with values). The difference with the type
746 synonym example is in the explicit conversion between the \hs{State
747 Word} and \hs{Word} types by pattern matching and by using the explicit
748 the \hs{State constructor}.
750 This explicit conversion makes the \VHDL generation easier: Whenever we
751 remove (unpack) the \hs{State} type, this means we are accessing the
752 current state (\eg, accessing the register output). Whenever we are a
753 adding (packing) the \hs{State} type, we are producing a new value for
754 the state (\eg, providing the register input).
756 When dealing with nested states (a stateful function that calls stateful
757 functions, which might call stateful functions, etc.) the state type
758 could quickly grow complex because of all the \hs{State} type constructors
759 needed. For example, consider the following state type (this is just the
760 state type, not the entire function type):
763 State (State Bit, State (State Word, Bit), Word)
766 We cannot leave all these \hs{State} type constructors out, since that
767 would change the type (unlike when using type synonyms). However, when
768 using type synonyms to hide away substates (see
769 \in{section}[sec:prototype:substatesynonyms] below), this
770 disadvantage should be limited.
772 \subsubsection{Different input and output types}
773 An alternative could be to use different types for input and output
774 state (\ie current and updated state). The accumulator example would
775 then become something like:
778 newtype StateIn s = StateIn s
779 newtype StateOut s = StateOut s
780 acc :: Word -> StateIn Word -> (StateIn Word, Word)
781 acc i (StateIn s) = let sum = s + i in (StateIn sum, sum)
784 This could make the implementation easier and the hardware
785 descriptions less errorprone (you can no longer \quote{forget} to
786 unpack and repack a state variable and just return it directly, which
787 can be a problem in the current prototype). However, it also means we
788 need twice as many type synonyms to hide away substates, making this
789 approach a bit cumbersome. It also makes it harder to copmare input
790 and output state types, possible reducing the type safety of the
793 \subsection[sec:prototype:substatesynonyms]{Type synonyms for substates}
794 As noted above, when using nested (hierarchical) states, the state types
795 of the \quote{upper} functions (those that call other functions, which
796 call other functions, etc.) quickly becomes complicated. Also, when the
797 state type of one of the \quote{lower} functions changes, the state
798 types of all the upper functions changes as well. If the state type for
799 each function is explicitly and completely specified, this means that a
800 lot of code needs updating whenever a state type changes.
802 To prevent this, it is recommended (but not enforced) to use a type
803 synonym for the state type of every function. Every function calling
804 other functions will then use the state type synonym of the called
805 functions in its own type, requiring no code changes when the state type
806 of a called function changes. This approach is used in
807 \in{example}[ex:AvgState] below. The \hs{AccState} and \hs{AvgState}
808 are examples of such state type synonyms.
810 \subsection{Chosen approach}
811 To keep implementation simple, the current prototype uses the type
812 renaming approach, with a single type for both input and output
813 states. In the future, it might be worthwhile to revisit this
814 approach if more complicated flow analysis is implemented for
815 state variables. This analysis is needed to add proper error
816 checking anyway and might allow the use of type synonyms without
817 losing any expressivity.
819 \subsubsection{Example}
820 As an example of the used approach, there is a simple averaging circuit in
821 \in{example}[ex:AvgState]. This circuit lets the accumulation of the
822 inputs be done by a subcomponent, \hs{acc}, but keeps a count of value
823 accumulated in its own state.\footnote{Currently, the prototype
824 is not able to compile this example, since the builtin function
825 for division has not been added.}
827 \startbuffer[AvgState]
828 -- The state type annotation
829 newtype State s = State s
831 -- The accumulator state type
832 type AccState = State Word
834 acc :: Word -> AccState -> (AccState, Word)
835 acc i (State s) = let sum = s + i in (State sum, sum)
837 -- The averaging circuit state type
838 type AvgState = State (AccState, Word)
839 -- The averaging circuit
840 avg :: Word -> AvgState -> (AvgState, Word)
841 avg i (State s) = (State s', o)
844 -- Pass our input through the accumulator, which outputs a sum
845 (accs', sum) = acc i accs
846 -- Increment the count (which will be our new state)
848 -- Compute the average
853 \placeexample[here][ex:AvgState]{Simple stateful averaging circuit.}
854 %\startcombination[2*1]
855 {\typebufferhs{AvgState}}%{Haskell description using function applications.}
856 % {\boxedgraphic{AvgState}}{The architecture described by the Haskell description.}
860 \section{Implementing state}
861 Now its clear how to put state annotations in the Haskell source,
862 there is the question of how to implement this state translation. As
863 we've seen in \in{section}[sec:prototype:design], the translation to
864 \VHDL happens as a simple, final step in the compilation process.
865 This step works on a core expression in normal form. The specifics
866 of normal form will be explained in
867 \in{chapter}[chap:normalization], but the examples given should be
868 easy to understand using the definitin of Core given above.
870 \startbuffer[AvgStateNormal]
873 -- Remove the State newtype
877 -- Add the State newtype again
878 spacked' = s' ▶ State Word
885 s = spacked ▶ (AccState, Word)
886 accs = case s of (accs, _) -> accs
887 count = case s of (_, count) -> count
889 accs' = case accres of (accs', _) -> accs'
890 sum = case accres of (_, sum) -> sum
894 spacked' = s' ▶ State (AccState, Word)
900 \placeexample[here][ex:AvgStateNormal]{Normalized version of \in{example}[ex:AvgState]}
901 {\typebufferlam{AvgStateNormal}}
903 \subsection[sec:prototype:statelimits]{State in normal form}
904 Before describing how to translate state from normal form to
905 \VHDL, we will first see how state handling looks in normal form.
906 What limitations are there on their use to guarantee that proper
907 \VHDL can be generated?
909 We will try to formulate a number of rules about what operations are
910 allowed with state variables. These rules apply to the normalized Core
911 representation, but will in practice apply to the original Haskell
912 hardware description as well. Ideally, these rules would become part
913 of the intended normal form definition \refdef{intended normal form
914 definition}, but this is not the case right now. This can cause some
915 problems, which are detailed in
916 \in{section}[sec:normalization:stateproblems].
918 In these rules we use the terms \emph{state variable} to refer to any
919 variable that has a \lam{State} type. A \emph{state-containing
920 variable} is any variable whose type contains a \lam{State} type,
921 but is not one itself (like \lam{(AccState, Word)} in the example,
922 which is a tuple type, but contains \lam{AccState}, which is again
923 equal to \lam{State Word}).
925 We also use a distinction between \emph{input} and \emph{output
926 (state) variables} and \emph{substate variables}, which will be
927 defined in the rules themselves.
929 \startdesc{State variables can appear as an argument.}
931 avg = λi.λspacked. ...
934 Any lambda that binds a variable with a state type, creates a new
935 input state variable.
938 \startdesc{Input state variables can be unpacked.}
940 s = spacked ▶ (AccState, Word)
943 An input state variable may be unpacked using a cast operation. This
944 removes the \lam{State} type renaming and the result has no longer a
947 If the result of this unpacking does not have a state type and does
948 not contain state variables, there are no limitations on its use.
949 Otherwise if it does not have a state type but does contain
950 substates, we refer to it as a \emph{state-containing input
951 variable} and the limitations below apply. If it has a state type
952 itself, we refer to it as an \emph{input substate variable} and the
953 below limitations apply as well.
955 It may seem strange to consider a variable that still has a state
956 type directly after unpacking, but consider the case where a
957 function does not have any state of its own, but does call a single
958 stateful function. This means it must have a state argument that
959 contains just a substate. The function signature of such a function
963 type FooState = State AccState
966 Which is of course equivalent to \lam{State (State Word)}.
969 \startdesc{Variables can be extracted from state-containing input variables.}
971 accs = case s of (accs, _) -> accs
974 A state-containing input variable is typically a tuple containing
975 multiple elements (like the current function's state, substates or
976 more tuples containing substates). All of these can be extracted
977 from an input variable using an extractor case (or possibly
978 multiple, when the input variable is nested).
980 If the result has no state type and does not contain any state
981 variables either, there are no further limitations on its use. If
982 the result has no state type but does contain state variables we
983 refer to it as a \emph{state-containing input variable} and this
984 limitation keeps applying. If the variable has a state type itself,
985 we refer to it as an \emph{input substate variable} and below
988 \startdesc{Input substate variables can be passed to functions.}
991 accs' = case accres of (accs', _) -> accs'
994 An input substate variable can (only) be passed to a function.
995 Additionally, every input substate variable must be used in exactly
996 \emph{one} application, no more and no less.
998 The function result should contain exactly one state variable, which
999 can be extracted using (multiple) case statements. The extracted
1000 state variable is referred to the \emph{output substate}
1002 The type of this output substate must be identical to the type of
1003 the input substate passed to the function.
1006 \startdesc{Variables can be inserted into a state-containing output variable.}
1008 s' = (accs', count')
1011 A function's output state is usually a tuple containing its own
1012 updated state variables and all output substates. This result is
1013 built up using any single-constructor algebraic datatype.
1015 The result of these expressions is referred to as a
1016 \emph{state-containing output variable}, which are subject to these
1020 \startdesc{State containing output variables can be packed.}
1022 spacked' = s' ▶ State (AccState, Word)
1025 As soon as all a functions own update state and output substate
1026 variables have been joined together, the resulting
1027 state-containing output variable can be packed into an output
1028 state variable. Packing is done by casting into a state type.
1031 \startdesc{Output state variables can appear as (part of) a function result.}
1040 When the output state is packed, it can be returned as a part
1041 of the function result. Nothing else can be done with this
1042 value (or any value that contains it).
1045 There is one final limitation that is hard to express in the above
1046 itemization. Whenever substates are extracted from the input state
1047 to be passed to functions, the corresponding output substates
1048 should be inserted into the output state in the same way. In other
1049 words, each pair of corresponding substates in the input and
1050 output states should be passed / returned from the same called
1053 The prototype currently does not check much of the above
1054 conditions. This means that if the conditions are violated,
1055 sometimes a compile error is generated, but in other cases output
1056 can be generated that is not valid \VHDL or at the very least does
1057 not correspond to the input.
1059 \subsection{Translating to \VHDL}
1060 As noted above, the basic approach when generating \VHDL for stateful
1061 functions is to generate a single register for every stateful function.
1062 We look around the normal form to find the let binding that removes the
1063 \lam{State} newtype (using a cast). We also find the let binding that
1064 adds a \lam{State} type. These are connected to the output and the input
1065 of the generated let binding respectively. This means that there can
1066 only be one let binding that adds and one that removes the \lam{State}
1067 type. It is easy to violate this constraint. This problem is detailed in
1068 \in{section}[sec:normalization:stateproblems].
1070 This approach seems simple enough, but will this also work for more
1071 complex stateful functions involving substates? Observe that any
1072 component of a function's state that is a substate, \ie passed on as
1073 the state of another function, should have no influence on the
1074 hardware generated for the calling function. Any state-specific
1075 \small{VHDL} for this component can be generated entirely within the
1076 called function. So, we can completely ignore substates when
1077 generating \VHDL for a function.
1079 From this observation, we might think to remove the substates from a
1080 function's states alltogether, and leave only the state components
1081 which are actual states of the current function. While doing this
1082 would not remove any information needed to generate \small{VHDL} from
1083 the function, it would cause the function definition to become invalid
1084 (since we won't have any substate to pass to the functions anymore).
1085 We could solve the syntactic problems by passing \type{undefined} for
1086 state variables, but that would still break the code on the semantic
1087 level (\ie, the function would no longer be semantically equivalent to
1088 the original input).
1090 To keep the function definition correct until the very end of the
1091 process, we will not deal with (sub)states until we get to the
1092 \small{VHDL} generation. Then, we are translating from Core to
1093 \small{VHDL}, and we can simply ignore substates, effectively removing
1094 the substate components alltogether.
1096 But, how will we know what exactly is a substate? Since any state
1097 argument or return value that represents state must be of the
1098 \type{State} type, we can look at the type of a value. However, we
1099 must be careful to ignore only \emph{substates}, and not a
1100 function's own state.
1102 In \in{example}[ex:AvgStateNorm] above, we should generate a register
1103 connected with its output connected to \lam{s} and its input connected
1104 to \lam{s'}. However, \lam{s'} is build up from both \lam{accs'} and
1105 \lam{count'}, while only \lam{count'} should end up in the register.
1106 \lam{accs'} is a substate for the \lam{acc} function, for which a
1107 register will be created when generating \VHDL for the \lam{acc}
1110 Fortunately, the \lam{accs'} variable (and any other substate) has a
1111 property that we can easily check: It has a \lam{State} type
1112 annotation. This means that whenever \VHDL is generated for a tuple
1113 (or other algebraic type), we can simply leave out all elements that
1114 have a \lam{State} type. This will leave just the parts of the state
1115 that do not have a \lam{State} type themselves, like \lam{count'},
1116 which is exactly a function's own state. This approach also means that
1117 the state part of the result is automatically excluded when generating
1118 the output port, which is also required.
1120 We can formalize this translation a bit, using the following
1124 \item A state unpack operation should not generate any \small{VHDL}.
1125 The binder to which the unpacked state is bound should still be
1126 declared, this signal will become the register and will hold the
1128 \item A state pack operation should not generate any \small{VHDL}.
1129 The binder to which the packed state is bound should not be
1130 declared. The binder that is packed is the signal that will hold the
1132 \item Any values of a State type should not be translated to
1133 \small{VHDL}. In particular, State elements should be removed from
1134 tuples (and other datatypes) and arguments with a state type should
1136 \item To make the state actually work, a simple \small{VHDL} proc
1137 should be generated. This proc updates the state at every
1138 clockcycle, by assigning the new state to the current state. This
1139 will be recognized by synthesis tools as a register specification.
1142 When applying these rules to the description in
1143 \in{example}[ex:AvgStateNormal], we be left with the description
1144 in \in{example}[ex:AvgStateRemoved]. All the parts that don't
1145 generate any \VHDL directly are crossed out, leaving just the
1146 actual flow of values in the final hardware.
1149 avg = iλ.--λspacked.--
1151 s = --spacked ▶ (AccState, Word)--
1152 --accs = case s of (accs, _) -> accs--
1153 count = case s of (--_,-- count) -> count
1154 accres = acc i --accs--
1155 --accs' = case accres of (accs', _) -> accs'--
1156 sum = case accres of (--_,-- sum) -> sum
1159 s' = (--accs',-- count')
1160 --spacked' = s' ▶ State (AccState, Word)--
1161 res = (--spacked',-- o)
1166 When we would really leave out the crossed out parts, we get a slightly
1167 weird program: There is a variable \lam{s} which has no value, and there
1168 is a variable \lam{s'} that is never used. Together, these two will form
1169 the state proc of the function. \lam{s} contains the "current" state,
1170 \lam{s'} is assigned the "next" state. So, at the end of each clock
1171 cycle, \lam{s'} should be assigned to \lam{s}.
1173 As you can see, the definition of \lam{s'} is still present, since
1174 it does not have a state type. The \lam{accums'} substate has been
1175 removed, leaving us just with the state of \lam{avg} itself.
1177 As an illustration of the result of this function,
1178 \in{example}[ex:AccStateVHDL] and \in{example}[ex:AvgStateVHDL] show the the \VHDL that is
1179 generated from the examples is this section.
1181 \startbuffer[AvgStateVHDL]
1182 entity avgComponent_0 is
1183 port (\izAlE2\ : in \unsigned_31\;
1184 \foozAo1zAo12\ : out \(,)unsigned_31\;
1185 clock : in std_logic;
1186 resetn : in std_logic);
1187 end entity avgComponent_0;
1190 architecture structural of avgComponent_0 is
1191 signal \szAlG2\ : \(,)unsigned_31\;
1192 signal \countzAlW2\ : \unsigned_31\;
1193 signal \dszAm62\ : \(,)unsigned_31\;
1194 signal \sumzAmk3\ : \unsigned_31\;
1195 signal \reszAnCzAnM2\ : \unsigned_31\;
1196 signal \foozAnZzAnZ2\ : \unsigned_31\;
1197 signal \reszAnfzAnj3\ : \unsigned_31\;
1198 signal \s'zAmC2\ : \(,)unsigned_31\;
1200 \countzAlW2\ <= \szAlG2\.A;
1202 \comp_ins_dszAm62\ : entity accComponent_1
1203 port map (\izAob3\ => \izAlE2\,
1204 \foozAoBzAoB2\ => \dszAm62\,
1208 \sumzAmk3\ <= \dszAm62\.A;
1210 \reszAnCzAnM2\ <= to_unsigned(1, 32);
1212 \foozAnZzAnZ2\ <= \countzAlW2\ + \reszAnCzAnM2\;
1214 \reszAnfzAnj3\ <= \sumzAmk3\ * \foozAnZzAnZ2\;
1216 \s'zAmC2\.A <= \foozAnZzAnZ2\;
1218 \foozAo1zAo12\.A <= \reszAnfzAnj3\;
1220 state : process (clock, resetn)
1222 if resetn = '0' then
1223 elseif rising_edge(clock) then
1224 \szAlG2\ <= \s'zAmC2\;
1227 end architecture structural;
1229 \startbuffer[AccStateVHDL]
1230 entity accComponent_1 is
1231 port (\izAob3\ : in \unsigned_31\;
1232 \foozAoBzAoB2\ : out \(,)unsigned_31\;
1233 clock : in std_logic;
1234 resetn : in std_logic);
1235 end entity accComponent_1;
1238 architecture structural of accComponent_1 is
1239 signal \szAod3\ : \unsigned_31\;
1240 signal \reszAonzAor3\ : \unsigned_31\;
1242 \reszAonzAor3\ <= \szAod3\ + \izAob3\;
1244 \foozAoBzAoB2\.A <= \reszAonzAor3\;
1246 state : process (clock, resetn)
1248 if resetn = '0' then
1249 elseif rising_edge(clock) then
1250 \szAod3\ <= \reszAonzAor3\;
1253 end architecture structural;
1256 \placeexample[][ex:AccStateVHDL]{\VHDL generated for acc from \in{example}[ex:AvgState]}
1257 {\typebuffer[AccStateVHDL]}
1258 \placeexample[][ex:AvgStateVHDL]{\VHDL generated for avg from \in{example}[ex:AvgState]}
1259 {\typebuffer[AvgStateVHDL]}
1260 % \subsection{Initial state}
1261 % How to specify the initial state? Cannot be done inside a hardware
1262 % function, since the initial state is its own state argument for the first
1263 % call (unless you add an explicit, synchronous reset port).
1265 % External init state is natural for simulation.
1267 % External init state works for hardware generation as well.
1269 % Implementation issues: state splitting, linking input to output state,
1270 % checking usage constraints on state variables.
1272 % \todo{Implementation issues: Separate compilation, simplified core.}
1274 % vim: set sw=2 sts=2 expandtab: