diff options
author | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-09-23 10:05:30 +0000 |
---|---|---|
committer | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-09-23 10:05:30 +0000 |
commit | 0fcfc52bb1eb3a4b420ba29c012737fc5fcb69eb (patch) | |
tree | 6a707bd54796f761b879e141e919a543104785cc /docs/index.html | |
parent | bb9ad00fce55d539a2cb7664ced14b78a3c681fb (diff) | |
download | vericert-docs-gh-pages.tar.gz vericert-docs-gh-pages.zip |
deploy: 42e19f2b20c907505a28486a8071147ed6c610fbgh-pages
Diffstat (limited to 'docs/index.html')
-rw-r--r-- | docs/index.html | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/index.html b/docs/index.html index 2a9f2ce..eda0422 100644 --- a/docs/index.html +++ b/docs/index.html @@ -6,5 +6,5 @@ <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><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=org8d9f0d3></a></p><figure><img src=/images/toolflow.svg 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=#org8d9f0d3>1</a> shows how Vericert leverages an existing verified C compiler +application-specific integrated circuit (ASIC).</p><p><a id=orge360ee1></a></p><figure><img src=/images/toolflow.svg 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=#orge360ee1>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 |