path: root/flashlight22.org

#+title: Verifying Software Pipelining to Approximate Hardware Pipelining in Verified High-Level Synthesis
#+author: Yann Herklotz
#+options: H:2 toc:nil
#+columns: %45ITEM %10BEAMER_ENV(Env) %10BEAMER_ACT(Act) %4BEAMER_COL(Col)
#+setupfile: setup.org

** Why HLS is unreliable
** Small Introduction to Coq
** Solution: Formally Verify HLS
*** Vericert
** Current Status of Vericert
* Loop Pipelining
** The Need for Loop Pipelining

# - really useful, or you might say necessary optimisation that HLS performs.

- Main difficulty with having hardware as a target is the need to pipeline loops.

*** Minipage
:PROPERTIES:
:BEAMER_ENV: minipage
:BEAMER_OPT: \textwidth
:END:

**** Original Code
:PROPERTIES:
:BEAMER_ENV: onlyenvNH
:BEAMER_ACT: 1
:END:

#+begin_src c
for (int i = 3; i < N; i++)
    acc[i] = acc[i-3]*c+x[i]*y[i];
#+end_src

**** Transformed code
:PROPERTIES:
:BEAMER_ENV: onlyenvNH
:BEAMER_ACT: 2
:END:

#+attr_latex: :options fontsize=\small,escapeinside=||
#+begin_src c
for (int i = 3; i < N; i++) {
|\sA{1}| x18 = i - 3
|\sR{1}| x16 = load[1, x18]
|\sM{1}| x8 = x16 * x1
|\sR{2}| x12 = load[3, i]
|\sR{3}| x13 = load[2, i]
|\sM{2}| x7 = x12 * x13
|\sA{2}| x11 = x8 + x7
|\sW{1}| store[1, i] = x11
   i = i + 1
}
#+end_src

**** Final DFG
:PROPERTIES:
:BEAMER_ENV: onlyenvNH
:BEAMER_ACT: 3
:END:

#+attr_latex: :options xleftmargin=0.3\textwidth
#+begin_src c
for (int i = 3; i < N; i++) {
#+end_src

#+begin_export latex
\begin{center}
  \begin{tikzpicture}[lnode/.style={circle,draw=black,minimum
      size=4mm,scale=0.7},nlabel/.style={midway,right ,font=\tiny},node distance=1.3cm,shorten
    >=1pt]
    \node[lnode,fill=s1col] (A1) {1};
    \node[lnode,fill=s2col,below of=A1] (R1) {1};
    \node[lnode,fill=s3col,below of=R1] (M1) {1};
    \node[lnode,fill=s2col,right of=A1] (R2) {2};
    \node[lnode,fill=s2col,right of=R2] (R3) {3};
    \node[lnode,fill=s3col,below of=R2,xshift=0.7cm] (M2) {2};
    \node[lnode,fill=s1col,below right of=M1,xshift=0.4cm] (A2) {2};
    \node[lnode,fill=s4col,below of=A2] (W1) {1};

    \draw[->,thick] (A1) -- (R1);
    \draw[->,thick,dashed] (R1) -- (M1);
    \draw[->,thick,dashed] (R2) -- (M2);
    \draw[->,thick,dashed] (R3) -- (M2);
    \draw[->,thick] (M1) -- (A2);
    \draw[->,thick] (M2) -- (A2);
    \draw[->,thick] (A2) -- (W1);
    \draw[->,thick] (W1) to [out=220,in=180,loop,looseness=2] node [midway,right] {3} (R1);
  \end{tikzpicture}
\end{center}
#+end_export

#+beamer: \vspace{-4em}

#+attr_latex: :options xleftmargin=0.3\textwidth
#+begin_src c
}
#+end_src

** Ideas Behind Static Hardware Loop Pipelining

*** One Possible Workflow

- Generate scheduling constraints for linear code as well as loops.
- Solve for a scheduling using an ILP solver.
- Place the instructions into the cycle that it was assigned to.

