various

1 files changed, 5 insertions, 1 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index fcc9dc7..ecb0a4c 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -104,6 +104,8 @@ Vericert branches off from CompCert at the intermediate language called \emph{re
 
 In the 3AC language, each function in the program is represented as a numbered list of instructions with gotos -- essentially, a control-flow graph (CFG). The essence of Vericert's compilation strategy is to treat this CFG as a state machine, with each instruction in the CFG becoming a state, and each edge in the CFG becoming a transition. Moreover, program variables that do not have their address taken are mapped to hardware registers; other variables (including arrays and structs) are allocated in a block of RAM that represents the stack. More precisely, Vericert builds a \emph{finite state machine with datapath} (FSMD). This comprises two maps, both of which take the current state as their input: the \emph{control logic} map for determining the next state, and a \emph{datapath} map for updating the RAM and registers. These state machines are captured in Vericert's new intermediate language, HTL. When Vericert compiles from HTL to the final Verilog output, these maps are converted from proper `mathematical' functions into syntactic Verilog case-statements, and each is placed inside an always-block.
 
+The overall Vericert flow is shown at the top of Figure~\ref{fig:flow}. The key point to note here is the `inlining' step, which folds all function definitions into their call sites. This allows Vericert to make the simplifying assumption that there is only a single CFG, but has the unwanted effect of duplicating hardware. In this work, we remove some of this inlining and hence some of the duplication.
+
 \begin{figure}
 
 \definecolor{colorflow}{HTML}{8EB85B}
@@ -181,7 +183,9 @@ tit/.style={anchor=north west, font=\tt},
 edlab/.style={auto, inner sep=2pt, align=left, font=\tt}
 }
 
-Figure~\ref{fig:example_C} shows a simple C file that we shall employ as a worked example. Each instruction is colour-coded so it can be tracked through the compilation stages.
+In this section, we shall explain the implementation of Vericert-Fun with the aid of the worked example shown in Figure~\ref{fig:example_C}. The basic idea is shown at the bottom of Figure~\ref{fig:flow}. \JW{Add more text here to explain the rough idea of Vericert-Fun.}
+
+We shall use the small C program in Figure~\ref{fig:example_C} as a worked example. Note that each instruction is colour-coded so it can be tracked through the compilation stages.
 
 \begin{figure}
 \centering