From 9a0b1f5ed471e2752480d91f5fc6a433dac714dc Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Sun, 19 Sep 2021 17:08:57 +0000 Subject: deploy: 54b98a4da47ac332827f9f8186256881575b3d76 --- docs/building/index.html | 2 +- docs/coq-style-guide/index.html | 2 +- docs/index.html | 4 ++-- docs/unreleased/index.html | 2 +- docs/using-vericert/index.html | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) (limited to 'docs') diff --git a/docs/building/index.html b/docs/building/index.html index cd26e32..a23c337 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

Building Vericert

To build Vericert, the provided Makefile can be used. External dependencies are needed to build the diff --git a/docs/coq-style-guide/index.html b/docs/coq-style-guide/index.html index 429b45c..cbcda1e 100644 --- a/docs/coq-style-guide/index.html +++ b/docs/coq-style-guide/index.html @@ -1,6 +1,6 @@ Coq Style Guide | Vericert +Code organization # Legal banner # Files should begin with a copyright/license banner, as shown in the example above.">Coq Style Guide | Vericert

Coq Style Guide

Coq Style Guide

This style guide was taken from Silveroak, it outlines code style for Coq code in this diff --git a/docs/index.html b/docs/index.html index dd0409f..5e7f5a5 100644 --- a/docs/index.html +++ b/docs/index.html @@ -1,10 +1,10 @@ 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 +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/unreleased/index.html b/docs/unreleased/index.html index 71db939..50abfc8 100644 --- a/docs/unreleased/index.html +++ b/docs/unreleased/index.html @@ -1,6 +1,6 @@ Unreleased Features | Vericert + scheduling, operation chaining, if-conversion, 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.">Unreleased Features | Vericert
Unreleased Features

Unreleased Features

The following are unreleased features in Vericert that are currently being worked on and have not diff --git a/docs/using-vericert/index.html b/docs/using-vericert/index.html index c752c7f..b42f92b 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

Using Vericert

Vericert can be used to translate a subset of C into Verilog. As a simple example, consider the -- cgit