diff options
| author | John Wickerson <j.wickerson@imperial.ac.uk> | 2021-01-19 12:56:09 +0000 |
|---|---|---|
| committer | overleaf <overleaf@localhost> | 2021-01-19 16:03:12 +0000 |
| commit | 92cd0135488bd6b4a6f27197850d8d56a0f66a62 (patch) | |
| tree | 02dc15d80552fc2b8e34584eccc92a4ee0a2664e /related.tex | |
| parent | 2f50894d316ee27a7bf10b61358bbe2e6a1afbb0 (diff) | |
| download | oopsla21_fvhls-92cd0135488bd6b4a6f27197850d8d56a0f66a62.tar.gz oopsla21_fvhls-92cd0135488bd6b4a6f27197850d8d56a0f66a62.zip | |
Update on Overleaf.
Diffstat (limited to 'related.tex')
| -rw-r--r-- | related.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/related.tex b/related.tex index e0cefa3..0ab67ce 100644 --- a/related.tex +++ b/related.tex @@ -39,10 +39,10 @@ \node at (2.1,4.1) {\color{colorhighlevel}\strut High-level software input}; \end{tikzpicture} - \caption{Summary of related work}\label{fig:related_venn} + \caption{Summary of related work}\label{fig:related_euler} \end{figure} -A summary of the related works can be found in Figure~\ref{fig:related_venn}, which is represented as a Venn diagram. The categories that were chosen for the Venn diagram are: if the tool is usable and available, if it takes a high-level software language as input, if it has a correctness proof and finally if that proof is mechanised. The goal of \vericert{} is to cover all of these categories. +A summary of the related works can be found in Figure~\ref{fig:related_euler}, which is represented as an Euler diagram. The categories that were chosen for the Euler diagram are: if the tool is usable and available, if it takes a high-level software language as input, if it has a correctness proof and finally if that proof is mechanised. The goal of \vericert{} is to cover all of these categories. Most practical HLS tools~\cite{canis11_legup,xilinx20_vivad_high_synth,intel20_sdk_openc_applic,nigam20_predic_accel_desig_time_sensit_affin_types} fit into the category of usable tools that take high-level inputs. On the other spectrum, there are tools such as BEDROC~\cite{chapman92_verif_bedroc} for which there is no practical tool, and even though it is described as high-level synthesis, it more closely resembles today's hardware synthesis tools. |