Add sitenote about arguments vs. inputs.
authorMatthijs Kooijman <matthijs@stdin.nl>
Mon, 7 Dec 2009 13:07:24 +0000 (14:07 +0100)
committerMatthijs Kooijman <matthijs@stdin.nl>
Mon, 7 Dec 2009 13:07:24 +0000 (14:07 +0100)
Chapters/Conclusions.tex
Chapters/HardwareDescription.tex
Chapters/Normalization.tex

index a8d7e9b5f5b7149f6801b97604f0b6aa2368afef..7e76abc4eca6c5a79b28687dfbcae784af49e651 100644 (file)
@@ -1,7 +1,7 @@
 \chapter[chap:conclusions]{Conclusions}
 \chapter[chap:conclusions]{Conclusions}
-At the end of this research, we have created a system called Cλash, which
-allows us to translate hardware descriptions written in Haskell to be
-translated to \VHDL, and be programmed into an FPGA.
+The product of this research is a system called Cλash, which allows hardware
+descriptions written in Haskell to be translated to \VHDL and be programmed
+into an \small{FPGA}.
 
 In this research, we have seen that a functional language is well suited
 for hardware descriptions. Function applications provide elegant notation for
 
 In this research, we have seen that a functional language is well suited
 for hardware descriptions. Function applications provide elegant notation for
@@ -21,7 +21,7 @@ allowing for experimenting with various functional language features and
 interpretations in Cλash. Even supporting more complex features like
 polymorphism and higher-order values has been possible. If a new language and
 compiler would have been designed from scratch, that new language would not
 interpretations in Cλash. Even supporting more complex features like
 polymorphism and higher-order values has been possible. If a new language and
 compiler would have been designed from scratch, that new language would not
-have been nearly as advanced as current Cλash.
+have been nearly as advanced as the current version of Cλash.
 
 However, Haskell might not have been the best choice for describing
 hardware. Some of the expressiveness it offers is not appropriate for
 
 However, Haskell might not have been the best choice for describing
 hardware. Some of the expressiveness it offers is not appropriate for
@@ -31,13 +31,13 @@ boilerplate).
 
 The lack of real dependent typing support in Haskell has been a burden.
 Haskell provides the tools to create some type level programming
 
 The lack of real dependent typing support in Haskell has been a burden.
 Haskell provides the tools to create some type level programming
-constructs (and is improving fast), but other language might have
-support for more advanced dependent types (and even type level
-operations) as a fundamental part of the language. The need for
-dependent typing is particularly present in Cλash to be able to fix some
-properties (list length, recursion depth, etc.) at compile time. Having
-better support for dependent typing might allow the use of typesafe
-recursion in Cλash, though this is fundamentally still a hard problem.
+constructs (and is improving fast), but another language might have
+support for more advanced dependent types (and even type level operations) as
+a fundamental part of the language. The need for dependent typing is
+particularly present in Cλash to be able to fix some properties (list length,
+recursion depth, etc.) at compile time. Having better support for dependent
+typing might allow the use of typesafe recursion in Cλash, though this is
+fundamentally still a hard problem.
 
 The choice of describing state very explicitly as extra arguments and
 results is a mixed blessing. It provides very explicit specification of
 
 The choice of describing state very explicitly as extra arguments and
 results is a mixed blessing. It provides very explicit specification of
@@ -52,7 +52,7 @@ and repacking becomes tedious and even errorprone. Removing some of this
 boilerplate would make the language even easier to use.
 
 On the whole, the usefulness of Cλash for describing hardware is not
 boilerplate would make the language even easier to use.
 
 On the whole, the usefulness of Cλash for describing hardware is not
-completely clear yet. Most elements of the language haven proven
+completely clear yet. Most elements of the language have proven
 suitable, and even a real world hardware circuit (the reducer \todo{ref
 christiaan}) has been implemented. However, the language has not been
 used during a complete design process, where its rapid prototyping and
 suitable, and even a real world hardware circuit (the reducer \todo{ref
 christiaan}) has been implemented. However, the language has not been
 used during a complete design process, where its rapid prototyping and
