deploy: 8d74fffc72abb3cc20df691d9d40c73fbd1c0c27

author: ymherklotz <ymherklotz@users.noreply.github.com> 2021-09-19 00:54:08 +0000
committer: ymherklotz <ymherklotz@users.noreply.github.com> 2021-09-19 00:54:08 +0000
commit: a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d (patch)
tree: 52ad54ef5468d7755357dd0a2d513af94c3ea9b5 /docs
parent: 20a623794340113684dfeb5a7ff2e78f6a4d35f3 (diff)
download: vericert-docs-a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d.tar.gz
vericert-docs-a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d.zip
4 files changed, 38 insertions, 18 deletions
diff --git a/docs/building/index.html b/docs/building/index.html
index c761f82..43ca1ba 100644
--- a/docs/building/index.html
+++ b/docs/building/index.html
@@ -5,16 +5,27 @@ The project is written in Coq, a theorem prover, which is extracted to OCaml so
  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>
 <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 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 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
+<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
+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
+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
 </code></pre></div><h2 id=setting-up-nix>Setting up Nix
-<a class=anchor href=#setting-up-nix>#</a></h2><p>Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way.</p><p>To open a shell which includes all the necessary dependencies, one can use:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>nix-shell
+<a class=anchor href=#setting-up-nix>#</a></h2><p>Nix is a package manager that can create an isolated environment so that the builds are
+reproducible. Once nix is installed, it can be used in the following way.</p><p>To open a shell which includes all the necessary dependencies, one can use:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>nix-shell
 </code></pre></div><p>which will open a shell that has all the dependencies loaded.</p><h2 id=makefile-build>Makefile build
-<a class=anchor href=#makefile-build>#</a></h2><p>If the dependencies were installed manually, or if one is in the <code>nix-shell</code>, the project can be built by running:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>make -j8
+<a class=anchor href=#makefile-build>#</a></h2><p>If the dependencies were installed manually, or if one is in the <code>nix-shell</code>, the project can be built
+by running:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>make -j8
 </code></pre></div><p>and installed locally, or under the <code>PREFIX</code> location using:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>make install
-</code></pre></div><p>Which will install the binary in <code>./bin/vericert</code> by default. However, this can be changed by changing the <code>PREFIX</code> environment variable, in which case the binary will be installed in <code>$PREFIX/bin/vericert</code>.</p><h2 id=testing>Testing
-<a class=anchor href=#testing>#</a></h2><p>To test out <code>vericert</code> you can try the following examples which are in the test folder using the following:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>./bin/vericert test/loop.c -o loop.v
+</code></pre></div><p>Which will install the binary in <code>./bin/vericert</code> by default. However, this can be changed by changing
+the <code>PREFIX</code> environment variable, in which case the binary will be installed in <code>$PREFIX/bin/vericert</code>.</p><h2 id=testing>Testing
+<a class=anchor href=#testing>#</a></h2><p>To test out <code>vericert</code> you can try the following examples which are in the test folder using the
+following:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>./bin/vericert test/loop.c -o loop.v
 ./bin/vericert test/conditional.c -o conditional.v
 ./bin/vericert test/add.c -o add.v
 </code></pre></div><p>Or by running the test suite using the following command:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>make <span class=nb>test</span>
diff --git a/docs/index.html b/docs/index.html
index 5c47f44..6b9cf54 100644
--- a/docs/index.html
+++ b/docs/index.html
@@ -4,4 +4,7 @@
   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>
 <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=org52e0c8a></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=#org52e0c8a>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=/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
+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 1cf635a..489c576 100644
--- a/docs/unreleased/index.html
+++ b/docs/unreleased/index.html
@@ -3,7 +3,10 @@
  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>
 <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 been completely proven correct yet. Currently this includes features such as:</p><ul><li><a href=#scheduling>scheduling</a>,</li><li><a href=#if-conversion>if-conversion</a>,</li><li><a href=#loop-pipelining>loop pipelining</a>, and</li><li><a href=#functions>functions</a>.</li></ul><p>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.</p><h2 id=scheduling>Scheduling
+<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
+been completely proven correct yet. Currently this includes features such as:</p><ul><li><a href=#scheduling>scheduling</a>,</li><li><a href=#if-conversion>if-conversion</a>,</li><li><a href=#loop-pipelining>loop pipelining</a>, and</li><li><a href=#functions>functions</a>.</li></ul><p>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.</p><h2 id=scheduling>Scheduling
 <a class=anchor href=#scheduling>#</a></h2><p>Scheduling is an optimisation which is used to run</p><h2 id=scheduling>Operation Chaining
 <a class=anchor href=#scheduling>#</a></h2><p>Scheduling is an optimisation which is used to run</p><h2 id=if-conversion>If-conversion
 <a class=anchor href=#if-conversion>#</a></h2><p>If-conversion</p><h2 id=loop-pipelining>Loop pipelining
