deploy: 4817968ab6439ef3830059dfd6cae2149fca8a17

author: ymherklotz <ymherklotz@users.noreply.github.com> 2021-09-19 13:21:13 +0000
committer: ymherklotz <ymherklotz@users.noreply.github.com> 2021-09-19 13:21:13 +0000
commit: 192b41cb48c2b5a703959b176d3d1ecd6d0f6d16 (patch)
tree: c4a6ee6c8a45a1bb4616e53128514e567f2884f6 /docs
parent: a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d (diff)
download: vericert-docs-192b41cb48c2b5a703959b176d3d1ecd6d0f6d16.tar.gz
vericert-docs-192b41cb48c2b5a703959b176d3d1ecd6d0f6d16.zip
4 files changed, 6 insertions, 6 deletions
diff --git a/docs/building/index.html b/docs/building/index.html
index 43ca1ba..49dc52b 100644
--- a/docs/building/index.html
+++ b/docs/building/index.html
@@ -2,13 +2,13 @@
 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="https://vericert.ymhg.org/docs/building/"><title>Building Vericert |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control>
+ Coq: theorem prover that is used to also program the HLS tool."><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/docs/building/"><title>Building Vericert |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.54c55766af8da62210d3127df0d1e8aaf9fc6cac5de780c02ac61d54f95f6d9d.js integrity="sha256-VMVXZq+NpiIQ0xJ98NHoqvn8bKxd54DAKsYdVPlfbZ0="></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><div class=book-brand><a href=/><div id=book-logo></div><span></span></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/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/ class=active>Building Vericert</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>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><h1>Building Vericert</h1><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
+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/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><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
diff --git a/docs/index.html b/docs/index.html
index 6b9cf54..419df0b 100644
--- a/docs/index.html
+++ b/docs/index.html
@@ -1,10 +1,10 @@
 <!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="https://vericert.ymhg.org/docs/"><title>Docs |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script><link rel=alternate type=application/rss+xml href=https://vericert.ymhg.org/docs/index.xml></head><body><input type=checkbox class="hidden toggle" id=menu-control>
+  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://vericert.ymhg.org/docs/"><title>Docs |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.54c55766af8da62210d3127df0d1e8aaf9fc6cac5de780c02ac61d54f95f6d9d.js integrity="sha256-VMVXZq+NpiIQ0xJ98NHoqvn8bKxd54DAKsYdVPlfbZ0="></script><link rel=alternate type=application/rss+xml href=https://vericert.ymhg.org/docs/index.xml></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><span></span></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/coq-style-guide/>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/ class=active>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</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>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><h1>Docs</h1><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=orgd5c959a></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=#orgd5c959a>1</a> shows how Vericert leverages an existing verified C compiler
+application-specific integrated circuit (ASIC).</p><p><a id=orgec42da1></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=#orgec42da1>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/unreleased/index.html b/docs/unreleased/index.html
index 489c576..c3ec67a 100644
--- a/docs/unreleased/index.html
+++ b/docs/unreleased/index.html
@@ -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="The following are unreleased features in Vericert that are currently being worked on and have not been completely proven correct yet. Currently this includes features such as:
  scheduling, if-conversion, loop pipelining, and functions.  This page gives some preliminary information on how the features are implemented and how the proofs for the features are being done. Once these features are properly implemented, they will be added to the proper documentation."><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Unreleased Features"><meta property="og:description" content="The following are unreleased features in Vericert that are currently being worked on and have not been completely proven correct yet. Currently this includes features such as:
