summaryrefslogtreecommitdiffstats
path: root/related.tex
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-06-25 22:52:47 +0100
committerYann Herklotz <git@yannherklotz.com>2020-06-25 22:52:47 +0100
commitf67483e75b91133b23f710e97110ede47121b9b9 (patch)
tree11c1ef65b1ad1fcb6d20da9f0afb811a466b9717 /related.tex
parent2692815675fa33c146dc0be79ff3b4d982646e9d (diff)
downloadoopsla21_fvhls-f67483e75b91133b23f710e97110ede47121b9b9.tar.gz
oopsla21_fvhls-f67483e75b91133b23f710e97110ede47121b9b9.zip
Separate tex file into separate files
Diffstat (limited to 'related.tex')
-rw-r--r--related.tex15
1 files changed, 15 insertions, 0 deletions
diff --git a/related.tex b/related.tex
new file mode 100644
index 0000000..335aa8d
--- /dev/null
+++ b/related.tex
@@ -0,0 +1,15 @@
+\section{Related Work}
+
+\JW{Some papers to cite somewhere:
+\begin{itemize}
+ \item \citet{kundu08_valid_high_level_synth} have done translation validation on an HLS tool called SPARK. They don't have \emph{very} strong evidence that HLS tools are buggy; they just say ``HLS tools are large and complex software systems, often with hundreds of
+thousands of lines of code, and as with any software of this scale, they are prone
+to logical and implementation errors''. They did, however, find two bugs in SPARK as a result of their efforts, so that provides a small bit of evidence that HLS tools are buggy. \@
+ \item \citet{chapman92_verif_bedroc} have proved (manually, as far as JW can tell) that the front-end and scheduler of the BEDROC synthesis system is correct. (NB:\@ Chapman also wrote a PhD thesis about this (1994) but it doesn't appear to be online.)
+ \item \citet{ellis08} wrote a PhD thesis that was supervised by Cliff Jones whom you met at the VeTSS workshop thing last year. At a high level, it's about verifying a high-level synthesis tool using Isabelle, so very relevant to this project, though scanning through the pdf, it's quite hard to ascertain exactly what the contributions are. Strange that they never published a paper about the work -- it makes it very hard to find!
+\end{itemize}
+}
+
+\YH{Amazing, thank you, yes it seems like Kundu \textit{et al.} have quite a few papers on formal verification of HLS algorithms using translation validation, as well as~\citet{karfa06_formal_verif_method_sched_high_synth}, all using the SPARK~\cite{gupta03_spark} synthesis tool. And yes thank you, will definitely cite that paper. There seem to be similar early proofs of high-level synthesis like \citet{hwang91_formal_approac_to_sched_probl} or \citet{grass94_high}. There are also the Occam papers that I need to mention too, like \citet{page91_compil_occam}, \citet{jifeng93_towar}, \citet{perna11_correc_hardw_synth} and \citet{perna12_mechan_wire_wise_verif_handel_c_synth}.}
+\JW{Well it's a good job there's no page limit on bibliographies these days then! I'll keep an eye out for more papers we could cite when I get a free moment. (No need to cite \emph{everything} of course.)}
+\YH{Yes that's true, there are too many to cite! And great thank you, that would help a lot, I have quite a few papers I still want to cite, but have to think about where they will fit in.}