@@ -60,11 +60,11 @@ reusability qualities could become real advantages, or perhaps the state
 boilerplate or synchronicity limitations could become real problems.
 
 It is expected that Cλash will be used as a tool in education at the
 boilerplate or synchronicity limitations could become real problems.
 
 It is expected that Cλash will be used as a tool in education at the
-University of Twente soon, hopefully this will provide a better insight
+University of Twente soon. Hopefully this will provide a better insight
 in how the system performs.
 
 The prototype compiler has a clear design. Its frontend is taken from the \GHC\
 in how the system performs.
 
 The prototype compiler has a clear design. Its frontend is taken from the \GHC\
-compiler and desugares Haskell into a small, but functional and typed
+compiler and desugars Haskell into a small, but functional and typed
 language, called \emph{Core}. Cλash adds a transformation system that reduces
 this small language to a normal form and a simple backend that performs a
 direct translation to \VHDL. This approach has worked well and should probably
 language, called \emph{Core}. Cλash adds a transformation system that reduces
 this small language to a normal form and a simple backend that performs a
 direct translation to \VHDL. This approach has worked well and should probably
@@ -77,14 +77,13 @@ However, the system can be (and has been) described in a mathematical sense,
 allowing us to reason about it and probably also prove various correctness
 properties in the future.
 
 allowing us to reason about it and probably also prove various correctness
 properties in the future.
 
-The scope of this research has been limited to structural descriptions
-that are synchronous in a single clock domain using cycle accurate
-designs. Even though this is a broad spectrum already, it may turn out
-that this scope is too narrow for practical use of Cλash. Most people
-that hear about using a functional language for hardware description
-instantly hope to be able to provide a concise mathematical description
-of their algorithm and have the hardware generated for them. Since this
-is obviously a different problem altogether, we could not have hoped to
-even start solving it. However, hopefully the current Cλash system
-provides a solid base on top of which further experimentation with
-functional descriptions can be built.
+The scope of this research has been limited to structural descriptions that
+are synchronous in a single clock domain using cycle accurate designs. Even
+though this is a broad spectrum already, it may turn out that this scope is
+too narrow for practical use of Cλash. A common response from people that hear
+about using a functional language for hardware description is that they hope
+to be able to provide a concise mathematical description of their algorithm
+and have the hardware generated for them. Since this is obviously a different
+problem altogether, we could not have hoped to even start solving it. However,
+hopefully the current Cλash system provides a solid base on top of which
+further experimentation with functional descriptions can be built.
index bf797f62a7356c02a0a40c1a8339d7f0f4017637..ff4b0c0b3143c78983f6464ad52d95e090b5488f 100644 (file)
@@ -56,7 +56,6 @@
 
 
   \section[sec:description:application]{Function application}
 
 
   \section[sec:description:application]{Function application}
-  \todo{Sidenote: Inputs vs arguments}
   The basic syntactic elements of a functional program are functions and
   function application. These have a single obvious \small{VHDL}
   translation: Each top level function becomes a hardware component, where each
   The basic syntactic elements of a functional program are functions and
   function application. These have a single obvious \small{VHDL}
   translation: Each top level function becomes a hardware component, where each
@@ -136,8 +135,7 @@ and3 a b c = and (and a b) c
     the condition is false.
 
     This \hs{if} function would then essentially describe a multiplexer and
     the condition is false.
 
     This \hs{if} function would then essentially describe a multiplexer and
-    allows us to describe any architecture that uses multiplexers. \fxnote{Are
-    there other mechanisms of choice in hardware?}
+    allows us to describe any architecture that uses multiplexers.
 
     However, to be able to describe our hardware in a more convenient way, we
     also want to translate Haskell's choice mechanisms. The easiest of these
 
     However, to be able to describe our hardware in a more convenient way, we
     also want to translate Haskell's choice mechanisms. The easiest of these
@@ -146,7 +144,26 @@ and3 a b c = and (and a b) c
     simply be translated to a conditional assignment, where the conditions use
     equality comparisons against the constructors in the \hs{case} expressions.
 
     simply be translated to a conditional assignment, where the conditions use
     equality comparisons against the constructors in the \hs{case} expressions.
 
