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
36
37
38
|
<!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.92c1de61cce4ee29dff6c954131fab2f5270d34b966e42f893b9227dc1d3f68f.css integrity="sha256-ksHeYczk7inf9slUEx+rL1Jw00uWbkL4k7kifcHT9o8="><script defer src=/en.search.min.8744a59deef42a09f73b965fa29a56c40c4f8892dff5bfae0b331df4b63bb70d.js integrity="sha256-h0Slne70Kgn3O5ZfoppWxAxPiJLf9b+uCzMd9LY7tw0="></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></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/blog/>Blog</a><ul></ul></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/coq-style-guide/>Coq Style Guide</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><article class=markdown><h1><a href=/docs/using-vericert/>Using Vericert</a></h1><p><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><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
$ <span class=nb>echo</span> <span class=nv>$?</span>
<span class=m>50</span>
</code></pre></div></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>
|
