deploy: e38739e42b8b7da37027b86cf58cc114d5224d69

author: ymherklotz <ymherklotz@users.noreply.github.com> 2021-01-22 13:00:13 +0000
committer: ymherklotz <ymherklotz@users.noreply.github.com> 2021-01-22 13:00:13 +0000
commit: af25d179c9bfa2aa4585f14210aa11906965f045 (patch)
tree: ca8e45cf74f2b876c4e21947e6ccccb5a812aa37 /docs/using-vericert
parent: bdaa8844be64818cab4bd8e77e91bb7af0bfcf98 (diff)
download: vericert-docs-af25d179c9bfa2aa4585f14210aa11906965f045.tar.gz
vericert-docs-af25d179c9bfa2aa4585f14210aa11906965f045.zip
1 files changed, 34 insertions, 3 deletions
diff --git a/docs/using-vericert/index.html b/docs/using-vericert/index.html
index 5f7cbbd..9d9df41 100644
--- a/docs/using-vericert/index.html
+++ b/docs/using-vericert/index.html
@@ -1,4 +1,35 @@
-<!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://vericert.ymhg.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.a4d6f3160019c50a1674877d2ccd95fce25e9106249985d3c32868cd7e574c28.css integrity="sha256-pNbzFgAZxQoWdId9LM2V/OJekQYkmYXTwyhozX5XTCg="><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=https://vericert.ymhg.org/docs/>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/ 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. 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 | Vericert</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.a4d6f3160019c50a1674877d2ccd95fce25e9106249985d3c32868cd7e574c28.css integrity="sha256-pNbzFgAZxQoWdId9LM2V/OJekQYkmYXTwyhozX5XTCg="><script defer src=/en.search.min.0954d4b2fc6bff27e6f999bbc5c4fd9011adb3be3811a6642db8ce343b98ef63.js integrity="sha256-CVTUsvxr/yfm+Zm7xcT9kBGts744EaZkLbjONDuY72M="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control>
+<input type=checkbox class="hidden toggle" id=toc-control><main class="container flex"><aside class=book-menu><nav><h2 class=book-brand><a href=/><span>Vericert</span></a></h2><div class=book-search><input type=text id=book-search-input placeholder=Search aria-label=Search maxlength=64 data-hotkeys=s/><div class="book-search-spinner hidden"></div><ul id=book-search-results></ul></div><ul><li><a href=https://vericert.ymhg.org/coq-style-guide/>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/ 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>
 <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=/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. 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>
+	    <span class=k>for</span> <span class=p>(</span><span class=kt>int</span> <span class=n>k</span> <span class=o>=</span> <span class=mi>0</span><span class=p>;</span> <span class=n>k</span> <span class=o>&lt;</span> <span class=mi>2</span><span class=p>;</span> <span class=n>k</span><span class=o>++</span><span class=p>)</span> <span class=p>{</span>
+		<span class=n>sum</span> <span class=o>=</span> <span class=n>sum</span> <span class=o>+</span> <span class=n>first</span><span class=p>[</span><span class=n>c</span><span class=p>][</span><span class=n>k</span><span class=p>]</span><span class=o>*</span><span class=n>second</span><span class=p>[</span><span class=n>k</span><span class=p>][</span><span class=n>d</span><span class=p>];</span>
+	    <span class=p>}</span>
+	    <span class=n>multiply</span><span class=p>[</span><span class=n>c</span><span class=p>][</span><span class=n>d</span><span class=p>]</span> <span class=o>=</span> <span class=n>sum</span><span class=p>;</span>
+	    <span class=n>sum</span> <span class=o>=</span> <span class=mi>0</span><span class=p>;</span>
+	<span class=p>}</span>
+    <span class=p>}</span>
+<span class=p>}</span>
+
+<span class=kt>int</span> <span class=nf>main</span><span class=p>()</span> <span class=p>{</span>
+    <span class=kt>int</span> <span class=n>f</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=o>=</span> <span class=p>{{</span><span class=mi>1</span><span class=p>,</span> <span class=mi>2</span><span class=p>},</span> <span class=p>{</span><span class=mi>3</span><span class=p>,</span> <span class=mi>4</span><span class=p>}};</span>
+    <span class=kt>int</span> <span class=n>s</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=o>=</span> <span class=p>{{</span><span class=mi>5</span><span class=p>,</span> <span class=mi>6</span><span class=p>},</span> <span class=p>{</span><span class=mi>7</span><span class=p>,</span> <span class=mi>8</span><span class=p>}};</span>
+    <span class=kt>int</span> <span class=n>m</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=o>=</span> <span class=p>{{</span><span class=mi>0</span><span class=p>,</span> <span class=mi>0</span><span class=p>},</span> <span class=p>{</span><span class=mi>0</span><span class=p>,</span> <span class=mi>0</span><span class=p>}};</span>
+
+    <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
+$ ./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
author	ymherklotz <ymherklotz@users.noreply.github.com>	2021-01-22 13:00:13 +0000
committer	ymherklotz <ymherklotz@users.noreply.github.com>	2021-01-22 13:00:13 +0000
commit	af25d179c9bfa2aa4585f14210aa11906965f045 (patch)
tree	ca8e45cf74f2b876c4e21947e6ccccb5a812aa37 /docs/using-vericert
parent	bdaa8844be64818cab4bd8e77e91bb7af0bfcf98 (diff)
download	vericert-docs-af25d179c9bfa2aa4585f14210aa11906965f045.tar.gz vericert-docs-af25d179c9bfa2aa4585f14210aa11906965f045.zip