From f7e372cacdc85498828fb9f0fc3ea86099f9301e Mon Sep 17 00:00:00 2001 From: John Wickerson Date: Tue, 3 Aug 2021 11:34:42 +0000 Subject: Update on Overleaf. --- related.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'related.tex') diff --git a/related.tex b/related.tex index c2cd8ff..29c335d 100644 --- a/related.tex +++ b/related.tex @@ -42,7 +42,7 @@ \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_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. +A summary of the related works can be found in Figure~\ref{fig:related_euler}, which is represented as an Euler diagram. The categories chosen for the Euler diagram are: whether the tool is usable \JWcouldcut{and available}, whether it takes a high-level software language as input, whether it has a correctness proof, and finally whether that proof is mechanised. The goal of \vericert{} is to cover all of these categories. Most practical HLS tools~\citep{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~\citep{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. -- cgit