1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
.. Vericert documentation master file, created by
sphinx-quickstart on Sat Mar 26 18:15:40 2022.
You can adapt this file completely to your liking, but it should at least
contain the root `toctree` directive.
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
vericert
.. toctree::
:maxdepth: 1
:caption: Sources
src/Compiler
src/hls/Gible.v
src/hls/GibleSeq.v
src/hls/GiblePar.v
src/hls/GibleSeqgen.v
src/hls/GibleSeqgenproof.v
Publications
------------
:OOPSLA '21: ___ ___, ___ D. ___, ___ Ramanathan, and John Wickerson. Formal
Verification of High-Level Synthesis. In *Proc. ACM Program. Lang.* 5, OOPSLA, 2021.
:LATTE '21: ___ ___ 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/~___/vericert-discuss <https://lists.sr.ht/~___/vericert-discuss>`_.
For contributing patches to the `sourcehut <https://sr.ht/~___/vericert/>`_ repository:
`lists.sr.ht/~___/vericert-devel <https://lists.sr.ht/~___/vericert-devel>`_.
Indices
=======
* :ref:`genindex`
* :ref:`search`
|