#+begin_export latex
\begin{center}
  \begin{tikzpicture}[lnode/.style={circle,draw=black,minimum size=4mm,scale=0.8},node
    distance=1.3cm,shorten >=1pt]
    \node[lnode,fill=s1col] (A1) {1}; \node[lnode,fill=s2col,below of=A1] (R2) {2};
    \node[lnode,fill=s2col,below of=R2] (R3) {3}; \node[lnode,fill=s2col,right of=A1] (R1) {1};
    \node[lnode,fill=s3col,right of=R1] (M2) {2}; \node[lnode,fill=s3col,right of=M2] (M1) {1};
    \node[lnode,fill=s1col,right of=M1] (A2) {2}; \node[lnode,right of=A2] (E1) {};
    \node[lnode,fill=s4col,right of=E1] (W1) {1}; \node[lnode,right of=W1] (E2) {}; \node[above
    right of=R1,xshift=-0.35cm] (S1T) {}; \node[below of=S1T,yshift=-2.5cm] (S1B) {}; \draw[very
    thick] (S1T) -- (S1B); \node[above right of=M1,xshift=-0.35cm] (S2T) {}; \node[below
    of=S2T,yshift=-2.5cm] (S2B) {}; \draw[very thick] (S2T) -- (S2B); \node[above right
    of=E1,xshift=-0.35cm] (S3T) {}; \node[below of=S3T,yshift=-2.5cm] (S3B) {}; \draw[very thick]
    (S3T) -- (S3B);
  \end{tikzpicture}
\end{center}
#+end_export

** Verifying Hardware Pipelining is Difficult

- Normally part of the scheduling step.
- Lose control about how the loops are translated, the fundamental structure of the loop could
  change and would be difficult to identify again.

* Verifying Loop Pipelining
** Ideas Behind Software Loop Pipelining

*** Schedule
:PROPERTIES:
:BEAMER_ENV: onlyenvNH
:BEAMER_ACT: 1-4
:END:

In software pipelining we represent a vertical slice of the pipeline.

#+begin_export latex
\begin{center}
  \begin{tikzpicture}[lnode/.style={circle,draw=black,minimum size=4mm,scale=0.4},node
    distance=1cm,shorten >=1pt]
    \node[lnode,fill=s1col] (A1) {1};
    \node[lnode,fill=s2col,below of=A1] (R2) {2};
    \node[lnode,fill=s2col,below of=R2] (R3) {3};
    \node[lnode,fill=s2col,right of=A1] (R1) {1};
    \node[lnode,fill=s3col,right of=R1] (M2) {2};
    \node[lnode,fill=s3col,right of=M2] (M1) {1};
    \node[lnode,fill=s1col,right of=M1] (A2) {2};
    \node[lnode,right of=A2] (E1) {};
    \node[lnode,fill=s4col,right of=E1] (W1) {1};
    \node[lnode,right of=W1] (E2) {};
    \begin{scope}[xshift=0.8cm,yshift=-0.5cm]
      \node[lnode,fill=s1col] (t1A1) {1};
      \node[lnode,fill=s2col,below of=t1A1] (t1R2) {2};
      \node[lnode,fill=s2col,below of=t1R2] (t1R3) {3};
      \node[lnode,fill=s2col,right of=t1A1] (t1R1) {1};
      \node[lnode,fill=s3col,right of=t1R1] (t1M2) {2};
      \node[lnode,fill=s3col,right of=t1M2] (t1M1) {1};
      \node[lnode,fill=s1col,right of=t1M1] (t1A2) {2};
      \node[lnode,right of=t1A2] (t1E1) {};
      \node[lnode,fill=s4col,right of=t1E1] (t1W1) {1};
      \node[lnode,right of=t1W1] (t1E2) {};
    \end{scope}
    \begin{scope}[xshift=1.6cm,yshift=-1cm]
      \node[lnode,fill=s1col] (t2A1) {1};
      \node[lnode,fill=s2col,below of=t2A1] (t2R2) {2};
      \node[lnode,fill=s2col,below of=t2R2] (t2R3) {3};
      \node[lnode,fill=s2col,right of=t2A1] (t2R1) {1};
      \node[lnode,fill=s3col,right of=t2R1] (t2M2) {2};
      \node[lnode,fill=s3col,right of=t2M2] (t2M1) {1};
      \node[lnode,fill=s1col,right of=t2M1] (t2A2) {2};
      \node[lnode,right of=t2A2] (t2E1) {};
      \node[lnode,fill=s4col,right of=t2E1] (t2W1) {1};
      \node[lnode,right of=t2W1] (t2E2) {};
    \end{scope}
    \begin{scope}[xshift=2.4cm,yshift=-1.5cm]
      \node[lnode,fill=s1col] (t3A1) {1};
      \node[lnode,fill=s2col,below of=t3A1] (t3R2) {2};
      \node[lnode,fill=s2col,below of=t3R2] (t3R3) {3};
      \node[lnode,fill=s2col,right of=t3A1] (t3R1) {1};
      \node[lnode,fill=s3col,right of=t3R1] (t3M2) {2};
      \node[lnode,fill=s3col,right of=t3M2] (t3M1) {1};
      \node[lnode,fill=s1col,right of=t3M1] (t3A2) {2};
      \node[lnode,right of=t3A2] (t3E1) {};
      \node[lnode,fill=s4col,right of=t3E1] (t3W1) {1};
      \node[lnode,right of=t3W1] (t3E2) {};
    \end{scope}
    \node[above right of=R1,xshift=-0.5cm] (S1T) {};
    \node[below of=S1T,yshift=-2.8cm] (S1B) {};
    \draw[thick] (S1T) -- (S1B);
    \node[above right of=M1,xshift=-0.5cm] (S2T) {};
    \node[below of=S2T,yshift=-2.8cm] (S2B) {};
    \draw[thick] (S2T) -- (S2B);
    \node[above right of=E1,xshift=-0.5cm] (S3T) {};
    \node[below of=S3T,yshift=-2.8cm] (S3B) {};
    \draw[thick] (S3T) -- (S3B);
    \node[above right of=E2,xshift=-0.5cm] (S4T) {};
    \node[below of=S4T,yshift=-2.8cm] (S4B) {};
    \draw[thick] (S4T) -- (S4B);
    \node[right of=S4T,xshift=-0.2cm] (S5T) {};
    \node[below of=S5T,yshift=-2.8cm] (S5B) {};
    \draw[thick] (S5T) -- (S5B);
    \node[right of=S5T,xshift=-0.2cm] (S6T) {};
    \node[below of=S6T,yshift=-2.8cm] (S6B) {};
    \draw[thick] (S6T) -- (S6B);

    \only<2>{\draw[very thick,red] ($(W1.north west)+(-0.1,0.1)$) rectangle ($(t3R3.south east)+(0.1,-0.1)$);}
    \only<3>{\draw[very thick,red] ($(E2.north west)+(-0.1,0.1)$) rectangle ($(t3R1.south east)+(0.1,-0.1)$);}
    \only<4>{\draw[very thick,red] ($(A1.north west)+(-0.1,0.1)$) rectangle (t3R2.west);}
    \only<4>{\draw[very thick,red] ($(t1W1.north west)+(-0.1,0.1)$) rectangle ($(t3E2.south east)+(0.1,-0.1)$);}
  \end{tikzpicture}
