\section{Analysis of the EDSLs}
\label{sec:analysis-of-the-edsls}
    \frame{\sectionpage}

    \subsection{Lava}
    \label{subsec:lava}
        % Lava intro
        \begin{frame}
            \frametitle{Lava}

            \begin{itemize}
                \item Developed at Chalmers University of Technology, Sweden
                    \begin{itemize}
                        \item Initially by Koen Claessen and Mary Sheeran
                        \item Later also Per Bjesse and David Sands
                    \end{itemize}

                \item Has several \emph{dialects}
                    \begin{itemize}
                        \item \texttt{chalmers-lava}, \texttt{xilinx-lava}, \texttt{kansas-lava}, etc. 
                        \item We focus on the ``canonical'' \texttt{chalmers-lava}
                    \end{itemize}
            \end{itemize}
        \end{frame}

        \begin{frame}
            \frametitle{Lava's \emph{key} characteristics}

            \begin{itemize}
                \item Deep-embedded
                \item Observable sharing
                    \begin{itemize}
                        \item ``Type-safe pointer equality'' to detect sharing and recursion
                        \item Advantages and disadvantages clearer with examples
                    \end{itemize}
                \item Capable of simulation, verification and synthesis
                    \begin{itemize}
                        \item Generates \emph{flat} VHDL
                        \item External tools for verification
                    \end{itemize}
                \item Very ``functional'' style of hardware description
                    \begin{itemize}
                        \item Will become clearer with examples
                    \end{itemize}
            \end{itemize}
        \end{frame}

        \begin{frame}
            \frametitle{Lava: Adders}
            \haskellfile{code/lava-adders.hs}

            \begin{itemize}
                \item Straightforward Haskell constructs
                \item ``\texttt{and2}'', ``\texttt{xor2}'', etc. are Lava's \emph{atomic} circuits
            \end{itemize}
        \end{frame}

        \begin{frame}
            \frametitle{Lava: Simulation and verification}

            \begin{itemize}
                \item A taste of simulation in Lava:
                    \haskellfile{code/lava-simulation-halfadder.hs}
                    \begin{itemize}
                        \item Cannot be easily automated: equality of \texttt{Signal} is non-trivial
                    \end{itemize}

                \item And verification\ldots
                    \haskellfile{code/lava-verify-fulladder-comm.hs}
                    \begin{itemize}
                        \item Advantage: Fully automated (external SAT solver)
                        \item Disadvantage: Only verifies instances of \emph{specific size}
                    \end{itemize}
            \end{itemize}

            \note{
                \begin{itemize}
                    \item Safety properties: circuit with one output always True
                \end{itemize}
            }
        \end{frame}

        % Lava ALU
        \begin{frame}
            \frametitle{Lava: ALU}
            \haskellfile{code/lava-alu.hs}
        \end{frame}

        \begin{frame}
            \frametitle{Remarks}

            \begin{itemize}
                \item Cannot introduce new, meaningful datatypes
                    \begin{itemize}
                        \item Only \texttt{Signal Bool} is synthesizable
                        \item Or tuples/lists thereof
                    \end{itemize}
                \item Input/Output types have to be \emph{uncurried}
                \item Weak type-safety over the inputs/outputs
                    \begin{itemize}
                        \item Working with tuples is tiresome and has limitations
                        \item Lists don't enforce \emph{size} constraints
                    \end{itemize}
            \end{itemize}

            \note{
                \begin{itemize}
                    \item Signal Int exists, but not synthesizable
                    \item Max tuple size implementation-dependent
                \end{itemize}
            }
        \end{frame}

        % Lava RAM64
        \begin{frame}
            \frametitle{Lava: RAM64}
            \haskellfile{code/lava-ram64.hs}
        \end{frame}

        \begin{frame}
            \frametitle{Remarks}

            \par{Positive:}
            \begin{itemize}
                \item Uses host language for binding (\texttt{let}/\texttt{where}) and recursion
                \item Uses host language for structural combinators
            \end{itemize}

            \par{Negative:}
            \begin{itemize}
                \item Again, weak type-safety of lists
                    \begin{itemize}
                        \item Extra \texttt{Int} parameter controls port \emph{sizes}
                        \item But not \emph{type-safe}
                    \end{itemize}
                \item \emph{No modularity} in the generated VHDL code.
            \end{itemize}

            \note{
                \begin{itemize}
                    \item Lists type un-safety: user can control, but not \emph{forced to} control
                \end{itemize}
            }
        \end{frame}

        % Lava CPU
        \begin{frame}
            \frametitle{Lava: \emph{Hack} CPU (new parts)}
            \haskellfile{code/lava-cpu.hs}

            \note{
                \begin{itemize}
                    \item Decoder is basically just slicing the instruction
                \end{itemize}
            }
        \end{frame}

        \begin{frame}
            \frametitle{Final remarks}

            \par{Lava could benefit from:}
            \vspace{0.2cm}
            \begin{itemize}
                \item Fixed-length vectors
                    \begin{itemize}
                        \item ForSyDe-style or with type-level naturals in recent GHC.
                    \end{itemize}
                \item Slicing operators over vectors
                \item \emph{Synthesizable} user-defined datatypes
                \item Better way of providing observable sharing
            \end{itemize}
        \end{frame}


    \subsection{ForSyDe}
    \label{subsec:forsyde}
        % ForSyDe intro
        \begin{frame}
            \frametitle{ForSyDe}

            \begin{itemize}
                \item Based on the ``Formal System Design'' approach
                    \begin{itemize}
                        \item Royal Institute of Technology - KTH, Stockholm
                    \end{itemize}
                \item Available for Haskell and SystemC
                \item Has BOTH shallow and deep-embedded ``versions''
                    \begin{itemize}
                        \item Same library, subtle distinction
                        \item Will become clearer with examples
                    \end{itemize}
                \item \emph{Template Haskell} to express circuits with Haskell syntax
            \end{itemize}
        \end{frame}

        \begin{frame}
            \frametitle{ForSyDe's key concepts}

            \begin{itemize}
                \item Models of Computation (MoCs)
                    \begin{itemize}
                        \item We focus on the \emph{synchronous} MoC
                    \end{itemize}
                \item Processes
                    \begin{itemize}
                        \item Basic unit of computation
                        \item A process belongs to a MoC
                        \item Built with a \emph{process constructor}
                    \end{itemize}
                \item Signals
                    \begin{itemize}
                        \item Connections among processes
                    \end{itemize}
            \end{itemize}

            \note{
                \begin{itemize}
                    \item Process and MoC intertwinned concepts
                \end{itemize}
            }
        \end{frame}

        \begin{frame}
            \frametitle{ForSyDe's key concepts}
            \begin{figure}[h!]
                \centerline{\includegraphics[width=0.8\textwidth]{imgs/forsyde-model.pdf}}
                \caption{Key concepts of the ForSyDe EDSL
                    \label{fig:forsyde-model}}
            \end{figure}
        \end{frame}

        % ForSyDe ALU non-synth
        \begin{frame}
            \frametitle{ForSyDe: ALU (non-synth)}
            \haskellfile{code/forsyde-alusim-slide1.hs}
        \end{frame}

        \begin{frame}
            \frametitle{ForSyDe: ALU (non-synth)}
            \haskellfile{code/forsyde-alusim-slide2.hs}
        \end{frame}

        \begin{frame}
            \frametitle{ForSyDe: synthesis restrictions}
            \par{Restrictions imposed on a model by ForSyDe so that it can be translated to VHDL:}
            \begin{itemize}
                \item ProcFun-related:
                    \begin{itemize}
                        \item Limited argument types (instances of \texttt{ProcType})
                        \item \texttt{Int}, \texttt{Int8}, \ldots, \texttt{Bool}, \texttt{Bit}
                        \item Enumerated types (deriving \texttt{Data} and \texttt{Lift})
                        \item Tuples and \texttt{FSVec}'s
                    \end{itemize}
                \item VHDL engine-related:
                    \begin{itemize}
                        \item No point-free notation
                        \item Single clause / no pattern matching
                        \item No \texttt{where} or \texttt{let} bindings
                    \end{itemize}
            \end{itemize}
        \end{frame}

        % ForSyDe ALU synth
        \begin{frame}
            \frametitle{ForSyDe: ALU (synthesizable)}
            \haskellfile{code/forsyde-alusyn-slide1.hs}
        \end{frame}

        \begin{frame}
            \frametitle{ForSyDe: ALU (synthesizable)}
            \haskellfile{code/forsyde-alusyn-slide2.hs}
        \end{frame}

        % ForSyDe Simulation

        % ForSyDe RAM64
        \begin{frame}
            \frametitle{ForSyDe: RAM64}
            \haskellfile{code/forsyde-ram64.hs}
        \end{frame}

        \begin{frame}
            \frametitle{Remarks}

            \begin{itemize}
                \item Component \emph{instantiation}
                    \begin{itemize}
                        \item Introduces \emph{hierarchy} in the design
                        \item Influences generated VHDL
                    \end{itemize}
                \item \emph{Manual} name management
                    \begin{itemize}
                        \item Error-prone
                        \item Every process must have a \emph{unique} identifier
                        \item Already was a (lesser) issue with the muxes
                    \end{itemize}
            \end{itemize}
        \end{frame}

        % ForSyDe CPU
        \begin{frame}
            \frametitle{ForSyDe: \emph{Hack} CPU (part)}
            \haskellfile{code/forsyde-cpu-decoder.hs}
        \end{frame}


    \subsection{Coquet}
    \label{subsec:coquet}
        % Coquet Intro
        \begin{frame}
            \frametitle{Coquet}

            \begin{itemize}
                \item Developed by Thomas Braibant (INRIA, France)
                    \begin{itemize}
                        \item Seminal paper published in 2011
                    \end{itemize}
                \item Library embedded in the \emph{Coq} proof assistant
                    \begin{itemize}
                        \item Deep-embedded
                        \item Models the \emph{architecture} of circuits
                    \end{itemize}
                \item Allows for \emph{correctness proofs} of circuits
                    \begin{itemize}
                        \item According to a given \emph{specification}
                        \item Provides \emph{tactics} to help with these proofs
                        \item More powerful, inductive proofs
                    \end{itemize}
            \end{itemize}

            \note{
                \begin{itemize}
                    \item More powerful than SAT-solver based formal verification
                \end{itemize}
            }
        \end{frame}

        % Coquet Circuit type
        \begin{frame}
            \frametitle{Coquet: The \texttt{Circuit} type}
            \coqfile{code/coquet-circuit-type.v}
        \end{frame}
        
        \begin{frame}
            \frametitle{Features from the \texttt{Circuit} type}

            \begin{itemize}
                \item Circuit \emph{structure} as constructors of the datatype
                    \begin{itemize}
                        \item \emph{Explicit} loops (recursion) as constructor
                    \end{itemize}
                \item Parameterized by one type of \emph{fundamental gate} (\texttt{Atom})
                    \begin{itemize}
                        \item For example, \texttt{NOR} or \texttt{NAND}
                    \end{itemize}
                \item Circuit I/O ports are defined by \emph{finite} types
                    \begin{itemize}
                        \item Instances of the ``\texttt{Fin}'' typeclass
                    \end{itemize}
            \end{itemize}
        \end{frame}

        % Coquet quick usage example
        \begin{frame}
            \frametitle{Coquet: circuit example}
            \coqfile{code/coquet-fulladder.v}
        \end{frame}

        \begin{frame}
            \frametitle{Features from the example}
            
            \begin{itemize}
                \item Circuit I/O types (finite types)
                    \begin{itemize}
                        \item Parameterized by strings: \emph{tagged units}
                        \item Default ``\texttt{Fin}'' instances for sums, units
                    \end{itemize}
                \item Serial/Parallel composition
                \item \emph{Associativity plugs} (reordering) automatically defined
                    \begin{itemize}
                        \item With help of proof search
                    \end{itemize}
            \end{itemize}
        \end{frame}

        % How to prove circuit correctness
        \begin{frame}
            \frametitle{Coquet: How to prove correctness}

            \par{To understand Coquet proofs, we need 2 concepts:}
            \begin{itemize}
                \item Meaning relation
                    \begin{itemize}
                        \item Circuit → \emph{Prop}
                    \end{itemize}
                \item Behavioural specification
                    \begin{itemize}
                        \item What should a circuit \emph{do} with its inputs
                    \end{itemize}
            \end{itemize}
            \vspace{0.5cm}
            \par{Let's take a look at the definition for each of these concepts\ldots}
        \end{frame}

        % Meaning relation
        \begin{frame}
            \frametitle{Coquet: Meaning relation}
            \coqfile{code/coquet-meaning-relation.v}
        \end{frame}

        % Specification definitions
        \begin{frame}
            \frametitle{Coquet: Specification}
            \coqfile{code/coquet-realise-implement.v}

            \vspace{0.5cm}
            \par{The semantics of a circuit \emph{entails} (implies):}
            \begin{itemize}
                \item A \emph{relation} between inputs and outputs
                \item The application of a \emph{function} to the inputs
                \item Up to isomorphisms\ldots
            \end{itemize}
            \par{Now for a (small) example of correctness proof\ldots}
        \end{frame}

        % Adder proof (1)
        \begin{frame}
            \frametitle{Coquet: Correctness proofs}
            \coqfile{code/coquet-halfadder-proof.v}
        \end{frame}

        % How to do proofs in Coquet (tac, etc)
        \begin{frame}
            \frametitle{Coquet: How to prove correctness}
            \coqfile{code/coquet-tac.v}
            % rinvert: invert derivation of meaning relation, following structure of circuit.
            % realise_all: use the Implement and Realise classes as hints to transform goals.
            % unreify_all: get rid of iso's
            % destruct all boolean, then proof by case analysis, not so important.
        \end{frame}

