diff options
| -rw-r--r-- | main.tex | 6 | ||||
| -rw-r--r-- | references.bib | 150 |
2 files changed, 155 insertions, 1 deletions
@@ -181,10 +181,14 @@ However, the fact that the behaviour is preserved after HLS cannot be guaranteed %% Current work in formal verification of HLS -Therefore, work is being done to prove the equivalence between the generated hardware and the original behavioural description in C. An example of a tool that implements this is Mentor's Catapult~\cite{mentor20_catap_high_level_synth}, which tries to match the states in the register transfer level (RTL) description to states in the original C code after an unverified translation. This has also been the approach that is taken by +Therefore, work is being done to prove the equivalence between the generated hardware and the original behavioural description in C. An example of a tool that implements this is Mentor's Catapult~\cite{mentor20_catap_high_level_synth}, which tries to match the states in the register transfer level (RTL) description to states in the original C code after an unverified translation. This technique is called translation validation~\cite{pnueli98_trans}, whereby the translation that the HLS tool performed is proven to have been correct for that input, by showing that they behave in the same way for all possible inputs. Using translation validation is quite effective for proving complex 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, the validation has to be run every time the high-level synthesis is performed. In addition to that, the proofs are often not mechanised or directly related to the actual implementation, meaning the verifying algorithm might be wrong and could give false positives or false negatives. + +CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has been written and formally verified in the Coq theorem prover~\cite{bertot04_inter_theor_provin_progr_devel}. First of all, most of the proofs in CompCert have been formally verified directly, meaning that once the compiler is built, the proofs can be erased as the algorithm has been shown to be correct independent of the input. However, some optimisations in CompCert have also been proven using translation validation~\cite{tristan08_formal_verif_trans_valid}, in which case the proof still happens at runtime. The difference is that in this case, the verifier itself is actually formally verified in Coq and is therefore proven that it will only ever say that the input and output are equivalent if that is actually the case. %% Contributions of paper +Using CompCert, we can therefore build a fully verified high-level synthesis tool written in Coq + \section{Background} \subsection{Verilog} diff --git a/references.bib b/references.bib index 63a9f94..82bba12 100644 --- a/references.bib +++ b/references.bib @@ -83,3 +83,153 @@ urldate = {2020-06-06}, year = 2020, } + +@inproceedings{gupta03_spark, + author = {S. {Gupta} and N. {Dutt} and R. {Gupta} and A. {Nicolau}}, + title = {{SPARK}: a high-level synthesis framework for applying parallelizing compiler + transformations}, + booktitle = {16th International Conference on VLSI Design, 2003. Proceedings.}, + year = 2003, + pages = {461-466}, + doi = {10.1109/ICVD.2003.1183177}, + url = {https://doi.org/10.1109/ICVD.2003.1183177}, + ISSN = {1063-9667}, + month = {Jan}, +} + +@article{chouksey20_verif_sched_condit_behav_high_level_synth, + author = {R. {Chouksey} and C. {Karfa}}, + title = {Verification of Scheduling of Conditional Behaviors in + High-Level Synthesis}, + journal = {IEEE Transactions on Very Large Scale Integration (VLSI) + Systems}, + volume = {}, + number = {}, + pages = {1-14}, + year = {2020}, + doi = {10.1109/TVLSI.2020.2978242}, + url = {https://doi.org/10.1109/TVLSI.2020.2978242}, + ISSN = {1557-9999}, + month = {}, +} + +@inproceedings{pnueli98_trans, + author = "Pnueli, A. and Siegel, M. and Singerman, E.", + title = "Translation validation", + booktitle = "Tools and Algorithms for the Construction and Analysis of Systems", + year = 1998, + pages = "151--166", + address = "Berlin, Heidelberg", + editor = "Steffen, Bernhard", + isbn = "978-3-540-69753-4", + publisher = "Springer", +} + +@article{chouksey19_trans_valid_code_motion_trans_invol_loops, + author = {R. {Chouksey} and C. {Karfa} and P. {Bhaduri}}, + title = {Translation Validation of Code Motion Transformations + Involving Loops}, + journal = {IEEE Transactions on Computer-Aided Design of Integrated + Circuits and Systems}, + volume = 38, + number = 7, + pages = {1378-1382}, + year = 2019, + doi = {10.1109/TCAD.2018.2846654}, + ISSN = {1937-4151}, + month = {July}, +} + +@article{banerjee14_verif_code_motion_techn_using_value_propag, + author = {K. {Banerjee} and C. {Karfa} and D. {Sarkar} and C. {Mandal}}, + title = {Verification of Code Motion Techniques Using Value + Propagation}, + journal = {IEEE Transactions on Computer-Aided Design of Integrated + Circuits and Systems}, + volume = 33, + number = 8, + pages = {1180-1193}, + year = 2014, + doi = {10.1109/TCAD.2014.2314392}, + ISSN = {1937-4151}, + month = {Aug} +} + +@inproceedings{kim04_autom_fsmd, + author = { {Youngsik Kim} and S. {Kopuri} and N. {Mansouri}}, + title = {Automated formal verification of scheduling process using + finite state machines with datapath (FSMD)}, + tags = {hls, verification}, + booktitle = {International Symposium on Signals, Circuits and + Systems. Proceedings, SCS 2003. (Cat. No.03EX720)}, + year = 2004, + pages = {110-115}, + doi = {10.1109/ISQED.2004.1283659}, + month = {March} +} + +@inproceedings{karfa06_formal_verif_method_sched_high_synth, + author = {Karfa, C and Mandal, C and Sarkar, D and Pentakota, S R. and + Reade, Chris}, + title = {A Formal Verification Method of Scheduling in High-level + Synthesis}, + tags = {hls}, + booktitle = {Proceedings of the 7th International Symposium on Quality + Electronic Design}, + year = 2006, + pages = {71--78}, + doi = {10.1109/ISQED.2006.10}, + acmid = 1126731, + address = {Washington, DC, USA}, + isbn = {0-7695-2523-7}, + numpages = 8, + publisher = {IEEE Computer Society}, + series = {ISQED '06}, +} + +@inproceedings{leroy06_formal_certif_compil_back_end, + author = {Leroy, Xavier}, + title = {Formal Certification of a Compiler Back-End or: Programming + a Compiler with a Proof Assistant}, + booktitle = {Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium + on Principles of Programming Languages}, + year = 2006, + pages = {42-54}, + doi = {10.1145/1111037.1111042}, + url = {https://doi.org/10.1145/1111037.1111042}, + address = {New York, NY, USA}, + isbn = 1595930272, + keywords = {the Coq theorem prover, certified compilation, compiler + transformations and optimizations, program proof, semantic + preservation}, + location = {Charleston, South Carolina, USA}, + numpages = 13, + publisher = {Association for Computing Machinery}, + series = {POPL '06} +} + +@book{bertot04_inter_theor_provin_progr_devel, + author = {Yves Bertot and Pierre Cast{\'{e}}ran}, + title = {Interactive Theorem Proving and Program Development}, + year = 2004, + publisher = {Springer Berlin Heidelberg}, + url = {https://doi.org/10.1007/978-3-662-07964-5}, + doi = {10.1007/978-3-662-07964-5}, +} + +@inproceedings{tristan08_formal_verif_trans_valid, + author = {Tristan, Jean-Baptiste and Leroy, Xavier}, + title = {Formal Verification of Translation Validators: A Case Study on + Instruction Scheduling Optimizations}, + booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on + Principles of Programming Languages}, + year = 2008, + pages = {17-27}, + doi = {10.1145/1328438.1328444}, + address = {New York, NY, USA}, + isbn = 9781595936899, + location = {San Francisco, California, USA}, + numpages = 11, + publisher = {Association for Computing Machinery}, + series = {POPL '08} +} |