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/vericert.rst | |
parent | cfa2956933619440ab9803b1468292b191765b38 (diff) | |
download | vericert-6959b38a343d4575efc442ea02422dc64cf59d00.tar.gz vericert-6959b38a343d4575efc442ea02422dc64cf59d00.zip |
Add to documentation
Diffstat (limited to 'doc/vericert.rst')
-rw-r--r-- | doc/vericert.rst | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/doc/vericert.rst b/doc/vericert.rst index 3c8eaeb..19ac28f 100644 --- a/doc/vericert.rst +++ b/doc/vericert.rst @@ -12,7 +12,7 @@ application-specific integrated circuit (ASIC). .. _fig:design: -.. figure:: /_static/images/toolflow.png +.. figure:: /_static/images/toolflow.svg Current design of Vericert, where HTL is an intermediate language representing a finite state machine with data-path (FSMD) and Verilog is the target language. @@ -20,8 +20,6 @@ application-specific integrated circuit (ASIC). The design shown in Figure `fig:design`_ shows how Vericert leverages an existing verified C compiler called `CompCert <https://compcert.org/compcert-C.html>`_ to perform this translation. -.. index:: vericert - .. _building: Building Vericert @@ -48,8 +46,6 @@ Or by running the test suite using the following command: .. _using-vericert: -.. index:: vericert - Using Vericert -------------- @@ -454,7 +450,7 @@ Example A small standalone Coq file that exhibits many of the style points. -.. code:: coq +.. coq:: no-out (* * Vericert: Verified high-level synthesis. |