diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-20 14:53:34 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-20 14:53:34 +0000 |
| commit | 8588ebb4621d85b7ccc738622339b3aa53486c31 (patch) | |
| tree | 89e78e3ec67f884f7062aebb81b68aa54cf5fc1c /docs/index.org | |
| parent | 34afd2f6ea0fc55cca1c674ab9b2f181be878291 (diff) | |
| download | vericert-8588ebb4621d85b7ccc738622339b3aa53486c31.tar.gz vericert-8588ebb4621d85b7ccc738622339b3aa53486c31.zip | |
Delete documents folder and move to separate repository
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]] |