diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-02-25 13:39:17 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-02-25 13:39:17 +0000 |
| commit | c1c5fc8e12342a9fe435c8066c8e9316036ff991 (patch) | |
| tree | bddfebf8f9d4c68ad99ea94f78c04504b479ebf9 /docs/documentation.org | |
| parent | e043d3bd21e9a0ebd37b8ac2ca262ed630a5b192 (diff) | |
| download | vericert-c1c5fc8e12342a9fe435c8066c8e9316036ff991.tar.gz vericert-c1c5fc8e12342a9fe435c8066c8e9316036ff991.zip | |
Add more documentation and add coqdoc stylesheet
Diffstat (limited to 'docs/documentation.org')
| -rw-r--r-- | docs/documentation.org | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/docs/documentation.org b/docs/documentation.org index d4ef799..3a0633f 100644 --- a/docs/documentation.org +++ b/docs/documentation.org @@ -18,7 +18,7 @@ application-specific integrated circuit (ASIC). #+attr_html: :width 600 #+caption: 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. #+name: fig:design -[[/images/toolflow.svg]] +[[./images/toolflow.svg]] The design shown in Figure [[fig:design]] shows how Vericert leverages an existing verified C compiler called [[https://compcert.org/compcert-C.html][CompCert]] to perform this translation. @@ -554,4 +554,4 @@ A small standalone Coq file that exhibits many of the style points. :appendix: t :END: -#+include: fdl.org +#+include: res/fdl.org |