\end{center}
#+end_export

*** Columns
:PROPERTIES:
:BEAMER_ENV: onlyenvNH
:BEAMER_ACT: 5-
:END:

**** Main idea
:PROPERTIES:
:BEAMER_ENV: onlyenvNH
:BEAMER_ACT: 5
:END:

- Source-to-source transformation to generate a *pipeline* in *software*.
- Use *rotating register file* to avoid unrolling due to *modulo variable expansion*.

**** Need to add the epilogue and prologue
:PROPERTIES:
:BEAMER_ENV: onlyenvNH
:BEAMER_ACT: 6
:END:

- Use *predicated execution* to avoid adding explicit prologue and epilogue.

**** Column left
:PROPERTIES:
:BEAMER_COL: 0.45
:END:

***** Initial loop
:PROPERTIES:
:BEAMER_ENV: onlyenvNH
:BEAMER_ACT: 5
:END:

#+attr_latex: :options xleftmargin=0.3\textwidth
#+begin_src c
for (int i = 3; i < N; i++) {
#+end_src

#+begin_export latex
\begin{center}
  \begin{tikzpicture}[lnode/.style={circle,draw=black,minimum
      size=4mm,scale=0.7},nlabel/.style={midway,right ,font=\tiny},node distance=1.3cm,shorten
    >=1pt]
    \node[lnode,fill=s1col] (A1) {1};
    \node[lnode,fill=s2col,below of=A1] (R1) {1};
    \node[lnode,fill=s3col,below of=R1] (M1) {1};
    \node[lnode,fill=s2col,right of=A1] (R2) {2};
    \node[lnode,fill=s2col,right of=R2] (R3) {3};
    \node[lnode,fill=s3col,below of=R2,xshift=0.7cm] (M2) {2};
    \node[lnode,fill=s1col,below right of=M1,xshift=0.4cm] (A2) {2};
    \node[lnode,fill=s4col,below of=A2] (W1) {1};

    \draw[->,thick] (A1) -- (R1);
    \draw[->,thick,dashed] (R1) -- (M1);
    \draw[->,thick,dashed] (R2) -- (M2);
    \draw[->,thick,dashed] (R3) -- (M2);
    \draw[->,thick] (M1) -- (A2);
    \draw[->,thick] (M2) -- (A2);
    \draw[->,thick] (A2) -- (W1);
    \draw[->,thick] (W1) to [out=220,in=180,loop,looseness=2] node [midway,right] {3} (R1);
  \end{tikzpicture}
\end{center}
#+end_export

#+beamer: \vspace{-4em}

#+attr_latex: :options xleftmargin=0.3\textwidth
#+begin_src c
}
#+end_src

