diff options
Diffstat (limited to 'docs/index.org')
| -rw-r--r-- | docs/index.org | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/docs/index.org b/docs/index.org deleted file mode 100644 index f82d5a8..0000000 --- a/docs/index.org +++ /dev/null @@ -1,18 +0,0 @@ -#+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/index.org][Vericert Proof]] -- [[./docs/index.org][Vericert Documentation]] |