From 6a892863d6e88fb4ce889007f98f2acb1a27c381 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 15 Jan 2021 21:34:41 +0000 Subject: Update website --- docs/docs/index.org | 92 ++++++++++++++++++++++++++++++++++++++++++++++++++ docs/documentation.org | 92 -------------------------------------------------- docs/index.org | 2 +- docs/proof/index.org | 3 ++ docs/proof/toc.org | 3 -- docs/publish.el | 6 ++-- 6 files changed, 99 insertions(+), 99 deletions(-) create mode 100644 docs/docs/index.org delete mode 100644 docs/documentation.org create mode 100644 docs/proof/index.org delete mode 100644 docs/proof/toc.org diff --git a/docs/docs/index.org b/docs/docs/index.org new file mode 100644 index 0000000..061d841 --- /dev/null +++ b/docs/docs/index.org @@ -0,0 +1,92 @@ +#+setupfile: publish.setup +#+title: Vericert Documentation +#+author: Yann Herklotz + +* Overview + +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). + +#+attr_html: :width 600 +#+caption: 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. +#+name: fig:design +[[../images/design.jpg]] + +The design shown in Figure [[fig:design]] shows how Vericert leverages an existing verified C compiler called [[https://compcert.org/compcert-C.html][CompCert]] to perform this translation. + +* 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 [[https://nixos.org/nix/][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: + +- [[https://coq.inria.fr/][Coq]]: theorem prover that is used to also program the HLS tool. +- [[https://ocaml.org/][OCaml]]: the OCaml compiler to compile the extracted files. +- [[https://github.com/mit-plv/bbv][bbv]]: an efficient bit vector library. +- [[https://github.com/ocaml/dune][dune]]: build tool for ocaml projects to gather all the ocaml files and compile them in the right order. +- [[http://gallium.inria.fr/~fpottier/menhir/][menhir]]: parser generator for ocaml. +- [[https://github.com/ocaml/ocamlfind][findlib]] to find installed OCaml libraries. +- [[https://gcc.gnu.org/][GCC]]: compiler to help build CompCert. + +These dependencies can be installed manually, or automatically through Nix. + +** Downloading CompCert + +CompCert is added as a submodule in the ~lib/CompCert~ directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run: + +#+begin_src shell +git clone --recursive https://github.com/ymherklotz/vericert +#+end_src + +If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded: + +#+begin_src shell +git submodule update --init +#+end_src + +** Setting up Nix + +Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way. + +To open a shell which includes all the necessary dependencies, one can use: + +#+begin_src shell +nix-shell +#+end_src + +which will open a shell that has all the dependencies loaded. + +** Makefile build + +If the dependencies were installed manually, or if one is in the ~nix-shell~, the project can be built by running: + +#+begin_src shell +make -j8 +#+end_src + +and installed locally, or under the ~PREFIX~ location using: + +#+begin_src shell +make install +#+end_src + +Which will install the binary in ~./bin/vericert~ by default. However, this can be changed by changing the ~PREFIX~ environment variable, in which case the binary will be installed in ~$PREFIX/bin/vericert~. + +** Testing + +To test out ~vericert~ you can try the following examples which are in the test folder using the following: + +#+begin_src shell +./bin/vericert test/loop.c -o loop.v +./bin/vericert test/conditional.c -o conditional.v +./bin/vericert test/add.c -o add.v +#+end_src + +Or by running the test suite using the following command: + +#+begin_src shell +make test +#+end_src + +* Using Vericert + +Vericert can be used to translate a subset of C into Verilog. diff --git a/docs/documentation.org b/docs/documentation.org deleted file mode 100644 index 3891fac..0000000 --- a/docs/documentation.org +++ /dev/null @@ -1,92 +0,0 @@ -#+setupfile: publish.setup -#+title: Vericert Documentation -#+author: Yann Herklotz - -* Overview - -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). - -#+attr_html: :width 600 -#+caption: 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. -#+name: fig:design -[[./images/design.jpg]] - -The design shown in Figure [[fig:design]] shows how Vericert leverages an existing verified C compiler called [[https://compcert.org/compcert-C.html][CompCert]] to perform this translation. - -* 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 [[https://nixos.org/nix/][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: - -- [[https://coq.inria.fr/][Coq]]: theorem prover that is used to also program the HLS tool. -- [[https://ocaml.org/][OCaml]]: the OCaml compiler to compile the extracted files. -- [[https://github.com/mit-plv/bbv][bbv]]: an efficient bit vector library. -- [[https://github.com/ocaml/dune][dune]]: build tool for ocaml projects to gather all the ocaml files and compile them in the right order. -- [[http://gallium.inria.fr/~fpottier/menhir/][menhir]]: parser generator for ocaml. -- [[https://github.com/ocaml/ocamlfind][findlib]] to find installed OCaml libraries. -- [[https://gcc.gnu.org/][GCC]]: compiler to help build CompCert. - -These dependencies can be installed manually, or automatically through Nix. - -** Downloading CompCert - -CompCert is added as a submodule in the ~lib/CompCert~ directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run: - -#+begin_src shell -git clone --recursive https://github.com/ymherklotz/vericert -#+end_src - -If the repository is already cloned, you can run the following command to make sure that CompCert is also downloaded: - -#+begin_src shell -git submodule update --init -#+end_src - -** Setting up Nix - -Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way. - -To open a shell which includes all the necessary dependencies, one can use: - -#+begin_src shell -nix-shell -#+end_src - -which will open a shell that has all the dependencies loaded. - -** Makefile build - -If the dependencies were installed manually, or if one is in the ~nix-shell~, the project can be built by running: - -#+begin_src shell -make -j8 -#+end_src - -and installed locally, or under the ~PREFIX~ location using: - -#+begin_src shell -make install -#+end_src - -Which will install the binary in ~./bin/vericert~ by default. However, this can be changed by changing the ~PREFIX~ environment variable, in which case the binary will be installed in ~$PREFIX/bin/vericert~. - -** Testing - -To test out ~vericert~ you can try the following examples which are in the test folder using the following: - -#+begin_src shell -./bin/vericert test/loop.c -o loop.v -./bin/vericert test/conditional.c -o conditional.v -./bin/vericert test/add.c -o add.v -#+end_src - -Or by running the test suite using the following command: - -#+begin_src shell -make test -#+end_src - -* Using Vericert - -Vericert can be used to translate a subset of C into Verilog. diff --git a/docs/index.org b/docs/index.org index 455a23a..4948d65 100644 --- a/docs/index.org +++ b/docs/index.org @@ -14,5 +14,5 @@ The project is currently a work in progress, so proofs remain to be finished. C * Content -- [[./proof/toc.html][Vericert Proof]] +- [[./proof/index.org][Vericert Proof]] - [[./documentation.org][Vericert Documentation]] diff --git a/docs/proof/index.org b/docs/proof/index.org new file mode 100644 index 0000000..1b5f074 --- /dev/null +++ b/docs/proof/index.org @@ -0,0 +1,3 @@ +#+title: Vericert Proof + +- [[./Compiler.html][Compiler]] diff --git a/docs/proof/toc.org b/docs/proof/toc.org deleted file mode 100644 index 9d4bcdb..0000000 --- a/docs/proof/toc.org +++ /dev/null @@ -1,3 +0,0 @@ -#+title: Table of Contents - -- [[./Compiler.html][Compiler]] diff --git a/docs/publish.el b/docs/publish.el index 930023c..0d6d2da 100644 --- a/docs/publish.el +++ b/docs/publish.el @@ -16,14 +16,14 @@ (defvar vericert/site-attachments nil) (defvar vericert/base "") -(setq vericert/base "/vericert") +(setq vericert/base "") (setq vericert/header (concat "

Vericert is the first formally verified high-level synthesis tool.

-- cgit