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/Makefile | 4 ++-- doc/_static/css/custom.css | 22 +++++++++++++++++++++- doc/conf.py | 21 ++++----------------- doc/index.rst | 42 +++++++++++++++++++++++++++++++++++++++--- doc/vericert.rst | 8 ++------ 5 files changed, 68 insertions(+), 29 deletions(-) (limited to 'doc') diff --git a/doc/Makefile b/doc/Makefile index 5662645..8a34845 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -9,7 +9,7 @@ SOURCEDIR = . BUILDDIR = _build SOURCE_DATE_EPOCH = $(shell git log -1 --format=%ct) -VS_DOCS := ../src/Compiler.v ../src/hls/RTLBlockInstr.v +VS_DOCS := Compiler.v hls/RTLBlockInstr.v hls/RTLBlockgen.v hls/RTLBlockgenproof.v # Put it first so that "make" without argument is like "make help". help: @@ -20,5 +20,5 @@ help: # Catch-all target: route all unknown targets to Sphinx using the new # "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS). %: Makefile - $(foreach d,$(VS_DOCS),cp $(d) $(patsubst ../%,%,$(d));) + $(foreach d,$(VS_DOCS),cp ../src/$(d) src/$(d);) @$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) diff --git a/doc/_static/css/custom.css b/doc/_static/css/custom.css index 66a1e35..e899c8f 100644 --- a/doc/_static/css/custom.css +++ b/doc/_static/css/custom.css @@ -3,9 +3,29 @@ .alectryon-coqdoc .doc .inlinecode, .alectryon-mref, .alectryon-block, .alectryon-io, -.alectryon-toggle-label, .alectryon-banner, pre, tt, code { +.alectryon-toggle-label, .alectryon-banner, pre, tt, code, +.rst-content kbd, .rst-content pre, .rst-content samp, +.rst-content .linenodiv pre, .rst-content div[class^="highlight"] pre, .rst-content pre.literal-block { font-family: 'Iosevka Fixed Slab', 'Iosevka Slab Web', 'Iosevka Web', 'Iosevka Slab', 'Iosevka', 'Fira Code', monospace; font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */; line-height: initial; + font-size: 0.9em; +} + +img { width: 100%; } +a { color: #469369; } +a:hover { color: #60b386; } + +.wy-menu-vertical header, .wy-menu-vertical p.caption { + color: #fff5db; +} + +.wy-nav-content, .wy-menu-vertical li.current > a, .wy-menu-vertical li.on a { + background-color: #fffbf2; + color: #2a3e40; +} + +.wy-side-nav-search .wy-dropdown > a, .wy-side-nav-search > a { + color: #2a3e40; } diff --git a/doc/conf.py b/doc/conf.py index c7a9970..7000f7b 100644 --- a/doc/conf.py +++ b/doc/conf.py @@ -48,25 +48,12 @@ pygments_style = "emacs" # The theme to use for HTML and HTML Help pages. See the documentation for # a list of builtin themes. # -html_theme = 'alabaster' +html_theme = 'sphinx_rtd_theme' -html_theme_options = { - 'logo': 'images/vericert-main.svg', - 'github_user': 'ymherklotz', - 'github_repo': 'vericert', - 'description': 'A formally verified high-level synthesis tool written in Coq.', - 'github_button': False, - 'show_powered_by': False, -} +html_logo = "_static/images/vericert-main.svg" -html_sidebars = { - '**': [ - 'about.html', - 'searchbox.html', - 'navigation.html', - 'relations.html', - 'donate.html', - ] +html_theme_options = { + 'style_nav_header_background': '#fff5db' } # Add any paths that contain custom static files (such as style sheets) here, 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 +`_ 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 `_. + +For contributing patches to the `sourcehut `_ repository: +`lists.sr.ht/~ymherklotz/vericert-devel `_. Indices -================== +======= * :ref:`genindex` * :ref:`search` 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