From 95bb2fda796ca17ad9cbb213dd15690ef6346c35 Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Fri, 2 Apr 2021 12:57:22 +0000 Subject: deploy: f85153b7335ebf99ab6bf6e696b5a08fef38b61b --- docs/building/index.html | 4 ++-- docs/index.html | 6 +++--- docs/index.xml | 5 +++-- docs/unreleased/index.html | 11 +++++++++++ docs/using-vericert/index.html | 4 ++-- 5 files changed, 21 insertions(+), 9 deletions(-) create mode 100644 docs/unreleased/index.html (limited to 'docs') diff --git a/docs/building/index.html b/docs/building/index.html index 2fa9951..c761f82 100644 --- a/docs/building/index.html +++ b/docs/building/index.html @@ -2,8 +2,8 @@ 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.">Building Vericert | Vericert -
+ Coq: theorem prover that is used to also program the HLS tool.">Building Vericert | +
Building Vericert

Building Vericert

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.

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
diff --git a/docs/index.html b/docs/index.html
index 3ef9d95..7319b68 100644
--- a/docs/index.html
+++ b/docs/index.html
@@ -1,7 +1,7 @@
 Docs | Vericert
-

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

 Docs
-
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.
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
+
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.
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 2807f93..42dff8e 100644
--- a/docs/index.xml
+++ b/docs/index.xml
@@ -1,4 +1,5 @@
-Docs on Vericerthttps://vericert.ymhg.org/docs/Recent content in Docs on VericertHugo -- gohugo.ioen-us© 2020-2021 Yann HerklotzBuilding Vericerthttps://vericert.ymhg.org/docs/building/Mon, 01 Jan 0001 00:00:00 +0000https://vericert.ymhg.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 onhttps://vericert.ymhg.org/docs/Recent content in Docs onHugo -- gohugo.ioen-us© 2020-2021 Yann HerklotzBuilding Vericerthttps://vericert.ymhg.org/docs/building/Mon, 01 Jan 0001 00:00:00 +0000https://vericert.ymhg.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.
 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 Vericerthttps://vericert.ymhg.org/docs/using-vericert/Mon, 01 Jan 0001 00:00:00 +0000https://vericert.ymhg.org/docs/using-vericert/Vericert can be used to translate a subset of C into Verilog. As a simple example, consider the following C file (main.c):
+Coq: theorem prover that is used to also program the HLS tool.Unreleased Featureshttps://vericert.ymhg.org/docs/unreleased/Mon, 01 Jan 0001 00:00:00 +0000https://vericert.ymhg.org/docs/unreleased/The following are unreleased features in Vericert that are currently being worked on and have not been completely proven correct yet. Currently this includes features such as:
+scheduling, if-conversion, loop pipelining, and functions. This page gives some preliminary information on how the features are implemented and how the proofs for the features are being done. Once these features are properly implemented, they will be added to the proper documentation.Using Vericerthttps://vericert.ymhg.org/docs/using-vericert/Mon, 01 Jan 0001 00:00:00 +0000https://vericert.ymhg.org/docs/using-vericert/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.
\ No newline at end of file
diff --git a/docs/unreleased/index.html b/docs/unreleased/index.html
new file mode 100644
index 0000000..1cf635a
--- /dev/null
+++ b/docs/unreleased/index.html
@@ -0,0 +1,11 @@
+Unreleased Features |
+

+Unreleased Features
+
Unreleased Features
The following are unreleased features in Vericert that are currently being worked on and have not been completely proven correct yet. Currently this includes features such as:
This page gives some preliminary information on how the features are implemented and how the proofs for the features are being done. Once these features are properly implemented, they will be added to the proper documentation.
Scheduling
+#
Scheduling is an optimisation which is used to run
Operation Chaining
+#
Scheduling is an optimisation which is used to run
If-conversion
+#
If-conversion
Loop pipelining
+#
Loop pipelining
Functions
+#
Functions.

\ No newline at end of file
diff --git a/docs/using-vericert/index.html b/docs/using-vericert/index.html
index d410356..56a0c3a 100644
--- a/docs/using-vericert/index.html
+++ b/docs/using-vericert/index.html
@@ -1,7 +1,7 @@
 Using Vericert | Vericert
-

+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.">Using Vericert |
+

 Using Vericert
 
Using Vericert
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;
-- 
cgit