diff options
| author | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-09-20 09:02:50 +0000 |
|---|---|---|
| committer | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-09-20 09:02:50 +0000 |
| commit | 83aaa860b691697d59b83fadac2c4dad51972387 (patch) | |
| tree | f6a647979875be79a2f7b044cc54d99317938840 /docs/index.html | |
| parent | 80568aaef48fab6aff08d0cc724909e5afeee5dd (diff) | |
| download | vericert-docs-83aaa860b691697d59b83fadac2c4dad51972387.tar.gz vericert-docs-83aaa860b691697d59b83fadac2c4dad51972387.zip | |
deploy: d9f8dee1a294ee087f56c6e54b16ad3b0bf8d895
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 6b5a5be..03748e7 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=org332cb94></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=#org332cb94>1</a> shows how Vericert leverages an existing verified C compiler +application-specific integrated circuit (ASIC).</p><p><a id=orgeab21f5></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=#orgeab21f5>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 |