diff options
| author | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-09-20 09:02:50 +0000 |
|---|---|---|
| committer | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-09-20 09:02:50 +0000 |
| commit | 83aaa860b691697d59b83fadac2c4dad51972387 (patch) | |
| tree | f6a647979875be79a2f7b044cc54d99317938840 | |
| parent | 80568aaef48fab6aff08d0cc724909e5afeee5dd (diff) | |
| download | vericert-docs-83aaa860b691697d59b83fadac2c4dad51972387.tar.gz vericert-docs-83aaa860b691697d59b83fadac2c4dad51972387.zip | |
deploy: d9f8dee1a294ee087f56c6e54b16ad3b0bf8d895
| -rw-r--r-- | docs/index.html | 2 | ||||
| -rw-r--r-- | index.html | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/docs/index.html b/docs/index.html index 6b5a5be..03748e7 100644 --- a/docs/index.html +++ b/docs/index.html @@ -6,5 +6,5 @@ <strong>Docs</strong> <label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents></nav></aside></header><article class=markdown><p>Vericert translates C code into a hardware description language called Verilog, which can then be synthesised into hardware, to be placed onto a field-programmable gate array (FPGA) or -application-specific integrated circuit (ASIC).</p><p><a id=org332cb94></a></p><figure><img src=/images/toolflow.svg alt="Figure 1: 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." width=600><figcaption><p>Figure 1: 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.</p></figcaption></figure><p>The design shown in Figure <a href=#org332cb94>1</a> shows how Vericert leverages an existing verified C compiler +application-specific integrated circuit (ASIC).</p><p><a id=orgeab21f5></a></p><figure><img src=/images/toolflow.svg alt="Figure 1: 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." width=600><figcaption><p>Figure 1: 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.</p></figcaption></figure><p>The design shown in Figure <a href=#orgeab21f5>1</a> shows how Vericert leverages an existing verified C compiler called <a href=https://compcert.org/compcert-C.html>CompCert</a> to perform this translation.</p></article><footer class=book-footer><div class="flex flex-wrap justify-between"></div></footer><div class=book-comments></div><label for=menu-control class="hidden book-menu-overlay"></label></div><aside class=book-toc><nav id=TableOfContents></nav></aside></main></body></html>
\ No newline at end of file @@ -1,13 +1,13 @@ <!doctype html><html lang=en><head><meta name=generator content="Hugo 0.80.0"><meta charset=utf-8><meta name=viewport content="width=device-width,initial-scale=1"><meta name=description content="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, so proofs remain to be finished. Currently, the following C features are supported, but are not all proven correct yet:"><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Vericert"><meta property="og:description" content><meta property="og:type" content="website"><meta property="og:url" content="https://vericert.ymhg.org/"><title>Vericert | Vericert</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.dbf27d0aee7c885a97dc865e7209c83dde91bef2046568d3366053c4027e2089.css integrity="sha256-2/J9Cu58iFqX3IZecgnIPd6RvvIEZWjTNmBTxAJ+IIk="><script defer src=/en.search.min.8744a59deef42a09f73b965fa29a56c40c4f8892dff5bfae0b331df4b63bb70d.js integrity="sha256-h0Slne70Kgn3O5ZfoppWxAxPiJLf9b+uCzMd9LY7tw0="></script><link rel=alternate type=application/rss+xml href=https://vericert.ymhg.org/index.xml title=Vericert></head><body><input type=checkbox class="hidden toggle" id=menu-control> +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:"><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Vericert"><meta property="og:description" content><meta property="og:type" content="website"><meta property="og:url" content="https://vericert.ymhg.org/"><title>Vericert | Vericert</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.dbf27d0aee7c885a97dc865e7209c83dde91bef2046568d3366053c4027e2089.css integrity="sha256-2/J9Cu58iFqX3IZecgnIPd6RvvIEZWjTNmBTxAJ+IIk="><script defer src=/en.search.min.8744a59deef42a09f73b965fa29a56c40c4f8892dff5bfae0b331df4b63bb70d.js integrity="sha256-h0Slne70Kgn3O5ZfoppWxAxPiJLf9b+uCzMd9LY7tw0="></script><link rel=alternate type=application/rss+xml href=https://vericert.ymhg.org/index.xml title=Vericert></head><body><input type=checkbox class="hidden toggle" id=menu-control> <input type=checkbox class="hidden toggle" id=toc-control><main class="container flex"><aside class=book-menu><nav><div class=book-brand><a href=/><div id=book-logo></div></a><p>A formally verified high-level synthesis tool written in Coq.</p></div><div class=book-search><input type=text id=book-search-input placeholder=Search aria-label=Search maxlength=64 data-hotkeys=s/><div class="book-search-spinner hidden"></div><ul id=book-search-results></ul></div><ul><li><a href=https://vericert.ymhg.org/blog/>Blog</a><ul></ul></li><li><a href=https://vericert.ymhg.org/docs/>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</a></li><li><a href=https://vericert.ymhg.org/docs/coq-style-guide/>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/unreleased/>Unreleased Features</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/>Using Vericert</a></li></ul></li><li><a href=https://vericert.ymhg.org/future/>Future Work</a></li></ul><ul><li><a href=https://github.com/ymherklotz/vericert target=_blank rel=noopener>Github</a></li></ul></nav><script>(function(){var menu=document.querySelector("aside.book-menu nav");addEventListener("beforeunload",function(event){localStorage.setItem("menu.scrollTop",menu.scrollTop);});menu.scrollTop=localStorage.getItem("menu.scrollTop");})();</script></aside><div class=book-page><header class=book-header><div class="flex align-center justify-between"><label for=menu-control><img src=/svg/menu.svg class=book-icon alt=Menu></label> <strong>Vericert</strong> <label for=toc-control><img src=/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#features>Features</a></li><li><a href=#content>Content</a></li><li><a href=#papers>Papers</a></li></ul></li></ul></nav></aside></header><article class=markdown><p>A formally verified high-level synthesis (HLS) tool written in Coq, building on top of <a href=https://github.com/AbsInt/CompCert>CompCert</a>. 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.</p><h2 id=features>Features -<a class=anchor href=#features>#</a></h2><p>The project is currently a work in progress, so proofs remain to be finished. Currently, the -following C features are supported, but are not all proven correct yet:</p><ul><li>all int operations,</li><li>non-recursive function calls,</li><li>local arrays and pointers, and</li><li>control-flow structures such as if-statements, for-loops, etc…</li></ul><h2 id=content>Content +<a class=anchor href=#features>#</a></h2><p>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:</p><ul><li>all int operations,</li><li>non-recursive function calls,</li><li>local arrays and pointers, and</li><li>control-flow structures such as if-statements, for-loops, etc…</li></ul><h2 id=content>Content <a class=anchor href=#content>#</a></h2><ul><li><a href=/docs/building/>Vericert Documentation</a></li></ul><h2 id=papers>Papers <a class=anchor href=#papers>#</a></h2><dl><dt>OOPSLA ‘21</dt><dd>Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal Verification of High-Level Synthesis. In <em>Proc. ACM Program. Lang.</em> 5, OOPSLA, 2021. [<a href=/papers/fvhls_oopsla21.pdf>pdf</a>]</dd><dt>LATTE ‘21</dt><dd>Yann Herklotz and John Wickerson. High-level synthesis tools should be proven |