***** Execution control
:PROPERTIES:
:BEAMER_ENV: onlyenvNH
:BEAMER_ACT: 6
:END:

#+begin_src c
if (i < N): p0 = true
|| if p0: p1 = true
|| if p1: p2 = true
|| if p2: p3 = true
if (i >= N): p0 = false
|| if !p0: p1 = false
|| if !p1: p2 = false
|| if !p2: p3 = false
#+end_src

**** Column right
:PROPERTIES:
:BEAMER_COL: 0.45
:END:

***** Initial converted
:PROPERTIES:
:BEAMER_ENV: onlyenvNH
:BEAMER_ACT: 5
:END:

#+attr_latex: :options escapeinside=||
#+begin_src c
for (int i = 3; i < N; i++) {
    |\sA{1}|[i]
    |\sR{2}|[i]
    |\sR{3}|[i]
    |\sM{2}|[i-1]
    |\sA{2}|[i-2]
    |\sW{1}|[i-3]

    |\sR{1}|[i]
    |\sM{1}|[i-1]
    i = i + 1
}
#+end_src

***** With predicates
:PROPERTIES:
:BEAMER_ENV: onlyenvNH
:BEAMER_ACT: 6
:END:

#+attr_latex: :options escapeinside=||
#+begin_src c
for (int i = 3; i < N+4; i++) {
    if p0: |\sA{1}|[i]
    if p0: |\sR{2}|[i]
    if p0: |\sR{3}|[i]
    if p1: |\sM{2}|[i-1]
    if p2: |\sA{2}|[i-2]
    if p3: |\sW{1}|[i-3]

    if p0: |\sR{1}|[i]
    if p1: |\sM{1}|[i-1]
    i = i + 1
}
#+end_src

** Use Symbolic Execution to Verify the Transformation

*** Symbolic Execution

Define an $\alpha$, such that $\alpha(\mathcal{C})$ evaluates some code $\mathcal{C}$ and returns
*symbolic states* for all registers.

*** Example
:PROPERTIES:
:BEAMER_ACT: 2-
:END:

Executing the following code will evaluate to the following symbolic code:

#+begin_export latex
\begin{equation*}
\alpha
\left(\begin{aligned}
  & \texttt{x = 2}\\
  & \texttt{y = x + z}
\end{aligned}\right)\qquad
 =\qquad
\begin{aligned}
  &\texttt{x}\mapsto 2\\
  &\texttt{y}\mapsto 2 + \texttt{z}^0
\end{aligned}
\end{equation*}
#+end_export

** Verifying Software Loop Pipelining

For a loop $\mathcal{L}_1$ and a pipelined loop $\mathcal{L}_2$, we want to prove:

#+begin_export latex
\begin{equation*}
  \forall N, \alpha(\mathcal{L}_{1}^{N}) = \alpha(\mathcal{L}_{2}^{N})
\end{equation*}
#+end_export

- This is not feasible as $N$ is often not known statically

*** Actual proof
:PROPERTIES:
:BEAMER_ENV: blockNH
:BEAMER_ACT: 2
:END:

It is enough to prove various static properties:

* Comparing Software and Hardware Loop Pipelining

** Comparing Pipelines in Hardware and Software

*** Representation

- Hardware pipelining :: each instruction is put into a state and it is filled with data at the
  correct II.
- Software pipelining :: the code represents the kernel of the pipeline, expressing each repeating
  instruction.

*** Pipelines themselvs are identical

- In terms of expressivity, both hardware and software pipelining can express the same loop
  pipelines.

** Resource Usage of Pipelines

- With some *hardware support* software pipeline resource usage can get close to hardware pipeline
  resource usage.
- Hardware pipelining is still simpler as filling a pipeline at an II is straightforward.

* Wrapping up
** Conclusion

- Verifying hardware pipelining together with scheduling is difficult.
  + Too many instructions move around and their positions need to be recovered.
- By doing *software pipelining* followed by *instruction scheduling* and *hardware generation*,
  hardware pipelines can be approximated.
  + Same pipeline but with higher resource usage.