diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-01-05 00:08:19 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-01-05 00:08:19 +0000 |
| commit | 731061bca6c596c77206c1dd35bae74c7dd2a4cf (patch) | |
| tree | 87d196ee29e1ef5ee5a70ac49c41e227373687b1 | |
| parent | 5b1b2bbb64a6a41b969b0b496c4bc97ecf9eacf1 (diff) | |
| download | vericert-docs-731061bca6c596c77206c1dd35bae74c7dd2a4cf.tar.gz vericert-docs-731061bca6c596c77206c1dd35bae74c7dd2a4cf.zip | |
Fix links again and add category
| -rw-r--r-- | documentation.org | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/documentation.org b/documentation.org index f6ed812..be9213b 100644 --- a/documentation.org +++ b/documentation.org @@ -634,7 +634,7 @@ A small standalone Coq file that exhibits many of the style points. Blog posts: -** A First Look at Vericert :introduction:summary:article: +** A First Look at Vericert :introduction:summary:@article: :PROPERTIES: :EXPORT_DATE: 2021-10-09 :EXPORT_FILE_NAME: a-first-look-at-vericert @@ -684,7 +684,7 @@ hardware accelerators, speeding up the design process even more. #+caption: Typical HLS flow compared to the standard software flow. #+attr_html: :width 500px -[[/images/hls-flow-handdrawn.svg]] +[[./static/images/hls-flow-handdrawn.svg]] However, in practice this does not seem to be the case yet. For now, the state-of-the-art HLS compilers restrict the subset of the input language greatly, and often cannot optimise it optimally. @@ -701,14 +701,14 @@ that it should be possible to check the correctness of the hardware design purel making the design process so much more efficient. The fact that it might therefore introduce bugs in the process, means that the final HLS designs need to be re-verified afterwards. -We have written a [[/papers/hlsspc_latte2021.pdf][workshop paper]] published at LATTE'21 which describes why HLS in particular is an +We have written a [[./static/papers/hlsspc_latte2021.pdf][workshop paper]] published at LATTE'21 which describes why HLS in particular is an important translation to verify. *** How do we formally verify it? #+caption: Add a back end branching off the three-address code intermediate language to produce Verilog. #+attr_html: :width 500px -[[/images/toolflow-handdrawn.svg]] +[[./static/images/toolflow-handdrawn.svg]] We use CompCert, an existing formally verified C compiler, to translate C into 3AC[fn:1], which is the starting point of our high-level synthesis pass. We chose this intermediate language in |