diff options
| -rw-r--r-- | CHANGELOG.org | 42 | ||||
| -rw-r--r-- | README.md | 84 | ||||
| -rw-r--r-- | README.org | 127 |
3 files changed, 169 insertions, 84 deletions
diff --git a/CHANGELOG.org b/CHANGELOG.org new file mode 100644 index 0000000..621683c --- /dev/null +++ b/CHANGELOG.org @@ -0,0 +1,42 @@ +# -*- fill-column: 80 -*- + +* Vericert Changelog + +** Unreleased + +*** New Features + +- Add *RTLBlock*, a basic block intermediate language that is based on CompCert's + RTL. +- Add *RTLPar*, which can execute groups of instructions in parallel. +- Add scheduling pass to go from RTLBlock to RTLPar. + +** v1.1.0 - 2020-12-17 + +Add a stable release with all proofs completed. + +** v1.0.1 - 2020-08-14 + +Release a new minor version fixing all proofs and fixing scripts to generate the +badges. + +*** Bug Fixes + +- Fix some of the proofs which were not passing. + +** v1.0.0 - 2020-08-13 + +First release of a fully verified version of Vericert with support for the +translation of many C constructs to Verilog. + +*** New Features + +- Most int instructions and operators. +- Non-recursive function calls. +- Local arrays, structs and unions of type int. +- Pointer arithmetic with int. + +** v0.1.0 - 2020-04-03 + +This is the first release with working HLS but without any proofs associated +with it. diff --git a/README.md b/README.md deleted file mode 100644 index d90b590..0000000 --- a/README.md +++ /dev/null @@ -1,84 +0,0 @@ -# Vericert - -[](https://github.com/ymherklotz/vericert/actions) -[](https://vericert.ymhg.org/) - - -A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [CompCert](https://github.com/AbsInt/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 - -The project is currently a work in progress, so proofs remain to be finished. Currently, the following C features are supported, but are not all proven correct yet: - -- all int operations, -- non-recursive function calls, -- local arrays and pointers -- control-flow structures such as if-statements, for-loops, etc... - -## Building - -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 [nix](https://nixos.org/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: - -- [Coq](https://coq.inria.fr/): theorem prover that is used to also program the HLS tool. -- [OCaml](https://ocaml.org/): the OCaml compiler to compile the extracted files. -- [bbv](https://github.com/mit-plv/bbv): an efficient bit vector library. -- [dune](https://github.com/ocaml/dune): build tool for ocaml projects to gather all the ocaml files and compile them in the right order. -- [menhir](http://gallium.inria.fr/~fpottier/menhir/): parser generator for ocaml. -- [findlib](https://github.com/ocaml/ocamlfind) to find installed OCaml libraries. -- [GCC](https://gcc.gnu.org/): compiler to help build CompCert. - -These dependencies can be installed manually, or automatically through Nix. - -### Downloading CompCert - -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, you can run: - -``` shell -git clone --recursive https://github.com/ymherklotz/vericert -``` - -If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded: - -``` shell -git submodule update --init -``` - -### Setting up Nix - -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: - -``` shell -nix-shell -``` - -which will open a shell that has all the dependencies loaded. - -### Makefile build - -If the dependencies were installed manually, or if one is in the `nix-shell`, the project can be built by running: - -``` shell -make -j8 -``` - -and installed locally, or under the `PREFIX` location using: - -``` shell -make install -``` - -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 - -To test out `vericert` you can try the following examples which are in the test folder using the following: - -``` 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 -``` diff --git a/README.org b/README.org new file mode 100644 index 0000000..608210f --- /dev/null +++ b/README.org @@ -0,0 +1,127 @@ +* Vericert + :PROPERTIES: +:CUSTOM_ID: vericert +:END: +#+html: <a href="https://github.com/ymherklotz/vericert/actions"><img src="https://github.com/ymherklotz/vericert/workflows/CI/badge.svg" /></a> +#+html: <a href="https://vericert.ymhg.org/"><img src="https://github.com/ymherklotz/vericert-docs/workflows/docs/badge.svg" /></a> + +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: +The project is currently a work in progress, so proofs remain to be +finished. Currently, the following C features are supported, but are not +all proven correct yet: + +- all int operations, +- non-recursive function calls, +- local arrays and pointers +- control-flow structures such as if-statements, for-loops, etc... + +** 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: + +- [[https://coq.inria.fr/][Coq]]: theorem prover that is used to also + program the HLS tool. +- [[https://ocaml.org/][OCaml]]: the OCaml compiler to compile the + extracted files. +- [[https://github.com/mit-plv/bbv][bbv]]: an efficient bit vector + library. +- [[https://github.com/ocaml/dune][dune]]: build tool for ocaml projects + to gather all the ocaml files and compile them in the right order. +- [[http://gallium.inria.fr/~fpottier/menhir/][menhir]]: parser + generator for ocaml. +- [[https://github.com/ocaml/ocamlfind][findlib]] to find installed + OCaml libraries. +- [[https://gcc.gnu.org/][GCC]]: compiler to help build CompCert. + +These dependencies can be installed manually, or automatically through +Nix. + +*** Downloading 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, you can run: + +#+begin_src shell + git clone --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: + +#+begin_src shell + 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 |