- scheduling, if-conversion, loop pipelining, and functions.  This page gives some preliminary information on how the features are implemented and how the proofs for the features are being done. Once these features are properly implemented, they will be added to the proper documentation."><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/docs/unreleased/"><title>Unreleased Features |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control>
+ scheduling, if-conversion, loop pipelining, and functions.  This page gives some preliminary information on how the features are implemented and how the proofs for the features are being done. Once these features are properly implemented, they will be added to the proper documentation."><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/docs/unreleased/"><title>Unreleased Features |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.54c55766af8da62210d3127df0d1e8aaf9fc6cac5de780c02ac61d54f95f6d9d.js integrity="sha256-VMVXZq+NpiIQ0xJ98NHoqvn8bKxd54DAKsYdVPlfbZ0="></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><div class=book-brand><a href=/><div id=book-logo></div><span></span></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/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/unreleased/ class=active>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>Unreleased Features</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=#scheduling>Scheduling</a></li><li><a href=#scheduling>Operation Chaining</a></li><li><a href=#if-conversion>If-conversion</a></li><li><a href=#loop-pipelining>Loop pipelining</a></li><li><a href=#functions>Functions</a></li></ul></li></ul></nav></aside></header><h1>Unreleased Features</h1><article class=markdown><p>The following are unreleased features in Vericert that are currently being worked on and have not
diff --git a/docs/using-vericert/index.html b/docs/using-vericert/index.html
index 9ededc8..c8b352d 100644
--- a/docs/using-vericert/index.html
+++ b/docs/using-vericert/index.html
@@ -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="Vericert can be used to translate a subset of C into Verilog. As a simple example, consider the following C file (main.c):
 void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) { int sum = 0; for (int c = 0; c < 2; c++) { for (int d = 0; d < 2; d++) { for (int k = 0; k < 2; k++) { sum = sum + first[c][k]*second[k][d]; } multiply[c][d] = sum; sum = 0; } } } int main() { int f[2][2] = {{1, 2}, {3, 4}}; int s[2][2] = {{5, 6}, {7, 8}}; int m[2][2] = {{0, 0}, {0, 0}}; matrix_multiply(f, s, m); return m[1][1]; } It can be compiled using the following command, assuming that vericert is somewhere on the path."><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. As a simple example, consider the following C file (main.c):
-void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) { int sum = 0; for (int c = 0; c < 2; c++) { for (int d = 0; d < 2; d++) { for (int k = 0; k < 2; k++) { sum = sum + first[c][k]*second[k][d]; } multiply[c][d] = sum; sum = 0; } } } int main() { int f[2][2] = {{1, 2}, {3, 4}}; int s[2][2] = {{5, 6}, {7, 8}}; int m[2][2] = {{0, 0}, {0, 0}}; matrix_multiply(f, s, m); return m[1][1]; } It can be compiled using the following command, assuming that vericert is somewhere on the path."><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/docs/using-vericert/"><title>Using Vericert |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control>
+void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) { int sum = 0; for (int c = 0; c < 2; c++) { for (int d = 0; d < 2; d++) { for (int k = 0; k < 2; k++) { sum = sum + first[c][k]*second[k][d]; } multiply[c][d] = sum; sum = 0; } } } int main() { int f[2][2] = {{1, 2}, {3, 4}}; int s[2][2] = {{5, 6}, {7, 8}}; int m[2][2] = {{0, 0}, {0, 0}}; matrix_multiply(f, s, m); return m[1][1]; } It can be compiled using the following command, assuming that vericert is somewhere on the path."><meta property="og:type" content="article"><meta property="og:url" content="https://vericert.ymhg.org/docs/using-vericert/"><title>Using Vericert |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.54c55766af8da62210d3127df0d1e8aaf9fc6cac5de780c02ac61d54f95f6d9d.js integrity="sha256-VMVXZq+NpiIQ0xJ98NHoqvn8bKxd54DAKsYdVPlfbZ0="></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><div class=book-brand><a href=/><div id=book-logo></div><span></span></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/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/unreleased/>Unreleased Features</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/ class=active>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>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><h1>Using Vericert</h1><article class=markdown><p>Vericert can be used to translate a subset of C into Verilog. As a simple example, consider the
author	ymherklotz <ymherklotz@users.noreply.github.com>	2021-09-19 13:21:13 +0000
committer	ymherklotz <ymherklotz@users.noreply.github.com>	2021-09-19 13:21:13 +0000
commit	192b41cb48c2b5a703959b176d3d1ecd6d0f6d16 (patch)
tree	c4a6ee6c8a45a1bb4616e53128514e567f2884f6 /docs
parent	a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d (diff)
download	vericert-docs-192b41cb48c2b5a703959b176d3d1ecd6d0f6d16.tar.gz vericert-docs-192b41cb48c2b5a703959b176d3d1ecd6d0f6d16.zip