From bb9ad00fce55d539a2cb7664ced14b78a3c681fb Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Wed, 22 Sep 2021 22:00:08 +0000 Subject: deploy: bf845f5601bef0b7b1bafa5db39a4a116a6a8d3b --- 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 60a9d58..3277755 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 0b5ab17..5b33d81 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 03748e7..2a9f2ce 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 4edd082..870b18c 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 481a784..8b3191b 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