diff options
| author | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-09-19 00:47:41 +0000 |
|---|---|---|
| committer | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-09-19 00:47:41 +0000 |
| commit | 20a623794340113684dfeb5a7ff2e78f6a4d35f3 (patch) | |
| tree | fb621903c27c106d94119bfc830992d0c4413a9e | |
| parent | 182d57ff0cd3baf682d722cfad441cf2872012a4 (diff) | |
| download | vericert-docs-20a623794340113684dfeb5a7ff2e78f6a4d35f3.tar.gz vericert-docs-20a623794340113684dfeb5a7ff2e78f6a4d35f3.zip | |
deploy: b6de77b0c4392dbfaa365b709cab99222f8dfa84
| -rw-r--r-- | docs/index.html | 2 | ||||
| -rw-r--r-- | index.html | 2 | ||||
| -rw-r--r-- | index.xml | 2 | ||||
| -rw-r--r-- | sitemap.xml | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/docs/index.html b/docs/index.html index f4be53e..5c47f44 100644 --- a/docs/index.html +++ b/docs/index.html @@ -4,4 +4,4 @@ The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation."><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Docs"><meta property="og:description" content><meta property="og:type" content="website"><meta property="og:url" content="https://vericert.ymhg.org/docs/"><title>Docs |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script><link rel=alternate type=application/rss+xml href=https://vericert.ymhg.org/docs/index.xml></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><span></span></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/coq-style-guide/>Coq Style Guide</a></li><li><a href=https://vericert.ymhg.org/docs/ class=active>Docs</a><ul><li><a href=https://vericert.ymhg.org/docs/building/>Building Vericert</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/>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>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><h1>Docs</h1><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=org0cc892a></a></p><figure><img src=/images/design.jpg 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=#org0cc892a>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 +<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><h1>Docs</h1><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=org52e0c8a></a></p><figure><img src=/images/design.jpg 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=#org52e0c8a>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 @@ -1,5 +1,5 @@ <!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="A formally verified high-level synthesis (HLS) tool written in Coq, building on top of CompCert. This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert’s C semantics, removing the need to check the resulting hardware for behavioural correctness. -Features # The project is currently a work in progress, so proofs remain to be finished. Currently, the following C features are supported, but are not all proven correct yet:"><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Vericert"><meta property="og:description" content><meta property="og:type" content="website"><meta property="og:url" content="https://vericert.ymhg.org/"><meta property="og:updated_time" content="2021-01-16T00:00:00+00:00"><title>Vericert |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script><link rel=alternate type=application/rss+xml href=https://vericert.ymhg.org/index.xml></head><body><input type=checkbox class="hidden toggle" id=menu-control> +Features # The project is currently a work in progress, so proofs remain to be finished. Currently, the following C features are supported, but are not all proven correct yet:"><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Vericert"><meta property="og:description" content><meta property="og:type" content="website"><meta property="og:url" content="https://vericert.ymhg.org/"><title>Vericert |</title><link rel=manifest href=/manifest.json><link rel=icon href=/favicon.png type=image/x-icon><link rel=stylesheet href=/book.min.b07e338e07a9a926c141d155a3e6d06d0c41e4afe4d81564015c56799705b0ca.css integrity="sha256-sH4zjgepqSbBQdFVo+bQbQxB5K/k2BVkAVxWeZcFsMo="><script defer src=/en.search.min.09c4470fdacb71a68922c07311d906b9cd808586067883b11db52f10e30e96d4.js integrity="sha256-CcRHD9rLcaaJIsBzEdkGuc2AhYYGeIOxHbUvEOMOltQ="></script><link rel=alternate type=application/rss+xml href=https://vericert.ymhg.org/index.xml></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><span></span></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/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/unreleased/>Unreleased Features</a></li><li><a href=https://vericert.ymhg.org/docs/using-vericert/>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>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><ul><li><ul><li><a href=#features>Features</a></li><li><a href=#content>Content</a></li><li><a href=#papers>Papers</a></li></ul></li></ul></nav></aside></header><h1>Vericert</h1><article class=markdown><p>A formally verified high-level synthesis (HLS) tool written in Coq, building on top of <a href=https://github.com/AbsInt/CompCert>CompCert</a>. This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert’s C semantics, removing the need to check the resulting hardware for behavioural correctness.</p><h2 id=features>Features @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8" standalone="yes"?><rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Vericert on</title><link>https://vericert.ymhg.org/</link><description>Recent content in Vericert on</description><generator>Hugo -- gohugo.io</generator><language>en-us</language><copyright>© 2020-2021 Yann Herklotz</copyright><lastBuildDate>Sat, 16 Jan 2021 00:00:00 +0000</lastBuildDate><atom:link href="https://vericert.ymhg.org/index.xml" rel="self" type="application/rss+xml"/><item><title>Building Vericert</title><link>https://vericert.ymhg.org/docs/building/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>https://vericert.ymhg.org/docs/building/</guid><description>To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with nix using the provided default.nix and shell.nix files. +<?xml version="1.0" encoding="utf-8" standalone="yes"?><rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Vericert on</title><link>https://vericert.ymhg.org/</link><description>Recent content in Vericert on</description><generator>Hugo -- gohugo.io</generator><language>en-us</language><copyright>© 2020-2021 Yann Herklotz</copyright><atom:link href="https://vericert.ymhg.org/index.xml" rel="self" type="application/rss+xml"/><item><title>Building Vericert</title><link>https://vericert.ymhg.org/docs/building/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>https://vericert.ymhg.org/docs/building/</guid><description>To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with nix using the provided default.nix and shell.nix files. The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following: Coq: theorem prover that is used to also program the HLS tool.</description></item><item><title>Coq Style Guide</title><link>https://vericert.ymhg.org/coq-style-guide/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>https://vericert.ymhg.org/coq-style-guide/</guid><description>This style guide was taken from Silveroak, it outlines code style for Coq code in this repository. There are certainly other valid strategies and opinions on Coq code style; this is laid out purely in the name of consistency. For a visual example of the style, see the example at the bottom of this file. Code organization # Legal banner # Files should begin with a copyright/license banner, as shown in the example above.</description></item><item><title>Future Work</title><link>https://vericert.ymhg.org/future/</link><pubDate>Mon, 01 Jan 0001 00:00:00 +0000</pubDate><guid>https://vericert.ymhg.org/future/</guid><description>This section contains future work that should be added to Vericert to make it into a better high-level synthesis tool. diff --git a/sitemap.xml b/sitemap.xml index b2166cf..8ab2110 100644 --- a/sitemap.xml +++ b/sitemap.xml @@ -1 +1 @@ -<?xml version="1.0" encoding="utf-8" standalone="yes"?><urlset xmlns="http://www.sitemaps.org/schemas/sitemap/0.9" xmlns:xhtml="http://www.w3.org/1999/xhtml"><url><loc>https://vericert.ymhg.org/</loc><lastmod>2021-01-16T00:00:00+00:00</lastmod></url><url><loc>https://vericert.ymhg.org/docs/building/</loc></url><url><loc>https://vericert.ymhg.org/categories/</loc></url><url><loc>https://vericert.ymhg.org/coq-style-guide/</loc></url><url><loc>https://vericert.ymhg.org/docs/</loc></url><url><loc>https://vericert.ymhg.org/future/</loc></url><url><loc>https://vericert.ymhg.org/tags/</loc></url><url><loc>https://vericert.ymhg.org/docs/unreleased/</loc></url><url><loc>https://vericert.ymhg.org/docs/using-vericert/</loc></url></urlset>
\ No newline at end of file +<?xml version="1.0" encoding="utf-8" standalone="yes"?><urlset xmlns="http://www.sitemaps.org/schemas/sitemap/0.9" xmlns:xhtml="http://www.w3.org/1999/xhtml"><url><loc>https://vericert.ymhg.org/docs/building/</loc></url><url><loc>https://vericert.ymhg.org/categories/</loc></url><url><loc>https://vericert.ymhg.org/coq-style-guide/</loc></url><url><loc>https://vericert.ymhg.org/docs/</loc></url><url><loc>https://vericert.ymhg.org/future/</loc></url><url><loc>https://vericert.ymhg.org/tags/</loc></url><url><loc>https://vericert.ymhg.org/docs/unreleased/</loc></url><url><loc>https://vericert.ymhg.org/docs/using-vericert/</loc></url><url><loc>https://vericert.ymhg.org/</loc></url></urlset>
\ No newline at end of file |