More work

3 files changed, 99 insertions, 1 deletions

diff --git a/draft.org b/draft.org
index 409ee00..423826f 100644
--- a/draft.org
+++ b/draft.org
@@ -1,6 +1,15 @@
 #+title: Paper Outline and Draft
 #+author: Yann Herklotz
 
+** A possible story:
+
+- High-level synthesis is increasingly being relied upon.
+- But it's really flaky. (Cite bugs from FCCM submission etc.)
+- There exist some workarounds. (Testing the output, formally verifying the output, etc.)
+- The time has come to prove the tool itself correct. (Mention success of Compcert and other fully verified tools?)
+- We've made some encouraging progress on this front in a prototype tool called Vericert. (Summarise current state of Vericert, and how it compares performance-wise to LegUp.)
+- But there's still a long way to go. (List the main things left to do, and how you expect Vericert to compare to LegUp after those things are done.)
+
 - Performance vs correctness.
 
 * Introduction
diff --git a/main.tex b/main.tex
index f206dc3..84d9c0d 100644
--- a/main.tex
+++ b/main.tex
@@ -194,7 +194,7 @@ The solution to both of these points is to have a formally verified high-level s
 
 \section{How to prove an HLS tool correct}
 
-The standard methods for checking the outputs of the HLS tools are the following.  First, the output could be checked by using a test bench and checking the outputs against the model.  However, this does not provide many guarantees, and a lot of the
+The standard methods for checking the outputs of the HLS tools are the following.  First, the output could be checked by using a test bench and checking the outputs against the model.  However, this does not provide many guarantees, as many edge cases may never be tested.  Second, if testing is not rigorous enough, there has been research on checking that the generated hardware design has the same functionality as the input design, where the focus is on creating translation validators~\cite{pnueli98_trans} to prove the equivalence between the design and input code, while supporting various optimisations such as scheduling~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth} or code motion~\cite{banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}.  However, these aren't perfect solutions either, as there is no guarantee that these proofs really compose with each other.  In addition to that, these translation validation tools
 
 \paragraph{How could such a tool be constructed?}
 
diff --git a/references.bib b/references.bib
index 24b1f75..242532b 100644
--- a/references.bib
+++ b/references.bib
@@ -87,3 +87,92 @@
 	numpages = 9,
 	publisher = {ACM}
 }
+
+@inproceedings{kim04_autom_fsmd,
+	author = { {Youngsik Kim} and S. {Kopuri} and N. {Mansouri}},
+	title = {Automated formal verification of scheduling process using finite state machines with datapath (FSMD)},
+	tags = {hls, verification},
+	booktitle = {International Symposium on Signals, Circuits and Systems. Proceedings, SCS 2003. (Cat. No.03EX720)},
+	year = 2004,
+	pages = {110-115},
+	doi = {10.1109/ISQED.2004.1283659},
+	url = {https://doi.org/10.1109/ISQED.2004.1283659},
+	ISSN = {null},
+	month = {March}
+}
+
+@inproceedings{karfa06_formal_verif_method_sched_high_synth,
+	author = {Karfa, C and Mandal, C and Sarkar, D and Pentakota, S R. and
+                  Reade, Chris},
+	title = {A Formal Verification Method of Scheduling in High-level Synthesis},
+	tags = {hls},
+	booktitle = {Proceedings of the 7th International Symposium on Quality Electronic Design},
+	year = 2006,
+	pages = {71--78},
+	doi = {10.1109/ISQED.2006.10},
+	url = {https://doi.org/10.1109/ISQED.2006.10},
+	acmid = 1126731,
+	address = {Washington, DC, USA},
+	isbn = {0-7695-2523-7},
+	numpages = 8,
+	publisher = {IEEE Computer Society},
+	series = {ISQED '06}
+}
+
+@article{chouksey20_verif_sched_condit_behav_high_level_synth,
+	author = {R. {Chouksey} and C. {Karfa}},
+	title = {Verification of Scheduling of Conditional Behaviors in High-Level Synthesis},
+	journal = {IEEE Transactions on Very Large Scale Integration (VLSI) Systems},
+	volume = {},
+	number = {},
+	pages = {1-14},
+	year = {2020},
+	doi = {10.1109/TVLSI.2020.2978242},
+	url = {https://doi.org/10.1109/TVLSI.2020.2978242},
+	ISSN = {1557-9999},
+	month = {}
+}
+
+@article{banerjee14_verif_code_motion_techn_using_value_propag,
+	author = {K. {Banerjee} and C. {Karfa} and D. {Sarkar} and C. {Mandal}},
+	title = {Verification of Code Motion Techniques Using Value Propagation},
+	tags = {hls, verification},
+	journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
+	volume = 33,
+	number = 8,
+	pages = {1180-1193},
+	year = 2014,
+	doi = {10.1109/TCAD.2014.2314392},
+	url = {https://doi.org/10.1109/TCAD.2014.2314392},
+	ISSN = {1937-4151},
+	keywords = {translation validation, compiler optimisation, verification, high-level synthesis},
+	month = {Aug}
+}
+
+@article{chouksey19_trans_valid_code_motion_trans_invol_loops,
+	author = {R. {Chouksey} and C. {Karfa} and P. {Bhaduri}},
+	title = {Translation Validation of Code Motion Transformations Involving Loops},
+	tags = {hls, verification},
+	journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
+	volume = 38,
+	number = 7,
+	pages = {1378-1382},
+	year = 2019,
+	doi = {10.1109/TCAD.2018.2846654},
+	url = {https://doi.org/10.1109/TCAD.2018.2846654},
+	ISSN = {1937-4151},
+	keywords = {translation validation, verification, compiler optimisation, high-level synthesis},
+	month = {July}
+}
+
+@inproceedings{pnueli98_trans,
+	author = "Pnueli, A.  and Siegel, M.  and Singerman, E.",
+	title = "Translation validation",
+	booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
+	year = 1998,
+	pages = "151--166",
+	address = "Berlin, Heidelberg",
+	editor = "Steffen, Bernhard",
+	isbn = "978-3-540-69753-4",
+	publisher = "Springer Berlin Heidelberg"
+}