diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-28 01:25:28 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-28 01:25:28 +0100 |
| commit | 6959b38a343d4575efc442ea02422dc64cf59d00 (patch) | |
| tree | f98f3a4d9851863b7998d3ca87d5951af8919e8a /doc/index.rst | |
| parent | cfa2956933619440ab9803b1468292b191765b38 (diff) | |
| download | vericert-6959b38a343d4575efc442ea02422dc64cf59d00.tar.gz vericert-6959b38a343d4575efc442ea02422dc64cf59d00.zip | |
Add to documentation
Diffstat (limited to 'doc/index.rst')
| -rw-r--r-- | doc/index.rst | 42 |
1 files changed, 39 insertions, 3 deletions
diff --git a/doc/index.rst b/doc/index.rst index ebb99df..06aa509 100644 --- a/doc/index.rst +++ b/doc/index.rst @@ -6,21 +6,57 @@ Vericert's Documentation ======================== +A formally verified high-level synthesis (HLS) tool written in Coq, building on top of `CompCert +<https://github.com/AbsInt/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. Currently, the following C features are supported and +have all been proven correct, providing a verified translation from C to Verilog: + +- all int operations, +- non-recursive function calls, +- local arrays and pointers, and +- control-flow structures such as if-statements, for-loops, etc... + .. toctree:: :maxdepth: 2 - :caption: Content: + :caption: Content vericert .. toctree:: :maxdepth: 1 - :caption: Sources: + :caption: Sources src/Compiler src/hls/RTLBlockInstr + src/hls/RTLBlockgen + src/hls/RTLBlockgenproof + +Publications +------------ + +:OOPSLA '21: Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal + Verification of High-Level Synthesis. In *Proc. ACM Program. Lang.* 5, OOPSLA, 2021. + +:LATTE '21: Yann Herklotz and John Wickerson. High-level synthesis tools should be proven + correct. In *Workshop on Languages, Tools, and Techniques for Accelerator + Design*, 2021. + +Mailing lists +------------- + +For discussions, you can join the following mailing list: `lists.sr.ht/~ymherklotz/vericert-discuss <https://lists.sr.ht/~ymherklotz/vericert-discuss>`_. + +For contributing patches to the `sourcehut <https://sr.ht/~ymherklotz/vericert/>`_ repository: +`lists.sr.ht/~ymherklotz/vericert-devel <https://lists.sr.ht/~ymherklotz/vericert-devel>`_. Indices -================== +======= * :ref:`genindex` * :ref:`search` |