From 80568aaef48fab6aff08d0cc724909e5afeee5dd Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Sun, 19 Sep 2021 23:17:53 +0000 Subject: deploy: 5508c21e064276aa4d5146b3af5b6f6e9a4c2364 --- 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 a23c337..60a9d58 100644 --- a/docs/building/index.html +++ b/docs/building/index.html @@ -3,7 +3,7 @@ The project is written in Coq, a theorem prover, which is extracted to OCaml so 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 project, which can be pulled in automatically with nix using the provided default.nix and shell.nix diff --git a/docs/coq-style-guide/index.html b/docs/coq-style-guide/index.html index cbcda1e..0b5ab17 100644 --- a/docs/coq-style-guide/index.html +++ b/docs/coq-style-guide/index.html @@ -1,7 +1,7 @@ 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 repository. There are certainly other valid strategies and opinions on Coq code style; this is laid diff --git a/docs/index.html b/docs/index.html index 5e7f5a5..6b5a5be 100644 --- a/docs/index.html +++ b/docs/index.html @@ -2,9 +2,9 @@ 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.">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 50abfc8..4edd082 100644 --- a/docs/unreleased/index.html +++ b/docs/unreleased/index.html @@ -1,7 +1,7 @@ Unreleased Features | Vericert -
+
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 diff --git a/docs/using-vericert/index.html b/docs/using-vericert/index.html index b42f92b..481a784 100644 --- a/docs/using-vericert/index.html +++ b/docs/using-vericert/index.html @@ -1,7 +1,7 @@ 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 following C file (main.c):

void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) {
-- 
cgit