404 Page not found

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.
OCaml: the OCaml compiler to compile the extracted files.
bbv: an efficient bit vector library.
dune: build tool for ocaml projects to gather all the ocaml files and compile them in the right order.
menhir: parser generator for ocaml.
findlib to find installed OCaml libraries.
GCC: compiler to help build CompCert.

These dependencies can be installed manually, or automatically through Nix.

Definition help := 0.

`Downloading CompCert #`

CompCert is added as a submodule in the lib/CompCert directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run:

git clone --recursive https://github.com/ymherklotz/vericert

If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded:

git submodule update --init
diff --git a/docs/index.html b/docs/index.html
index c264cdc..12c9fe0 100644
--- a/docs/index.html
+++ b/docs/index.html
@@ -1,7 +1,7 @@
 Docs | Vericert
-Vericert
DocsBuilding Vericert
Using Vericert
Github

+  The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation.">Docs | Vericert
+Vericert
DocsBuilding Vericert
Using Vericert
Github

 Docs
-
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).
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.
The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation.

\ No newline at end of file
+
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).
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.
The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation.

\ No newline at end of file
diff --git a/docs/index.xml b/docs/index.xml
index 03139d4..199ed30 100644
--- a/docs/index.xml
+++ b/docs/index.xml
@@ -1,3 +1,3 @@
-Docs on Vericerthttp://example.org/docs/Recent content in Docs on VericertHugo -- gohugo.ioen-us© 2020-2021 Yann HerklotzBuilding Vericerthttp://example.org/docs/building/Mon, 01 Jan 0001 00:00:00 +0000http://example.org/docs/building/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.
+Docs on Vericerthttps://ymherklotz.github.io/vericert-docs/docs/Recent content in Docs on VericertHugo -- gohugo.ioen-us© 2020-2021 Yann HerklotzBuilding Vericerthttps://ymherklotz.github.io/vericert-docs/docs/building/Mon, 01 Jan 0001 00:00:00 +0000https://ymherklotz.github.io/vericert-docs/docs/building/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.Using Vericerthttp://example.org/docs/using-vericert/Mon, 01 Jan 0001 00:00:00 +0000http://example.org/docs/using-vericert/Vericert can be used to translate a subset of C into Verilog.
\ No newline at end of file
+Coq: theorem prover that is used to also program the HLS tool.Using Vericerthttps://ymherklotz.github.io/vericert-docs/docs/using-vericert/Mon, 01 Jan 0001 00:00:00 +0000https://ymherklotz.github.io/vericert-docs/docs/using-vericert/Vericert can be used to translate a subset of C into Verilog.
\ No newline at end of file
diff --git a/docs/using-vericert/index.html b/docs/using-vericert/index.html
index 6d9d6f7..750e168 100644
--- a/docs/using-vericert/index.html
+++ b/docs/using-vericert/index.html
@@ -1,4 +1,4 @@
-Using Vericert | Vericert
-Vericert
DocsBuilding Vericert
Using Vericert
Github

+Using Vericert | Vericert
+Vericert
DocsBuilding Vericert
Using Vericert
Github

 Using Vericert
-
Vericert can be used to translate a subset of C into Verilog.

\ No newline at end of file
+
Vericert can be used to translate a subset of C into Verilog.

