diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-09-14 21:09:35 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-09-14 21:09:35 +0100 |
| commit | 69c5fdb036c8fdc824fa5d67ce0b4d5f27b8b9ed (patch) | |
| tree | 3b220e6a2cb6c38bf9fa624afb8ba95cce3a4e7e | |
| parent | 0d3fdd26c1997fb11b4a467b2927a0410b5aa328 (diff) | |
| parent | bdff10f26041ab5b1dbb242a1502e815ddf0d0d1 (diff) | |
| download | fccm21_esrhls-69c5fdb036c8fdc824fa5d67ce0b4d5f27b8b9ed.tar.gz fccm21_esrhls-69c5fdb036c8fdc824fa5d67ce0b4d5f27b8b9ed.zip | |
Merge branch 'master' of https://git.overleaf.com/5f2d21b9b10d6c0001c164a4 into master
| -rw-r--r-- | related.tex | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/related.tex b/related.tex index ef3edc1..ce07eba 100644 --- a/related.tex +++ b/related.tex @@ -6,8 +6,7 @@ Other stages of the FPGA toolchain have been subjected to fuzzing. Herklotz et a Several authors have taken steps toward more rigorously engineered HLS tools that may be more resilient to testing campaigns such as ours. One such example might be the Handel-C compiler by Perna and Woodcock~\cite{perna12_mechan_wire_wise_verif_handel_c_synth} which has been mechanically proven correct, at least in part, using the HOL theorem prover. %However, the Handel-C language relies upon the user to perform the parallelisation that is necessary for good hardware performance, and would require many more checks to avoid data races. -Howev -in any case, the tool does not support C as input directly. +However, the tool does not support C as input directly, so is not amenable to fuzzing. Another example is an HLS tool called SPARK~\cite{gupta03_spark}, in which some passes, such as scheduling, are mechanically validated during compilation~\cite{chouksey20_verif_sched_condit_behav_high_level_synth}. Unfortunately, this tool is not readily available yet to test properly. Finally, the HLS tool Catapult C~\cite{mentor20_catap_high_level_synth} is designed only to produce an output netlist if it can mechanically prove it equivalent to the input program. It should therefore never produce wrong RTL. Future work will address testing Catapult-C as well, however, as Vivado HLS, LegUp HLS and Intel HLS are more prevalent these were prioritised. \JW{Obvious reader question at this point: why not test that claim by giving our Csmith test cases to Catapult C too? Can we address that here? No worries if not; but shall we try and do that after the deadline anyway?}\YH{Yes, definitely, it would be great to get an idea of how Catapult C performs, and I currently have it installed already. I have added a small sentence for that now, but let me know if I should mention this in the conclusion instead though. } %%% Local Variables: |