From aca7b8f57370ccdba41577c845361800ae6f8d39 Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Fri, 22 Jan 2021 17:23:49 +0000 Subject: deploy: 1ff8b1c7a3f3e37809e9ac8c1e21d50df270696a --- docs/building/index.html | 2 +- docs/index.html | 4 ++-- docs/using-vericert/index.html | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) (limited to 'docs') diff --git a/docs/building/index.html b/docs/building/index.html index 976571d..20d5841 100644 --- a/docs/building/index.html +++ b/docs/building/index.html @@ -2,7 +2,7 @@ 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 | 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 diff --git a/docs/index.html b/docs/index.html index b8b9228..a38e747 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 | Vericert
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 +

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/using-vericert/index.html b/docs/using-vericert/index.html index 043db1e..c97296d 100644 --- a/docs/using-vericert/index.html +++ b/docs/using-vericert/index.html @@ -1,6 +1,6 @@ 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 | 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]) {
-- 
cgit