diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-07-26 00:02:40 +0200 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-07-26 00:02:40 +0200 |
| commit | fe56f9efb8f9d983a9024383fa17695b347ec67e (patch) | |
| tree | 50637e19ddab1692b1a03ae17b2715bf6aedc9c2 /introduction.tex | |
| parent | 3826f25870abb2725c5c0552ff0ebddd62803ebc (diff) | |
| download | oopsla21_fvhls-fe56f9efb8f9d983a9024383fa17695b347ec67e.tar.gz oopsla21_fvhls-fe56f9efb8f9d983a9024383fa17695b347ec67e.zip | |
Add section clarifying translation validation
Diffstat (limited to 'introduction.tex')
| -rw-r--r-- | introduction.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/introduction.tex b/introduction.tex index cfb99b8..49d8708 100644 --- a/introduction.tex +++ b/introduction.tex @@ -29,7 +29,9 @@ Aware of the reliability shortcomings of HLS tools, hardware designers routinely An alternative is to use \emph{translation validation}~\cite{pnueli98_trans} to prove the input and output equivalent. Translation validation has been successfully applied to several 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}. But translation validation is an expensive task, especially for large designs, and it must be repeated every time the compiler is invoked. -For example, the translation validation for Catapult C~\cite{mentor20_catap_high_level_synth} may require several rounds of expert `adjustments'~\cite[p.~3]{slec_whitepaper} to the input C program before validation succeeds. And even when it succeeds, translation validation does not provide watertight guarantees unless the validator itself has been mechanically proven correct, which is seldom the case. +For example, the translation validation for Catapult C~\cite{mentor20_catap_high_level_synth} may require several rounds of expert `adjustments'~\cite[p.~3]{slec_whitepaper} to the input C program before validation succeeds. And even when it succeeds, translation validation does not provide watertight guarantees unless the validator itself has been mechanically proven correct, which is seldom the case. + +However, translation validation has many benefits in a mechanically verified setting as well to simplify the proofs and depend less on the exact implementation of the optimisation. It has also already been used to prove certain passes in \compcert{} correct. By proving specific optimisations with a constraint on the kinds of transformations it can perform, it is possible to write a verified validator that is also believed to be complete and should not fail on valid transformations unless bugs are present. Our position is that none of the above workarounds are necessary if the HLS tool can simply be trusted to work correctly. |