diff options
| author | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-01-22 13:00:13 +0000 |
|---|---|---|
| committer | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-01-22 13:00:13 +0000 |
| commit | af25d179c9bfa2aa4585f14210aa11906965f045 (patch) | |
| tree | ca8e45cf74f2b876c4e21947e6ccccb5a812aa37 /index.html | |
| parent | bdaa8844be64818cab4bd8e77e91bb7af0bfcf98 (diff) | |
| download | vericert-docs-af25d179c9bfa2aa4585f14210aa11906965f045.tar.gz vericert-docs-af25d179c9bfa2aa4585f14210aa11906965f045.zip | |
deploy: e38739e42b8b7da37027b86cf58cc114d5224d69
Diffstat (limited to 'index.html')
| -rw-r--r-- | index.html | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -1,6 +1,6 @@ <!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/"><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.a4d6f3160019c50a1674877d2ccd95fce25e9106249985d3c32868cd7e574c28.css integrity="sha256-pNbzFgAZxQoWdId9LM2V/OJekQYkmYXTwyhozX5XTCg="><script defer src=/en.search.min.90cea40d1c9e495620e94dded717dbc4c64fd0e3c89f00dc75212bbfccf36188.js integrity="sha256-kM6kDRyeSVYg6U3e1xfbxMZP0OPInwDcdSErv8zzYYg="></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><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=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/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://vericert.ymhg.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.a4d6f3160019c50a1674877d2ccd95fce25e9106249985d3c32868cd7e574c28.css integrity="sha256-pNbzFgAZxQoWdId9LM2V/OJekQYkmYXTwyhozX5XTCg="><script defer src=/en.search.min.0954d4b2fc6bff27e6f999bbc5c4fd9011adb3be3811a6642db8ce343b98ef63.js integrity="sha256-CVTUsvxr/yfm+Zm7xcT9kBGts744EaZkLbjONDuY72M="></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><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=https://vericert.ymhg.org/coq-style-guide/>Coq Style Guide</a></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/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> <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 <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 |