From 80568aaef48fab6aff08d0cc724909e5afeee5dd Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Sun, 19 Sep 2021 23:17:53 +0000 Subject: deploy: 5508c21e064276aa4d5146b3af5b6f6e9a4c2364 --- blog/index.html | 2 +- categories/index.html | 2 +- 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 +- future/index.html | 2 +- index.html | 2 +- tags/index.html | 2 +- 10 files changed, 11 insertions(+), 11 deletions(-) diff --git a/blog/index.html b/blog/index.html index d91aded..227a91d 100644 --- a/blog/index.html +++ b/blog/index.html @@ -1,4 +1,4 @@ Blog | Vericert -
+
Blog
\ No newline at end of file diff --git a/categories/index.html b/categories/index.html index cd0aa90..eb6e6bf 100644 --- a/categories/index.html +++ b/categories/index.html @@ -1,4 +1,4 @@ Categories | Vericert -
+
Categories
\ No newline at end of file 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]) {
diff --git a/future/index.html b/future/index.html
index 0ade3aa..562ef22 100644
--- a/future/index.html
+++ b/future/index.html
@@ -3,7 +3,7 @@ The next interesting optimisations that should be looked at are the following:
  globals, type support, memory partitioning, and loop pipelining.  Globals #  Globals are an important feature to add, as have to be handled carefully in HLS, because they have to be placed into memory, and are often used in HLS designs.">Future Work | Vericert
-

+

 Future Work
 
Future Work
This section contains future work that should be added to Vericert to make it into a better
 high-level synthesis tool.
The next interesting optimisations that should be looked at are the following:
Globals
diff --git a/index.html b/index.html
index f46a016..7244326 100644
--- a/index.html
+++ b/index.html
@@ -1,6 +1,6 @@
 Vericert | Vericert
-

+

 Vericert
 
A formally verified high-level synthesis (HLS) tool written in Coq, building on top of CompCert.
 This ensures the correctness of the C to Verilog translation according to our Verilog semantics and
diff --git a/tags/index.html b/tags/index.html
index 306bdd2..4cf6fa7 100644
--- a/tags/index.html
+++ b/tags/index.html
@@ -1,4 +1,4 @@
 Tags | Vericert
-

+

 Tags
 

\ No newline at end of file
-- 
cgit