From 428e424b75999eda16f5c5ccb4ee48763d99c9d1 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 3 May 2022 23:20:21 +0100
Subject: Add section on discussion of hardware pipelining

---
 chapters/pipelining.tex | 62 +++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 58 insertions(+), 4 deletions(-)

(limited to 'chapters/pipelining.tex')

diff --git a/chapters/pipelining.tex b/chapters/pipelining.tex
index 5aa03dc..26ed8c3 100644
--- a/chapters/pipelining.tex
+++ b/chapters/pipelining.tex
@@ -97,17 +97,71 @@ semantics.  Essentially, as the loop pipelining algorithm only modifies loops, i
 that the input loop $X$ is equivalent to the pipelined version of the loop $Y$.  Assuming that the
 validation algorithm is called $\alpha$, we therefore want to show that the following statement
 holds, where $X_N$ means that we are considering $N$ iterations of the loop.
+
 \placeformula\startformula
   \forall N,\quad \alpha(X_N) = \startmathcases
     \NC \alpha(Y_{N/\delta}; X_{N\%\delta}) \NC N \ge \mu \NR
     \NC \alpha(X_N) \NC \text{otherwise} \NR
 \stopmathcases\stopformula
 
-This states that for any number of iteration of the loop X, the formula should hold.  As the number
-of loop iterations $N$ are not always known at compile time, this may become an infinite property
-that needs to be checked.
+This states that for any number of iteration of the loop $X$, the formula should hold.  As the
+number of loop iterations $N$ are not always known at compile time, this may become an infinite
+property that needs to be checked.
+
+This infinite property can be proven by checking smaller finite properties that loop pipelining
+should ensure.  The two key insights that \cite[authors][tristan10_simpl_verif_valid_softw_pipel]
+found where that mainly only the two following properties needed to be checked:
 
-\startmode[section]
+\placeformula\startformula
+\alpha(\mathcal{S}; \mathcal{E}) = \alpha(\mathcal{E}; \mathcal{B}^{\delta})
+\stopformula
+
+\placeformula\startformula
+\alpha(\mathcal{S}; \mathcal{E}) = \alpha(\mathcal{E}; \mathcal{B}^{\delta})
+\stopformula
+
+\noindent In addition to some simpler properties, this means that the infinite property can still be
+checked.
+
+Finally, the verifier itself needs to be proven correct, meaning the correctness of the symbolic
+evaluation needs to be shown to be semantics preserving.  If the comparison between two symbolic
+states succeeds, then this must imply that the initial blocks themselves execute in the same way.
+
+\section{Hardware and Software Pipelining}
+
+Hardware and software pipelining algorithms have a lot of commonalities, even though the way the
+pipeline is implemented in the end differs.
+
+Pipelining in hardware is intuitive.  If one has two separate blocks where one is data-dependent on
+the other, then it is natural to start executing the first block once it has finished and passed the
+result to the second block.  This idea is also the key building block for processor designs, as it
+is a straightforward way to improve the throughput of a series of distinct and dependent operations.
+In \HLS\ it is also an important optimisation to efficiently translate loops.  As these are often
+executed many times, any improvements can reduce the throughput of the entire design.  The \HLS\
+tool therefore often automatically creates pipeline stages for loops and calculates a correct \II\
+for the loop, which will be the rate at which the pipeline needs to be filled.  The benefit though
+of generating hardware directly, is that the pipeline can already be laid out in the optimal and
+natural way.
+
+It is less clear why, and especially how, software can be pipelined in the same way as hardware, and
+what the benefits are if the code is going to be executed.  The main difference between the hardware
+pipeline is that in software one inherently only following one control-flow through the program.
+This means that it is not possible to lay out a pipeline in the same way as it is done in hardware
+to improve the throughput of loops.  However, a pipeline can be simulated in software, so that it
+behaves the same as the hardware pipeline, but it will manually have to unroll the loop so that all
+the stages can be executed by following one control-flow.  However, the inherent order of
+instructions will be quite different to the order of the pipeline stages in hardware.  In hardware,
+the pipeline can be written naturally in sequential order, and then the \II\ contract is fulfilled
+by setting the rate at which the pipeline is filled.  However, in software, one horizontal slice of
+the pipeline needs to be extracted and will be the new loop body, which represents the computation
+that the whole hardware pipeline is performing at one point in time.
+
+The main question that comes up is are the two pipelining methods actually equivalent?  In Vericert
+we are assuming that performing software pipelining, followed by scheduling and finally followed by
+the hardware generation approximates the hardware pipelining that traditional \HLS\ tools perform as
+part of their hardware generation.
+
+\startmode[chapter]
   \section{Bibliography}
   \placelistofpublications
 \stopmode
-- 
cgit 

