Update on Overleaf.

3 files changed, 25 insertions, 9 deletions

diff --git a/algorithm.tex b/algorithm.tex
index b731dfc..3c33757 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -8,7 +8,7 @@ First of all, the choice of C as the input language of \vericert{} is simply bec
 %Since a lot of existing code for HLS is written in C, supporting C as an input language, rather than a custom domain-specific language, means that \vericert{} is more practical. 
 %An alternative was to support LLVM IR as an input language, however, to get a full work flow from a higher level language to hardware, a front end for that language to LLVM IR would also have to be verified. \JW{Maybe save LLVM for the `Choice of implementation language'?}
 We considered Bluespec~\cite{nikhil04_blues_system_veril}, but decided that although it ``can be classed as a high-level language''~\cite{greaves_note}, it is too hardware-oriented to be used for traditional HLS.
-We also considered using a language with built-in parallel constructs that map well to parallel hardware, such as occam~\cite{page91_compil_occam} or Spatial~\cite{spatial}, but found these languages too niche.
+We also considered using a language with built-in parallel constructs that map well to parallel hardware, such as occam~\cite{page91_compil_occam}, Spatial~\cite{spatial} or Scala~\cite{chisel}, but we found these languages too niche.
 % However, this would not qualify as being HLS due to the manual parallelism that would have to be performed. \JW{I don't think the presence of parallelism stops it being proper HLS.} 
 %\JP{I think I agree with Yann here, but it could be worded better. At any rate not many people have experience writing what is essentially syntactic sugar over a process calculus.} 
 %\JW{I mean: there are plenty of software languages that involve parallel constructs. Anyway, perhaps we can just dismiss occam for being too obscure.}
diff --git a/references.bib b/references.bib
index 982434f..d4cd81f 100644
--- a/references.bib
+++ b/references.bib
@@ -820,3 +820,22 @@ year = {2020},
   note            = {unpublished},
   title           = {Fuzzing High-Level Synthesis Tools},
 }
+
+
+@inproceedings{kiwi_hls,
+  title={Kiwi: Synthesis of FPGA circuits from parallel programs},
+  author={Singh, Satnam and Greaves, David J},
+  booktitle={2008 16th International Symposium on Field-Programmable Custom Computing Machines},
+  pages={3--12},
+  year={2008},
+  organization={IEEE}
+}
+
+@inproceedings{chisel,
+  title={Chisel: constructing hardware in a scala embedded language},
+  author={Bachrach, Jonathan and Vo, Huy and Richards, Brian and Lee, Yunsup and Waterman, Andrew and Avi{\v{z}}ienis, Rimas and Wawrzynek, John and Asanovi{\'c}, Krste},
+  booktitle={DAC Design Automation Conference 2012},
+  pages={1212--1221},
+  year={2012},
+  organization={IEEE}
+}
\ No newline at end of file
diff --git a/verilog.tex b/verilog.tex
index de9da13..79964ee 100644
--- a/verilog.tex
+++ b/verilog.tex
@@ -18,18 +18,15 @@ An example of a rule for executing an \alwaysblock{} is shown below, where $\Sig
   \inferrule[Always]{(\Sigma, s)\downarrow_{\text{stmnt}} \Sigma'}{(\Sigma, \yhkeyword{always @(posedge clk) } s) \downarrow_{\text{always}} \Sigma'}
 \end{equation*}
 
-\noindent which shows that assuming the statement $s$ in the \alwaysblock{} runs with state $\Sigma$ and produces the new state $\Sigma'$, the \alwaysblock{} will result in the same final state.  As only clocked \alwaysblock{} are supported, and one step in the semantics correspond to one clock cycle, it means that this rule is run once per clock cycle for each \alwaysblock{}.
-
-Two types of assignments are supported in \alwaysblock{}: nonblocking and blocking assignment.  Nonblocking assignment modifies the signal at the end of the clock cycle and atomically.  Blocking assignment, on the other hand, assigns the variable instantaneously in the \alwaysblock{} for later signals to pick up.  To model both these assignments, the state $\Sigma$ has to be split into two maps: $\Gamma$, containing the current values of all variables, and $\Delta$, containing the values that will be assigned to the variables at the end of the clock cycle, we can therefore say that $\Sigma = (\Gamma, \Delta)$.  The nonblocking assignment can therefore be expressed as the following:
-
-%~\NR{Can we say that $\Gamma$ contains instantaneous (ephemeral) updates for the current cycle and $\Delta$ contains periodical updates for the next cycle? Will be good to distinguish those two updates with the same terms across the paper, which can tie in with small-step and big-step distinction maybe asynchronous vs synchronous updates. }\YH{Hmm, so I don't think nonblocking and blocking ties in with big-step and smallstep, but yes it would be better to use the same terms throughoug the paper}
+\noindent This rule says that assuming the statement $s$ in the \alwaysblock{} runs with state $\Sigma$ and produces the new state $\Sigma'$, the \alwaysblock{} will result in the same final state.  %Since only clocked \alwaysblock{} are supported, and one step in the semantics correspond to one clock cycle, it means that this rule is run once per clock cycle for each \alwaysblock{}.
 
+Two types of assignments are supported in \alwaysblock{}s: nonblocking and blocking assignment.  Nonblocking assignments all take effect simultaneously at the end of the clock cycle, %and atomically.
+while blocking assignments happen instantly so that later assignments in the clock cycle can pick them up.  To model both of these assignments, the state $\Sigma$ has to be split into two maps: $\Gamma$, which contains the current values of all variables, and $\Delta$, which contains the values that will be assigned at the end of the clock cycle. %, we can therefore say that $\Sigma = (\Gamma, \Delta)$. 
+Nonblocking assignment can therefore be expressed as follows:
 \begin{equation*}
   \inferrule[Nonblocking Reg]{\yhkeyword{name}\ d = \yhkeyword{OK}\ n \\ (\Gamma, e) \downarrow_{\text{expr}} v}{((\Gamma, \Delta), d\ \yhkeyword{ <= } e) \downarrow_{\text{stmnt}} (\Gamma, \Delta [n \mapsto v])}\\
 \end{equation*}
-
-\noindent where assuming that $\downarrow_{\text{expr}}$ evaluates an expression $e$ to a value $v$, then the nonblocking assignment $d\ \yhkeyword{ <= } e$ will update the future state of the variable $d$ with value $v$.  Finally, at the end of the clock cycle, the registers need to be updated with their future values in $\Delta$, which can be shown by the rule in the semantics that runs a whole module, $\vec{m}$ is a list of variable declarations and \alwaysblock{}s, and the $\downarrow_{\vec{m}}$ evaluates these sequentially and obtains the final state $(\Gamma', \Delta')$.
-%\JW{I'm a little torn. On the one hand, this is interesting stuff, and I almost want to suggest putting in the `Blocking Reg' rule alongside the one above, because seeing the rules side-by-side makes it really clear how they both work. But I'm conscious that talking about the distinction between non-blocking and blocking assignments is all a bit moot because Vericert never produces blocking assignments (right?). And this text is all just explaining Loow's work, not your own work. So, in short, I'm a bit torn. Probably best to keep it as-is for now, but bear this in mind as a candidate for chopping nearer the deadline. What do yout think?}
+where assuming that $\downarrow_{\text{expr}}$ evaluates an expression $e$ to a value $v$, then the nonblocking assignment $d\ \yhkeyword{ <= } e$ will update the future state of the variable $d$ with value $v$.  Finally, at the end of the clock cycle, the registers need to be updated with their future values in $\Delta$, which can be shown by the rule in the semantics that runs a whole module, $\vec{m}$ is a list of variable declarations and \alwaysblock{}s, and the $\downarrow_{\vec{m}}$ evaluates these sequentially and obtains the final state $(\Gamma', \Delta')$.
 
 
 \begin{equation*}