1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
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. 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.0faad4b80b963ba9a029cd4fce44afdc8cf46575513a229f054a74530a26c80f.css integrity="sha256-D6rUuAuWO6mgKc1PzkSv3Iz0ZXVROiKfBUp0UwomyA8="><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. 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><</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><</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><</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>
|