-    \todo{Assignment vs multiplexers}
+    \placeintermezzo{}{
+      \defref{substitution notation}
+      \startframedtext[width=8cm,background=box,frame=no]
+      \startalignment[center]
+        {\tfa Arguments / results vs. inputs / outputs}
+      \stopalignment
+      \blank[medium]
+        Due to the translation chosen for function application, there is a
+        very strong relation between arguments, results, inputs and outputs.
+        For clarity, the former two will always refer to the arguments and
+        results in the functional description (either Haskell or Core). The
+        latter two will refer to input and output ports in the generated
+        \VHDL.
+
+        Even though these concepts seem to be nearly identical, when stateful
+        functions are introduces we will see arguments and results that will
+        not get translated into input and output ports, making this
+        distinction more important.
+      \stopframedtext
+    }
 
     In \in{example}[ex:CaseInv] a simple \hs{case} expression is shown,
     scrutinizing a boolean value. The corresponding architecture has a
 
     In \in{example}[ex:CaseInv] a simple \hs{case} expression is shown,
     scrutinizing a boolean value. The corresponding architecture has a
@@ -163,8 +180,6 @@ and3 a b c = and (and a b) c
     Optimizations such as these are left for the \VHDL\ synthesizer, which
     handles them very well.
 
     Optimizations such as these are left for the \VHDL\ synthesizer, which
     handles them very well.
 
-    \todo{Be more explicit about >2 alternatives}
-
     \startbuffer[CaseInv]
     inv :: Bool -> Bool
     inv x = case x of
     \startbuffer[CaseInv]
     inv :: Bool -> Bool
     inv x = case x of
@@ -235,6 +250,11 @@ and3 a b c = and (and a b) c
     nested) multiplexers. These multiplexers are driven by comparators and
     other logic, that check each pattern in turn.
 
     nested) multiplexers. These multiplexers are driven by comparators and
     other logic, that check each pattern in turn.
 
+    In these examples we have seen only binary case expressions and pattern
+    matches (\ie, with two alternatives). In practice, case expressions can
+    choose between more than two values, resulting in a number of nested
+    multiplexers.
+
   \section{Types}
     Translation of two most basic functional concepts has been
     discussed: Function application and choice. Before looking further
   \section{Types}
     Translation of two most basic functional concepts has been
     discussed: Function application and choice. Before looking further
index 433871013eced36c05be270707d14eceeed84646..d564d231405a00ab7f31622ef525b15f987c2218 100644 (file)
     developed in the final part of the research, leaving no more time
     for verifying these properties. In fact, it is likely that the
     current transformation system still violates some of these
     developed in the final part of the research, leaving no more time
     for verifying these properties. In fact, it is likely that the
     current transformation system still violates some of these
-    properties in some cases and should be improved (or extra conditions
-    on the input hardware descriptions should be formulated).
+    properties in some cases (see
+    \in{section}[sec:normalization:non-determinism] and
+    \in{section}[sec:normalization:stateproblems]) and should be improved (or
+    extra conditions on the input hardware descriptions should be formulated).
 
     This is most likely the case with the completeness and determinism
 
     This is most likely the case with the completeness and determinism
-    properties, perhaps als the termination property. The soundness
+    properties, perhaps also the termination property. The soundness
     property probably holds, since it is easier to manually verify (each
     transformation can be reviewed separately).
 
     property probably holds, since it is easier to manually verify (each
     transformation can be reviewed separately).
 
       each node in the normal set is also in the intended normal set.
       Reasoning about our intended normal set is easier, since we know
       how to generate it from its definition. \refdef{intended normal
       each node in the normal set is also in the intended normal set.
       Reasoning about our intended normal set is easier, since we know
       how to generate it from its definition. \refdef{intended normal
-      form definition}.
+      form definition}
 
       Fortunately, we can also prove the complement (which is
       equivalent, since $A \subseteq B \Leftrightarrow \overline{B}
 
       Fortunately, we can also prove the complement (which is
       equivalent, since $A \subseteq B \Leftrightarrow \overline{B}