diff options
Diffstat (limited to 'README.org')
| -rw-r--r-- | README.org | 27 |
1 files changed, 20 insertions, 7 deletions
@@ -1,8 +1,21 @@ -#+title: +#+title: Scheduled Vericert -#+html: <a href="https://vericert.ymhg.org"><img src="https://vericert.ymhg.org/vericert-main.svg" width="100%" height="144" /></a> +* Scheduled Vericert -#+html: <p align=center><a href="https://github.com/ymherklotz/vericert/actions"><img src="https://github.com/ymherklotz/vericert/workflows/CI/badge.svg" /></a> <a href="https://vericert.ymhg.org/"><img src="https://github.com/ymherklotz/vericert-docs/workflows/docs/badge.svg" /></a></p> +This artefact contains modifications to Vericert with a scheduled back end, +together with a forward simulation proof from C to the scheduling language and a +testing backend that is not verified, but goes to Verilog. + +The top-level forward simulation proof can be found in =src/Compiler.v= +(=transf_c_program_correct=). + +There are a couple of =Admitted= theorems in the code, however, these are only +in: =src/hls/DVeriloggenproof.v=, =src/hls/HTLPargen.v= and +=src/hls/ClockRegisters.v=. These translation passes are only used for +benchmarking purposes, and are not used for the =transf_c_program_correct= +theorem. + +* Original README A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [[https://github.com/AbsInt/CompCert][CompCert]]. This ensures the correctness of the C to Verilog translation according to our Verilog semantics and @@ -52,7 +65,7 @@ together with the repository. To clone CompCert together with this project, and correct revision, you can run: #+begin_src shell -git clone -b v1.2.2 --recursive https://github.com/ymherklotz/vericert +git clone -b v1.2.2 --recursive https://github.com/___/vericert #+end_src If the repository is already cloned, you can run the following command to make sure that CompCert is @@ -113,11 +126,11 @@ following: ** Citation -If you use Vericert in any way, please cite it using our [[https://yannherklotz.com/papers/fvhls_oopsla21.pdf][OOPSLA'21 paper]]: +If you use Vericert in any way, please cite it using our [[https://______.com/papers/fvhls_oopsla21.pdf][OOPSLA'21 paper]]: #+begin_src bibtex -@inproceedings{herklotz21_fvhls, - author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John}, +@inproceedings{___21_fvhls, + author = {___, ___ and ___, ___ D. and Ramanathan, ___ and Wickerson, John}, title = {Formal Verification of High-Level Synthesis}, year = {2021}, number = {OOPSLA}, |