\ No newline at end of file
diff --git a/en.search-data.min.0015af60283cd2484bb334b5af19a373f6f03d1acd9757a629ebc0830ef9e9a6.js b/en.search-data.min.0015af60283cd2484bb334b5af19a373f6f03d1acd9757a629ebc0830ef9e9a6.js
deleted file mode 100644
index 5560a56..0000000
--- a/en.search-data.min.0015af60283cd2484bb334b5af19a373f6f03d1acd9757a629ebc0830ef9e9a6.js
+++ /dev/null
@@ -1 +0,0 @@
-'use strict';(function(){const indexCfg={cache:true};indexCfg.doc={id:'id',field:['title','content'],store:['title','href','section'],};const index=FlexSearch.create('balance',indexCfg);window.bookSearchIndex=index;index.add({'id':0,'href':'/docs/building/','title':"Building Vericert",'section':"Docs",'content':"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.\nThe 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:\n Coq: theorem prover that is used to also program the HLS tool. OCaml: the OCaml compiler to compile the extracted files. bbv: an efficient bit vector library. dune: build tool for ocaml projects to gather all the ocaml files and compile them in the right order. menhir: parser generator for ocaml. findlib to find installed OCaml libraries. GCC: compiler to help build CompCert.  These dependencies can be installed manually, or automatically through Nix.\nDefinition help := 0. Downloading CompCert #  CompCert is added as a submodule in the lib/CompCert directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run:\ngit clone --recursive https://github.com/ymherklotz/vericert If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded:\ngit submodule update --init Setting up Nix #  Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way.\nTo open a shell which includes all the necessary dependencies, one can use:\nnix-shell which will open a shell that has all the dependencies loaded.\nMakefile build #  If the dependencies were installed manually, or if one is in the nix-shell, the project can be built by running:\nmake -j8 and installed locally, or under the PREFIX location using:\nmake install Which will install the binary in ./bin/vericert by default. However, this can be changed by changing the PREFIX environment variable, in which case the binary will be installed in $PREFIX/bin/vericert.\nTesting #  To test out vericert you can try the following examples which are in the test folder using the following:\n./bin/vericert test/loop.c -o loop.v ./bin/vericert test/conditional.c -o conditional.v ./bin/vericert test/add.c -o add.v Or by running the test suite using the following command:\nmake test "});index.add({'id':1,'href':'/docs/','title':"Docs",'section':"Vericert",'content':"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).\n\n  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.\n  The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation.\n"});index.add({'id':2,'href':'/docs/using-vericert/','title':"Using Vericert",'section':"Docs",'content':"Vericert can be used to translate a subset of C into Verilog.\n"});})();
\ No newline at end of file
diff --git a/en.search-data.min.7b5933dbdcf2b2b8e261bda6e5d9a67f20411606895154199be29ff129a8c1be.js b/en.search-data.min.7b5933dbdcf2b2b8e261bda6e5d9a67f20411606895154199be29ff129a8c1be.js
new file mode 100644
index 0000000..e77cf92
--- /dev/null
+++ b/en.search-data.min.7b5933dbdcf2b2b8e261bda6e5d9a67f20411606895154199be29ff129a8c1be.js
@@ -0,0 +1 @@
+'use strict';(function(){const indexCfg={cache:true};indexCfg.doc={id:'id',field:['title','content'],store:['title','href','section'],};const index=FlexSearch.create('balance',indexCfg);window.bookSearchIndex=index;index.add({'id':0,'href':'/vericert-docs/docs/building/','title':"Building Vericert",'section':"Docs",'content':"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.\nThe 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:\n Coq: theorem prover that is used to also program the HLS tool. OCaml: the OCaml compiler to compile the extracted files. bbv: an efficient bit vector library. dune: build tool for ocaml projects to gather all the ocaml files and compile them in the right order. menhir: parser generator for ocaml. findlib to find installed OCaml libraries. GCC: compiler to help build CompCert.  These dependencies can be installed manually, or automatically through Nix.\nDefinition help := 0. Downloading CompCert #  CompCert is added as a submodule in the lib/CompCert directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run:\ngit clone --recursive https://github.com/ymherklotz/vericert If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded:\ngit submodule update --init Setting up Nix #  Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way.\nTo open a shell which includes all the necessary dependencies, one can use:\nnix-shell which will open a shell that has all the dependencies loaded.\nMakefile build #  If the dependencies were installed manually, or if one is in the nix-shell, the project can be built by running:\nmake -j8 and installed locally, or under the PREFIX location using:\nmake install Which will install the binary in ./bin/vericert by default. However, this can be changed by changing the PREFIX environment variable, in which case the binary will be installed in $PREFIX/bin/vericert.\nTesting #  To test out vericert you can try the following examples which are in the test folder using the following:\n./bin/vericert test/loop.c -o loop.v ./bin/vericert test/conditional.c -o conditional.v ./bin/vericert test/add.c -o add.v Or by running the test suite using the following command:\nmake test "});index.add({'id':1,'href':'/vericert-docs/docs/','title':"Docs",'section':"Vericert",'content':"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).\n\n  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.\n  The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation.\n"});index.add({'id':2,'href':'/vericert-docs/docs/using-vericert/','title':"Using Vericert",'section':"Docs",'content':"Vericert can be used to translate a subset of C into Verilog.\n"});})();
\ No newline at end of file
diff --git a/en.search.min.77eecb367a48b50a7df2acdb69aba4b0107b4b1306bd8f7510bb929a260db0b1.js b/en.search.min.77eecb367a48b50a7df2acdb69aba4b0107b4b1306bd8f7510bb929a260db0b1.js
new file mode 100644
index 0000000..90f612a
--- /dev/null
+++ b/en.search.min.77eecb367a48b50a7df2acdb69aba4b0107b4b1306bd8f7510bb929a260db0b1.js
@@ -0,0 +1,11 @@
+'use strict';(function(){const input=document.querySelector('#book-search-input');const results=document.querySelector('#book-search-results');if(!input){return}
+input.addEventListener('focus',init);input.addEventListener('keyup',search);document.addEventListener('keypress',focusSearchFieldOnKeyPress);function focusSearchFieldOnKeyPress(event){if(input===document.activeElement){return;}
+const characterPressed=String.fromCharCode(event.charCode);if(!isHotkey(characterPressed)){return;}
+input.focus();event.preventDefault();}
+function isHotkey(character){const dataHotkeys=input.getAttribute('data-hotkeys')||'';return dataHotkeys.indexOf(character)>=0;}
+function init(){input.removeEventListener('focus',init);input.required=true;loadScript('/vericert-docs/flexsearch.min.js');loadScript('/vericert-docs/en.search-data.min.7b5933dbdcf2b2b8e261bda6e5d9a67f20411606895154199be29ff129a8c1be.js',function(){input.required=false;search();});}
+function search(){while(results.firstChild){results.removeChild(results.firstChild);}
+if(!input.value){return;}
+const searchHits=window.bookSearchIndex.search(input.value,10);searchHits.forEach(function(page){const li=element('');const a=li.querySelector('a'),small=li.querySelector('small');a.href=page.href;a.textContent=page.title;small.textContent=page.section;results.appendChild(li);});}
+function loadScript(src,callback){const script=document.createElement('script');script.defer=true;script.async=false;script.src=src;script.onload=callback;document.head.appendChild(script);}
+function element(content){const div=document.createElement('div');div.innerHTML=content;return div.firstChild;}})();
\ No newline at end of file
diff --git a/en.search.min.90cea40d1c9e495620e94dded717dbc4c64fd0e3c89f00dc75212bbfccf36188.js b/en.search.min.90cea40d1c9e495620e94dded717dbc4c64fd0e3c89f00dc75212bbfccf36188.js
deleted file mode 100644
index 0e818fe..0000000
--- a/en.search.min.90cea40d1c9e495620e94dded717dbc4c64fd0e3c89f00dc75212bbfccf36188.js
+++ /dev/null
@@ -1,11 +0,0 @@
-'use strict';(function(){const input=document.querySelector('#book-search-input');const results=document.querySelector('#book-search-results');if(!input){return}
-input.addEventListener('focus',init);input.addEventListener('keyup',search);document.addEventListener('keypress',focusSearchFieldOnKeyPress);function focusSearchFieldOnKeyPress(event){if(input===document.activeElement){return;}
-const characterPressed=String.fromCharCode(event.charCode);if(!isHotkey(characterPressed)){return;}
-input.focus();event.preventDefault();}
-function isHotkey(character){const dataHotkeys=input.getAttribute('data-hotkeys')||'';return dataHotkeys.indexOf(character)>=0;}
-function init(){input.removeEventListener('focus',init);input.required=true;loadScript('/flexsearch.min.js');loadScript('/en.search-data.min.0015af60283cd2484bb334b5af19a373f6f03d1acd9757a629ebc0830ef9e9a6.js',function(){input.required=false;search();});}
-function search(){while(results.firstChild){results.removeChild(results.firstChild);}
-if(!input.value){return;}
-const searchHits=window.bookSearchIndex.search(input.value,10);searchHits.forEach(function(page){const li=element('');const a=li.querySelector('a'),small=li.querySelector('small');a.href=page.href;a.textContent=page.title;small.textContent=page.section;results.appendChild(li);});}
-function loadScript(src,callback){const script=document.createElement('script');script.defer=true;script.async=false;script.src=src;script.onload=callback;document.head.appendChild(script);}
-function element(content){const div=document.createElement('div');div.innerHTML=content;return div.firstChild;}})();
\ No newline at end of file
diff --git a/index.html b/index.html
index e27bcc8..4b44540 100644
--- a/index.html
+++ b/index.html
@@ -1,7 +1,7 @@
 Vericert | Vericert