diff --git a/docs/using-vericert/index.html b/docs/using-vericert/index.html
index 56a0c3a..9ededc8 100644
--- a/docs/using-vericert/index.html
+++ b/docs/using-vericert/index.html
@@ -3,7 +3,8 @@ void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) { in
 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>
 <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 following C file (<code>main.c</code>):</p><div class=highlight><pre class=chroma><code class=language-C data-lang=C><span class=kt>void</span> <span class=nf>matrix_multiply</span><span class=p>(</span><span class=kt>int</span> <span class=n>first</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>],</span> <span class=kt>int</span> <span class=n>second</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>],</span> <span class=kt>int</span> <span class=n>multiply</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>])</span> <span class=p>{</span>
+<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
+following C file (<code>main.c</code>):</p><div class=highlight><pre class=chroma><code class=language-C data-lang=C><span class=kt>void</span> <span class=nf>matrix_multiply</span><span class=p>(</span><span class=kt>int</span> <span class=n>first</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>],</span> <span class=kt>int</span> <span class=n>second</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>],</span> <span class=kt>int</span> <span class=n>multiply</span><span class=p>[</span><span class=mi>2</span><span class=p>][</span><span class=mi>2</span><span class=p>])</span> <span class=p>{</span>
     <span class=kt>int</span> <span class=n>sum</span> <span class=o>=</span> <span class=mi>0</span><span class=p>;</span>
     <span class=k>for</span> <span class=p>(</span><span class=kt>int</span> <span class=n>c</span> <span class=o>=</span> <span class=mi>0</span><span class=p>;</span> <span class=n>c</span> <span class=o>&lt;</span> <span class=mi>2</span><span class=p>;</span> <span class=n>c</span><span class=o>++</span><span class=p>)</span> <span class=p>{</span>
 	<span class=k>for</span> <span class=p>(</span><span class=kt>int</span> <span class=n>d</span> <span class=o>=</span> <span class=mi>0</span><span class=p>;</span> <span class=n>d</span> <span class=o>&lt;</span> <span class=mi>2</span><span class=p>;</span> <span class=n>d</span><span class=o>++</span><span class=p>)</span> <span class=p>{</span>
@@ -24,12 +25,14 @@ void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) { in
     <span class=n>matrix_multiply</span><span class=p>(</span><span class=n>f</span><span class=p>,</span> <span class=n>s</span><span class=p>,</span> <span class=n>m</span><span class=p>);</span>
     <span class=k>return</span> <span class=n>m</span><span class=p>[</span><span class=mi>1</span><span class=p>][</span><span class=mi>1</span><span class=p>];</span>
 <span class=p>}</span>
-</code></pre></div><p>It can be compiled using the following command, assuming that vericert is somewhere on the path.</p><pre><code class=language-nil data-lang=nil>vericert main.c -o main.v
-</code></pre><p>The Verilog file contains a top-level test-bench, which can be given to any Verilog simulator to simulate the hardware, which should give the same result as executing the C code. Using <a href=http://iverilog.icarus.com/>Icarus Verilog</a> as an example:</p><pre><code class=language-nil data-lang=nil>iverilog -o main_v main.v
-</code></pre><p>When executing, it should therefore print the following:</p><pre><code class=language-nil data-lang=nil>$ ./main_v
-finished: 50
-</code></pre><p>This gives the same result as executing the C in the following way:</p><pre><code class=language-nil data-lang=nil>$ gcc -o main_c main.c
+</code></pre></div><p>It can be compiled using the following command, assuming that vericert is somewhere on the path.</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>vericert main.c -o main.v
+</code></pre></div><p>The Verilog file contains a top-level test-bench, which can be given to any Verilog simulator to
+simulate the hardware, which should give the same result as executing the C code. Using <a href=http://iverilog.icarus.com/>Icarus
+Verilog</a> as an example:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>iverilog -o main_v main.v
+</code></pre></div><p>When executing, it should therefore print the following:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>$ ./main_v
+finished: <span class=m>50</span>
+</code></pre></div><p>This gives the same result as executing the C in the following way:</p><div class=highlight><pre class=chroma><code class=language-shell data-lang=shell>$ gcc -o main_c main.c
 $ ./main_c
-$ echo $?
-50
-</code></pre></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
+$ <span class=nb>echo</span> <span class=nv>$?</span>
+<span class=m>50</span>
+</code></pre></div></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
author	ymherklotz <ymherklotz@users.noreply.github.com>	2021-09-19 00:54:08 +0000
committer	ymherklotz <ymherklotz@users.noreply.github.com>	2021-09-19 00:54:08 +0000
commit	a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d (patch)
tree	52ad54ef5468d7755357dd0a2d513af94c3ea9b5 /docs
parent	20a623794340113684dfeb5a7ff2e78f6a4d35f3 (diff)
download	vericert-docs-a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d.tar.gz vericert-docs-a6fdaf10c24b5b01921b34b1d2cfc9ef3c23d50d.zip