blob: 7a926508167a57ede1ab76694ab971487c274989 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
#+SETUPFILE: publish.setup
#+TITLE: Vericert
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
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...
* Content
- [[./proof/toc.html][Vericert Proof]]
- [[./documentation.org][Vericert Documentation]]
|
