1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
#+html: <a href="https://vericert.ymhg.org"><img src="https://vericert.ymhg.org/vericert-main.svg" width="100%" height="144" /></a>
#+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>
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
|
