Add more information about paper to README

1 files changed, 64 insertions, 48 deletions

diff --git a/README.org b/README.org
index c2382f1..26f94ee 100644
--- a/README.org
+++ b/README.org
@@ -2,19 +2,17 @@
 
 #+html: <p align=center><a href="https://github.com/ymherklotz/vericert/actions"><img src="https://github.com/ymherklotz/vericert/workflows/CI/badge.svg" /></a>&nbsp;<a href="https://vericert.ymhg.org/"><img src="https://github.com/ymherklotz/vericert-docs/workflows/docs/badge.svg" /></a></p>
 
-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.
+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.
 
 ** Features
    :PROPERTIES:
    :CUSTOM_ID: features
    :END:
-The project is currently a work in progress, so proofs remain to be
-finished. Currently, the following C features are supported, but are not
-all proven correct yet:
+The project is currently a work in progress, so proofs remain to be finished. Currently, the
+following C features are supported, but are not all proven correct yet:
 
 - all int operations,
 - non-recursive function calls,
@@ -25,48 +23,38 @@ all proven correct yet:
    :PROPERTIES:
    :CUSTOM_ID: building
    :END:
-To build Vericert, the provided [[/Makefile][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][default.nix]] and [[/shell.nix][shell.nix]]
+To build Vericert, the provided [[/Makefile][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][default.nix]] and [[/shell.nix][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.
+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.
+These dependencies can be installed manually, or automatically through Nix.
 
 *** Downloading CompCert
     :PROPERTIES:
     :CUSTOM_ID: downloading-compcert
     :END:
-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:
+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:
+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
@@ -76,12 +64,10 @@ to make sure that CompCert is also downloaded:
     :PROPERTIES:
     :CUSTOM_ID: setting-up-nix
     :END:
-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.
+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:
+To open a shell which includes all the necessary dependencies, one can use:
 
 #+begin_src shell
   nix-shell
@@ -93,8 +79,8 @@ which will open a shell that has all the dependencies loaded.
     :PROPERTIES:
     :CUSTOM_ID: makefile-build
     :END:
-If the dependencies were installed manually, or if one is in the
-=nix-shell=, the project can be built by running:
+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
@@ -106,19 +92,49 @@ and installed locally, or under the =PREFIX= location using:
   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=.
+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
    :PROPERTIES:
    :CUSTOM_ID: running
    :END:
-To test out =vericert= you can try the following examples which are in
-the test folder using the following:
+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
+
+** Citation
+
+If you use Vericert in any ways, please cite it using our [[https://yannherklotz.com/papers/fvhls_oopsla21.pdf][OOPSLA'21 paper]]:
+
+#+begin_src bibtex
+@inproceedings{herklotz21_fvhls,
+  author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John},
+  title = {Formal Verification of High-Level Synthesis},
+  year = {2021},
+  number = {OOPSLA},
+  numpages = {30},
+  month = {11},
+  journal = {Proc. ACM Program. Lang.},
+  volume = {5},
+  publisher = {Association for Computing Machinery},
+  address = {New York, NY, USA},
+}
+#+end_src
+
+** License
+
+This project is licensed under [[https://www.gnu.org/licenses/gpl-3.0.en.html][GPLv3]].  The license can be seen in [[/LICENSE][~/LICENSE~]].
+
+The following external code and its license is present in this repository:
+
+- [[/src/SoftwarePipelining][~/src/SoftwarePipelining~]] :: MIT
+
+#+begin_src text
+Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA
+#+end_src