diff options
| author | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-01-16 22:17:24 +0000 |
|---|---|---|
| committer | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-01-16 22:17:24 +0000 |
| commit | 3be488277ce46005570f08888fbf3125b9187c88 (patch) | |
| tree | fcbfb09001aaf7efa539f567a443a5e3f2a19c80 /docs/index.html | |
| parent | 678816865a90216b750b9cf43f570ff3b868350f (diff) | |
| download | vericert-docs-3be488277ce46005570f08888fbf3125b9187c88.tar.gz vericert-docs-3be488277ce46005570f08888fbf3125b9187c88.zip | |
deploy: 5388aa50c0f6d329bbb10109369e9bf809c55a3e
Diffstat (limited to 'docs/index.html')
| -rw-r--r-- | docs/index.html | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/docs/index.html b/docs/index.html index c264cdc..12c9fe0 100644 --- a/docs/index.html +++ b/docs/index.html @@ -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="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). 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. - The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation."><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Docs"><meta property="og:description" content><meta property="og:type" content="website"><meta property="og:url" content="http://example.org/docs/"><title>Docs | 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/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=/><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/ class=active>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> + The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation."><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Docs"><meta property="og:description" content><meta property="og:type" content="website"><meta property="og:url" content="https://ymherklotz.github.io/vericert-docs/docs/"><title>Docs | 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/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/ class=active>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>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=org56d9d9f></a></p><figure><img src=/images/design.jpg 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=#org56d9d9f>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 +<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></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=org1fcc175></a></p><figure><img src=/images/design.jpg 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=#org1fcc175>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 |