diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-25 15:47:30 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-25 16:59:51 +0000 |
| commit | e8027cbeac9e4fc0efe5a0b661bcc2e2a89dab35 (patch) | |
| tree | b656612ce422b55339ab2a1ee3d1dbde9d63fe9e /docs/index.org | |
| parent | 2f5aedb202bdfb860152f25932c6df40100801bc (diff) | |
| download | vericert-kvx-e8027cbeac9e4fc0efe5a0b661bcc2e2a89dab35.tar.gz vericert-kvx-e8027cbeac9e4fc0efe5a0b661bcc2e2a89dab35.zip | |
Fix documentation for docs website
Diffstat (limited to 'docs/index.org')
| -rw-r--r-- | docs/index.org | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/docs/index.org b/docs/index.org index 6ec0130..7a92650 100644 --- a/docs/index.org +++ b/docs/index.org @@ -1,5 +1,5 @@ -#+SETUPFILE: setup.org -#+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. @@ -14,5 +14,5 @@ The project is currently a work in progress, so proofs remain to be finished. C * Content -- [[./docs/toc.html][Vericert Coq Documentation]] -- [[./building.org][Building Vericert]] +- [[./proof/toc.html][Vericert Proof]] +- [[./documentation.org][Vericert Documentation]] |