diff options
Diffstat (limited to 'introduction.tex')
| -rw-r--r-- | introduction.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/introduction.tex b/introduction.tex index 3895fe4..a71f9a2 100644 --- a/introduction.tex +++ b/introduction.tex @@ -74,7 +74,7 @@ Meanwhile, Xilinx's Vivado HLS has been shown to apply pipelining optimisations \subsection{Existing verification workarounds} It is rather difficult to exhaustively test a HLS tool to prove for the absence of bugs since these codebases are very large and often include custom passes and directives. -Hence, most existing work on verifying HLS tools focus on proving that HLS-generated hardware is equivalent to its software counterpart for all possible inputs of the program, as known as translation validation~\cite{pnueli98_trans}. +Hence, most existing work on verifying HLS tools focus on proving that HLS-generated hardware is equivalent to its software counterpart for all possible inputs of the program, or \emph{translation validation}~\cite{pnueli98_trans}. Translation validation has been successfully applied to many HLS optimisations~\cite{kim04_autom_fsmd,karfa06_formal_verif_method_sched_high_synth,chouksey20_verif_sched_condit_behav_high_level_synth,banerjee14_verif_code_motion_techn_using_value_propag,chouksey19_trans_valid_code_motion_trans_invol_loops}. However, translation validation often suffers from one key problem: the validator itself might not have been mechanically proven to be correct and even it is proven there can be an interpretation gap between the mechanised proof and its implementation. Furthermore, translation validation also has other practical problems: it needs to be invoked everytime a new program is compiled and it can also lead to exponential growth in state space. |