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 | |
| parent | 678816865a90216b750b9cf43f570ff3b868350f (diff) | |
| download | vericert-docs-3be488277ce46005570f08888fbf3125b9187c88.tar.gz vericert-docs-3be488277ce46005570f08888fbf3125b9187c88.zip | |
deploy: 5388aa50c0f6d329bbb10109369e9bf809c55a3e
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/building/index.html | 6 | ||||
| -rw-r--r-- | docs/index.html | 6 | ||||
| -rw-r--r-- | docs/index.xml | 4 | ||||
| -rw-r--r-- | docs/using-vericert/index.html | 6 |
4 files changed, 11 insertions, 11 deletions
diff --git a/docs/building/index.html b/docs/building/index.html index aa247ff..ddff1f7 100644 --- a/docs/building/index.html +++ b/docs/building/index.html @@ -2,10 +2,10 @@ The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following: Coq: theorem prover that is used to also program the HLS tool."><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Building Vericert"><meta property="og:description" content="To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with nix using the provided default.nix and shell.nix files. The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following: - Coq: theorem prover that is used to also program the HLS tool."><meta property="og:type" content="article"><meta property="og:url" content="http://example.org/docs/building/"><title>Building 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></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/ class=active>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> + Coq: theorem prover that is used to also program the HLS tool."><meta property="og:type" content="article"><meta property="og:url" content="https://ymherklotz.github.io/vericert-docs/docs/building/"><title>Building 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></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/ class=active>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>Building 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=#downloading-compcert>Downloading CompCert</a></li><li><a href=#setting-up-nix>Setting up Nix</a></li><li><a href=#makefile-build>Makefile build</a></li><li><a href=#testing>Testing</a></li></ul></li></ul></nav></aside></header><article class=markdown><p>To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with <a href=https://nixos.org/nix/>nix</a> using the provided <code>default.nix</code> and <code>shell.nix</code> files.</p><p>The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following:</p><ul><li><a href=https://coq.inria.fr/>Coq</a>: theorem prover that is used to also program the HLS tool.</li><li><a href=https://ocaml.org/>OCaml</a>: the OCaml compiler to compile the extracted files.</li><li><a href=https://github.com/mit-plv/bbv>bbv</a>: an efficient bit vector library.</li><li><a href=https://github.com/ocaml/dune>dune</a>: build tool for ocaml projects to gather all the ocaml files and compile them in the right order.</li><li><a href=http://gallium.inria.fr/~fpottier/menhir/>menhir</a>: parser generator for ocaml.</li><li><a href=https://github.com/ocaml/ocamlfind>findlib</a> to find installed OCaml libraries.</li><li><a href=https://gcc.gnu.org/>GCC</a>: compiler to help build CompCert.</li></ul><p>These dependencies can be installed manually, or automatically through Nix.</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=kn>Definition</span> <span class=n>help</span> <span class=o>:=</span> <span class=n>0</span><span class=o>.</span> +<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=#downloading-compcert>Downloading CompCert</a></li><li><a href=#setting-up-nix>Setting up Nix</a></li><li><a href=#makefile-build>Makefile build</a></li><li><a href=#testing>Testing</a></li></ul></li></ul></nav></aside></header><article class=markdown><p>To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with <a href=https://nixos.org/nix/>nix</a> using the provided <code>default.nix</code> and <code>shell.nix</code> files.</p><p>The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following:</p><ul><li><a href=https://coq.inria.fr/>Coq</a>: theorem prover that is used to also program the HLS tool.</li><li><a href=https://ocaml.org/>OCaml</a>: the OCaml compiler to compile the extracted files.</li><li><a href=https://github.com/mit-plv/bbv>bbv</a>: an efficient bit vector library.</li><li><a href=https://github.com/ocaml/dune>dune</a>: build tool for ocaml projects to gather all the ocaml files and compile them in the right order.</li><li><a href=http://gallium.inria.fr/~fpottier/menhir/>menhir</a>: parser generator for ocaml.</li><li><a href=https://github.com/ocaml/ocamlfind>findlib</a> to find installed OCaml libraries.</li><li><a href=https://gcc.gnu.org/>GCC</a>: compiler to help build CompCert.</li></ul><p>These dependencies can be installed manually, or automatically through Nix.</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=kn>Definition</span> <span class=n>help</span> <span class=o>:=</span> <span class=n>0</span><span class=o>.</span> </code></pre></div><h2 id=downloading-compcert>Downloading CompCert <a class=anchor href=#downloading-compcert>#</a></h2><p>CompCert is added as a submodule in the <code>lib/CompCert</code> directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>git clone --recursive https://github.com/ymherklotz/vericert </code></pre></div><p>If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>git submodule update --init 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 diff --git a/docs/index.xml b/docs/index.xml index 03139d4..199ed30 100644 --- a/docs/index.xml +++ b/docs/index.xml @@ -1,3 +1,3 @@ -<?xml version="1.0" encoding="utf-8" standalone="yes"?><rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Docs on Vericert</title><link>http://example.org/docs/</link><description>Recent content in Docs on Vericert</description><generator>Hugo -- gohugo.io</generator><language>en-us</language><copyright>© 2020-2021 Yann Herklotz</copyright><atom:link href="http://example.org/docs/index.xml" rel="self" type="application/rss+xml"/><item><title>Building Vericert</title><link>http://example.org/docs/building/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>http://example.org/docs/building/</guid><description>To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with nix using the provided default.nix and shell.nix files. +<?xml version="1.0" encoding="utf-8" standalone="yes"?><rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Docs on Vericert</title><link>https://ymherklotz.github.io/vericert-docs/docs/</link><description>Recent content in Docs on Vericert</description><generator>Hugo -- gohugo.io</generator><language>en-us</language><copyright>© 2020-2021 Yann Herklotz</copyright><atom:link href="https://ymherklotz.github.io/vericert-docs/docs/index.xml" rel="self" type="application/rss+xml"/><item><title>Building Vericert</title><link>https://ymherklotz.github.io/vericert-docs/docs/building/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>https://ymherklotz.github.io/vericert-docs/docs/building/</guid><description>To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with nix using the provided default.nix and shell.nix files. The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following: -Coq: theorem prover that is used to also program the HLS tool.</description></item><item><title>Using Vericert</title><link>http://example.org/docs/using-vericert/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>http://example.org/docs/using-vericert/</guid><description>Vericert can be used to translate a subset of C into Verilog.</description></item></channel></rss>
\ No newline at end of file +Coq: theorem prover that is used to also program the HLS tool.</description></item><item><title>Using Vericert</title><link>https://ymherklotz.github.io/vericert-docs/docs/using-vericert/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>https://ymherklotz.github.io/vericert-docs/docs/using-vericert/</guid><description>Vericert can be used to translate a subset of C into Verilog.</description></item></channel></rss>
\ No newline at end of file diff --git a/docs/using-vericert/index.html b/docs/using-vericert/index.html index 6d9d6f7..750e168 100644 --- a/docs/using-vericert/index.html +++ b/docs/using-vericert/index.html @@ -1,4 +1,4 @@ -<!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 can be used to translate a subset of C into Verilog."><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Using Vericert"><meta property="og:description" content="Vericert can be used to translate a subset of C into Verilog."><meta property="og:type" content="article"><meta property="og:url" content="http://example.org/docs/using-vericert/"><title>Using 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></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/ class=active>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> +<!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 can be used to translate a subset of C into Verilog."><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Using Vericert"><meta property="og:description" content="Vericert can be used to translate a subset of C into Verilog."><meta property="og:type" content="article"><meta property="og:url" content="https://ymherklotz.github.io/vericert-docs/docs/using-vericert/"><title>Using 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></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/ class=active>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>Using 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></nav></aside></header><article class=markdown><p>Vericert can be used to translate a subset of C into Verilog.</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 can be used to translate a subset of C into Verilog.</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 |