-Vericert
DocsBuilding Vericert
Using Vericert
Github

+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:">Vericert | Vericert
+Vericert
DocsBuilding Vericert
Using Vericert
Github

 Vericert
-
Features
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
+
Features
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:
all int operations,
non-recursive function calls,
local arrays and pointers
control-flow structures such as if-statements, for-loops, etc…
Content
 #
Vericert Documentation
Features
Content
\ No newline at end of file
diff --git a/index.xml b/index.xml
index bc4d48b..4311f90 100644
--- a/index.xml
+++ b/index.xml
@@ -1,3 +1,3 @@
-Vericerthttp://example.org/Recent content on VericertHugo -- gohugo.ioen-us© 2020-2021 Yann HerklotzSat, 16 Jan 2021 00:00:00 +0000Building Vericerthttp://example.org/docs/building/Mon, 01 Jan 0001 00:00:00 +0000http://example.org/docs/building/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.
+Vericerthttps://ymherklotz.github.io/vericert-docs/Recent content on VericertHugo -- gohugo.ioen-us© 2020-2021 Yann HerklotzSat, 16 Jan 2021 00:00:00 +0000Building Vericerthttps://ymherklotz.github.io/vericert-docs/docs/building/Mon, 01 Jan 0001 00:00:00 +0000https://ymherklotz.github.io/vericert-docs/docs/building/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.Using Vericerthttp://example.org/docs/using-vericert/Mon, 01 Jan 0001 00:00:00 +0000http://example.org/docs/using-vericert/Vericert can be used to translate a subset of C into Verilog.
\ No newline at end of file
+Coq: theorem prover that is used to also program the HLS tool.Using Vericerthttps://ymherklotz.github.io/vericert-docs/docs/using-vericert/Mon, 01 Jan 0001 00:00:00 +0000https://ymherklotz.github.io/vericert-docs/docs/using-vericert/Vericert can be used to translate a subset of C into Verilog.
\ No newline at end of file
diff --git a/manifest.json b/manifest.json
index c9bce8a..03239bf 100644
--- a/manifest.json
+++ b/manifest.json
@@ -1,14 +1,14 @@
 {
   "name": "Vericert",
   "short_name": "Vericert",
-  "start_url": "/",
-  "scope": "/",
+  "start_url": "/vericert-docs/",
+  "scope": "/vericert-docs/",
   "display": "standalone",
   "background_color": "#000000",
   "theme_color": "#000000",
   "icons": [
     {
-      "src": "/favicon.svg",
+      "src": "/vericert-docs/favicon.svg",
       "sizes": "512x512"
     }
   ]
diff --git a/sitemap.xml b/sitemap.xml
index 30483a3..f673ffb 100644
--- a/sitemap.xml
+++ b/sitemap.xml
@@ -1 +1 @@
-http://example.org/2021-01-16T00:00:00+00:00http://example.org/docs/building/http://example.org/categories/http://example.org/docs/http://example.org/tags/http://example.org/docs/using-vericert/
\ No newline at end of file
+https://ymherklotz.github.io/vericert-docs/2021-01-16T00:00:00+00:00https://ymherklotz.github.io/vericert-docs/docs/building/https://ymherklotz.github.io/vericert-docs/categories/https://ymherklotz.github.io/vericert-docs/docs/https://ymherklotz.github.io/vericert-docs/tags/https://ymherklotz.github.io/vericert-docs/docs/using-vericert/
\ No newline at end of file
diff --git a/tags/index.html b/tags/index.html
index 2cb3928..43a844e 100644
--- a/tags/index.html
+++ b/tags/index.html
@@ -1,4 +1,4 @@
-Tags | Vericert
-Vericert
DocsBuilding Vericert
Using Vericert
Github

+Tags | Vericert
+Vericert
DocsBuilding Vericert
Using Vericert
Github

 Tags
-
Categories
Tags
Categories
Tags
\ No newline at end of file
+
Categories
Tags
Categories
Tags
\ No newline at end of file
diff --git a/tags/index.xml b/tags/index.xml
index 6331734..fa76a12 100644
--- a/tags/index.xml
+++ b/tags/index.xml
@@ -1 +1 @@
-Tags on Vericerthttp://example.org/tags/Recent content in Tags on VericertHugo -- gohugo.ioen-us© 2020-2021 Yann Herklotz
\ No newline at end of file
+Tags on Vericerthttps://ymherklotz.github.io/vericert-docs/tags/Recent content in Tags on VericertHugo -- gohugo.ioen-us© 2020-2021 Yann Herklotz
\ No newline at end of file
diff --git a/tags/page/1/index.html b/tags/page/1/index.html
index 42616e4..ea10702 100644
--- a/tags/page/1/index.html
+++ b/tags/page/1/index.html
@@ -1 +1 @@
-http://example.org/tags/
\ No newline at end of file
+https://ymherklotz.github.io/vericert-docs/tags/
\ No newline at end of file
-- 
cgit

404

Page Not Found

Vericert

404

Page Not Found

Vericert

`Downloading CompCert #`

Features +

Features #

Content #