ymherklotz / vericert

A formally verified high-level synthesis tool based on CompCert and written in Coq.
https://vericert.ymhg.org
GNU General Public License v3.0
88 stars 5 forks source link
coq high-level-synthesis

+title:

+html:

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 CompCert's C semantics, removing the need to check the resulting hardware for behavioural correctness.

** Features :PROPERTIES: :CUSTOM_ID: features :END:

Currently all proofs of the following features have been completed.

** Building :PROPERTIES: :CUSTOM_ID: building :END: To build Vericert, the provided [[/Makefile][Makefile]] can be used. External dependencies are needed to build the project, which can be pulled in automatically with [[https://nixos.org/nix/][nix]] using the provided [[/default.nix][default.nix]] and [[/shell.nix][shell.nix]] files.

The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following:

These dependencies can be installed manually, or automatically through Nix.

*** Downloading Vericert and CompCert :PROPERTIES: :CUSTOM_ID: downloading-compcert :END: CompCert is added as a submodule in the =lib/CompCert= directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, and check it out at the correct revision, you can run:

+begin_src shell

git clone -b v1.2.2 --recursive https://github.com/ymherklotz/vericert

+end_src

If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded and the correct branch is checked out:

+begin_src shell

git checkout v1.2.2 git submodule update --init

+end_src

*** Setting up Nix :PROPERTIES: :CUSTOM_ID: setting-up-nix :END: Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way.

To open a shell which includes all the necessary dependencies, one can use:

+begin_src shell

nix-shell

+end_src

which will open a shell that has all the dependencies loaded.

*** Makefile build :PROPERTIES: :CUSTOM_ID: makefile-build :END: If the dependencies were installed manually, or if one is in the =nix-shell=, the project can be built by running:

+begin_src shell

make -j8

+end_src

and installed locally, or under the =PREFIX= location using:

+begin_src shell

make install

+end_src

Which will install the binary in =./bin/vericert= by default. However, this can be changed by changing the =PREFIX= environment variable, in which case the binary will be installed in =$PREFIX/bin/vericert=.

** Running :PROPERTIES: :CUSTOM_ID: running :END: To test out =vericert= you can try the following examples which are in the test folder using the following:

+begin_src shell

./bin/vericert test/loop.c -o loop.v ./bin/vericert test/conditional.c -o conditional.v ./bin/vericert test/add.c -o add.v

+end_src

** Citation

If you use Vericert in any way, please cite it using our [[https://yannherklotz.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}, title = {Formal Verification of High-Level Synthesis}, year = {2021}, number = {OOPSLA}, numpages = {30}, month = {11}, journal = {Proc. ACM Program. Lang.}, volume = {5}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, doi = {10.1145/3485494} }

+end_src

** License

This project is licensed under [[https://www.gnu.org/licenses/gpl-3.0.en.html][GPLv3]]. The license can be seen in [[file:LICENSE][LICENSE]].

The following external code and its license is present in this repository:

+begin_src text

Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA

+end_src