diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-25 20:08:42 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-25 20:08:42 +0000 |
| commit | 2ae0478bcb186de821ea37995f784954b4b35f29 (patch) | |
| tree | 6ffef7e4d2d5b89eeb7276f43918fab8cbad3da3 /docs/index.org | |
| parent | 40bd9b96f33cdbea6318a7bbb9cd2ca605c60d56 (diff) | |
| download | vericert-2ae0478bcb186de821ea37995f784954b4b35f29.tar.gz vericert-2ae0478bcb186de821ea37995f784954b4b35f29.zip | |
Add more documentation
Diffstat (limited to 'docs/index.org')
| -rw-r--r-- | docs/index.org | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/docs/index.org b/docs/index.org index 7a92650..455a23a 100644 --- a/docs/index.org +++ b/docs/index.org @@ -1,5 +1,5 @@ -#+SETUPFILE: publish.setup -#+TITLE: Vericert +#+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. |