diff options
Diffstat (limited to 'main.tex')
| -rw-r--r-- | main.tex | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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?} |