blob: 907ac2558cd6b2ae9aad96ccad3a2d2a3fd00d90 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
#+SETUPFILE: setup.org
#+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...
* TOC
[[/docs/toc.html][- Vericert Coq Documentation]]
- [[./building.org][Building Vericert]]
|
