diff options
Diffstat (limited to 'index.html')
| -rw-r--r-- | index.html | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -1,7 +1,7 @@ <!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="http://example.org/"><meta property="og:updated_time" content="2021-01-16T00:00:00+00:00"><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.9a01d8047438cc0bac3d13e2a238c5a321f8116bf4a172e80d498712a58ce50d.css integrity="sha256-mgHYBHQ4zAusPRPiojjFoyH4EWv0oXLoDUmHEqWM5Q0="><script defer src=/en.search.min.90cea40d1c9e495620e94dded717dbc4c64fd0e3c89f00dc75212bbfccf36188.js integrity="sha256-kM6kDRyeSVYg6U3e1xfbxMZP0OPInwDcdSErv8zzYYg="></script><link rel=alternate type=application/rss+xml href=http://example.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><h2 class=book-brand><a href=/><span>Vericert</span></a></h2><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=http://example.org/docs/>Docs</a><ul><li><a href=http://example.org/docs/building/>Building Vericert</a></li><li><a href=http://example.org/docs/using-vericert/>Using Vericert</a></li></ul></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> +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://ymherklotz.github.io/vericert-docs/"><meta property="og:updated_time" content="2021-01-16T00:00:00+00:00"><title>Vericert | Vericert</title><link rel=manifest href=/vericert-docs/manifest.json><link rel=icon href=/vericert-docs/favicon.png type=image/x-icon><link rel=stylesheet href=/vericert-docs/book.min.9a01d8047438cc0bac3d13e2a238c5a321f8116bf4a172e80d498712a58ce50d.css integrity="sha256-mgHYBHQ4zAusPRPiojjFoyH4EWv0oXLoDUmHEqWM5Q0="><script defer src=/vericert-docs/en.search.min.77eecb367a48b50a7df2acdb69aba4b0107b4b1306bd8f7510bb929a260db0b1.js integrity="sha256-d+7LNnpItQp98qzbaauksBB7SxMGvY91ELuSmiYNsLE="></script><link rel=alternate type=application/rss+xml href=https://ymherklotz.github.io/vericert-docs/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><h2 class=book-brand><a href=/vericert-docs><span>Vericert</span></a></h2><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://ymherklotz.github.io/vericert-docs/docs/>Docs</a><ul><li><a href=https://ymherklotz.github.io/vericert-docs/docs/building/>Building Vericert</a></li><li><a href=https://ymherklotz.github.io/vericert-docs/docs/using-vericert/>Using Vericert</a></li></ul></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=/vericert-docs/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></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 +<label for=toc-control><img src=/vericert-docs/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></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</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></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><ul><li><ul><li><a href=#features>Features</a></li><li><a href=#content>Content</a></li></ul></li></ul></nav></aside></main></body></html>
\ No newline at end of file |