summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-10 15:46:02 +0100
committerYann Herklotz <git@yannherklotz.com>2021-09-10 15:46:02 +0100
commita61f0a5b3a4664f2e1f42e788cc195a7d56ade28 (patch)
treedb56fb1c2ee34e2834ea90bb5743f8bd5977a397
parentc53674cda775192d380e1423706b66d4b7c6050c (diff)
downloadoopsla21_fvhls-a61f0a5b3a4664f2e1f42e788cc195a7d56ade28.tar.gz
oopsla21_fvhls-a61f0a5b3a4664f2e1f42e788cc195a7d56ade28.zip
Make the diagram larger and add copyright
-rw-r--r--algorithm.tex6
-rw-r--r--main.tex5
2 files changed, 6 insertions, 5 deletions
diff --git a/algorithm.tex b/algorithm.tex
index a4941d5..0182d70 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -35,7 +35,7 @@ The .NET framework has been used as a basis for other HLS tools, such as Kiwi~\c
continuation/.style={},
linecount/.style={rounded corners=3pt,dashed}]
\fill[compcert,rounded corners=3pt] (-1,-0.5) rectangle (9.9,2);
- \fill[formalhls,rounded corners=3pt] (-1,-1) rectangle (9.9,-2);
+ \fill[formalhls,rounded corners=3pt] (-1,-1) rectangle (9.9,-2.4);
%\draw[linecount] (-0.95,-0.45) rectangle (3.6,1);
%\draw[linecount] (4,-0.45) rectangle (7.5,1);
\node[language] at (-0.3,0) (clight) {Clight};
@@ -54,7 +54,7 @@ The .NET framework has been used as a basis for other HLS tools, such as Kiwi~\c
%%\node[anchor=west] at (-0.9,0.7) {\small $\sim$ 27 kloc};
%%\node[anchor=west] at (4.1,0.7) {\small $\sim$ 46 kloc};
%%\node[anchor=west] at (2,-1.5) {\small $\sim$ 17 kloc};
- \node[align=center] at (3.5,-2.4) {\footnotesize RAM\\[-0.5em]\footnotesize insertion};
+ \node[align=center] at (3.2,-2) {\footnotesize RAM\\[-0.5em]\footnotesize insertion};
\draw[->,thick] (clight) -- (conta);
\draw[->,thick] (conta) -- (cminor);
\draw[->,thick] (cminor) -- (rtl);
@@ -67,7 +67,7 @@ The .NET framework has been used as a basis for other HLS tools, such as Kiwi~\c
\draw[->,thick] (htl) -- (verilog);
\draw[->,thick] (htl.west) to [out=180,in=150] (4,-2.2) to [out=330,in=270] (htl.south);
\end{tikzpicture}%}
- \caption{\vericert{} as a Verilog back end to \compcert{}. \JW{The placement of the `RAM insertion' label suggests that it's not part of Vericert. Maybe move it inside the orange rectangle?}}%
+ \caption{\vericert{} as a Verilog back end to \compcert{}.}%
\label{fig:rtlbranch}
\end{figure}
diff --git a/main.tex b/main.tex
index 9330e10..3bb0c86 100644
--- a/main.tex
+++ b/main.tex
@@ -46,7 +46,8 @@
%%% 'Formal Verification of High-Level Synthesis'
%%% by Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson.
%%%
-\setcopyright{rightsretained}
+
+\setcopyright{acmlicensed}
\acmPrice{}
\acmDOI{10.1145/3485494}
\acmYear{2021}
@@ -216,7 +217,7 @@
We would like to thank Sandrine Blazy, Jianyi Cheng, Alastair Donaldson, Andreas Lööw, and the
anonymous reviewers for their helpful feedback. This work was financially supported by the EPSRC
via the Research Institute for Verified Trustworthy Software Systems (VeTSS) and the IRIS
- Programme Grant (EP/R006865/1).
+ Programme Grant (EP/R006865/1) as well as EP/P010040/1.
\end{acks}
%% Bibliography