diff options
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. |