Add more documentation

4 files changed, 45 insertions, 8 deletions

diff --git a/docs/documentation.org b/docs/documentation.org
index 09c3ffe..3891fac 100644
--- a/docs/documentation.org
+++ b/docs/documentation.org
@@ -1,7 +1,19 @@
-#+SETUPFILE: publish.setup
-#+TITLE: Vericert Documentation
+#+setupfile: publish.setup
+#+title: Vericert Documentation
+#+author: Yann Herklotz
 
-* Building
+* 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.
 
@@ -59,7 +71,7 @@ make install
 
 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~.
 
-** Running
+** Testing
 
 To test out ~vericert~ you can try the following examples which are in the test folder using the following:
 
@@ -68,3 +80,13 @@ To test out ~vericert~ you can try the following examples which are in the test
 ./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/images/design.jpg b/docs/images/design.jpg
new file mode 100644
index 0000000..d254e1a
--- /dev/null
+++ b/docs/images/design.jpg
diff --git a/docs/index.org b/docs/index.org
index 7a92650..455a23a 100644
--- a/docs/index.org
+++ b/docs/index.org
@@ -1,5 +1,5 @@
-#+SETUPFILE: publish.setup
-#+TITLE: Vericert
+#+setupfile: publish.setup
+#+title: Vericert
 
 A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [[https://github.com/AbsInt/CompCert][CompCert]].  This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert's C semantics, removing the need to check the resulting hardware for behavioural correctness.
 
diff --git a/docs/publish.setup b/docs/publish.setup
index a3e7255..f3e7611 100644
--- a/docs/publish.setup
+++ b/docs/publish.setup
@@ -1,2 +1,17 @@
-#+MACRO: begin-summary #+HTML: <div class="summary"><h2>Summary</h2>
-#+MACRO: end-summary #+HTML: </div>
+# -*- mode: org -*-
+#+macro: begin-summary #+HTML: <div class="summary"><h2>Summary</h2>
+#+macro: end-summary #+HTML: </div>
+
+#+latex_class: scrartcl
+#+latex_header: \usepackage{ifluatex}
+#+latex_header: \usepackage{ifxetex}
+#+latex_header: \usepackage{libertine}
+#+latex_header: \ifluatex%
+#+latex_header: \usepackage{fontspec}\setmonofont[Scale=0.9]{Iosevka}
+#+latex_header: \else\ifxetex%
+#+latex_header: \usepackage{fontspec}\setmonofont[Scale=0.9]{Iosevka}
+#+latex_header: \else
+#+latex_header: \usepackage{inconsolata}
+#+latex_header: \fi
+#+latex_header: \fi
+#+latex_header: \usepackage[a4paper,margin=1in]{geometry}