From 6959b38a343d4575efc442ea02422dc64cf59d00 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 28 Mar 2022 01:25:28 +0100 Subject: Add to documentation --- doc/vericert.rst | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'doc/vericert.rst') 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 `_ 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. -- cgit