Merge remote-tracking branch 'origin/master'

6 files changed, 131 insertions, 81 deletions

diff --git a/.gitattributes b/.gitattributes
index 30dd12d..8c19733 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1,4 +1,4 @@
 *.h linguist-language=C
 *.c linguist-language=C
 *.v linguist-language=Coq
-benchmarks/* linguist-vendored
+benchmarks/** linguist-vendored
diff --git a/CITATION.cff b/CITATION.cff
new file mode 100644
index 0000000..9328474
--- /dev/null
+++ b/CITATION.cff
@@ -0,0 +1,46 @@
+# -*- mode: yaml -*-
+cff-version: 1.2.0
+message: "If you use this software, please cite it as below."
+authors:
+- family-names: "Herklotz"
+  given-names: "Yann"
+  orcid: "https://orcid.org/0000-0002-2329-1029"
+- family-names: "Pollard"
+  given-names: "James D."
+  orcid: "https://orcid.org/0000-0003-1404-1527"
+- family-names: "Ramanathan"
+  given-names: "Nadesh"
+  orcid: "https://orcid.org/0000-0001-9083-8349"
+- family-names: "Wickerson"
+  given-names: "John"
+  orcid: "https://orcid.org/0000-0001-6735-5533"
+title: "Vericert"
+version: 1.2.1
+doi: 10.5281/zenodo.5093839
+date-released: 2021-07-12
+url: "https://github.com/ymherklotz/vericert"
+preferred-citation:
+  type: article
+  authors:
+  - family-names: "Herklotz"
+    given-names: "Yann"
+    orcid: "https://orcid.org/0000-0002-2329-1029"
+  - family-names: "Pollard"
+    given-names: "James D."
+    orcid: "https://orcid.org/0000-0003-1404-1527"
+  - family-names: "Ramanathan"
+    given-names: "Nadesh"
+    orcid: "https://orcid.org/0000-0001-9083-8349"
+  - family-names: "Wickerson"
+    given-names: "John"
+    orcid: "https://orcid.org/0000-0001-6735-5533"
+  doi: "10.1145/3485494"
+  journal: "Proc. ACM Program. Lang."
+  month: 11
+  pages: 30
+  title: "Formal Verification of High-Level Synthesis"
+  volume: 5
+  year: 2021
+  number: OOPSLA
+  publisher: Association for Computing Machinery
+  address: New York, NY, USA
diff --git a/LICENSE b/LICENSE
index edd3e1e..b386211 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,13 +1,3 @@
-Everything under src/ is licensed under the GPLv3 shown below, except for the
-following files:
-
-src/SoftwarePipeline/*: MIT
-
-    Copyright (c) 2008-2010 Jean-Baptiste Tristan and INRIA
-    Copyright (c) 2020-2021 Yann Herklotz
-
---------------------------------------------------------------------------------
-
                     GNU GENERAL PUBLIC LICENSE
                        Version 3, 29 June 2007
 
@@ -682,25 +672,3 @@ may consider it more useful to permit linking proprietary applications with
 the library.  If this is what you want to do, use the GNU Lesser General
 Public License instead of this License.  But first, please read
 <https://www.gnu.org/licenses/why-not-lgpl.html>.
-
---------------------------------------------------------------------------------
-
-Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA
-
-Permission is hereby granted, free of charge, to any person obtaining a copy
-of this software and associated documentation files (the "Software"), to deal
-in the Software without restriction, including without limitation the rights
-to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in
-all copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-SOFTWARE.
diff --git a/README.org b/README.org
index c2382f1..4426561 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,50 @@ 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 way, 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},
+  doi = {10.1145/3485494}
+}
+#+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
diff --git a/docs b/docs
-Subproject f85153b7335ebf99ab6bf6e696b5a08fef38b61
+Subproject 3b2ce146bc6e651df8ac9910d08da05d88c06fb
diff --git a/src/SoftwarePipelining/LICENSE b/src/SoftwarePipelining/LICENSE
new file mode 100644
index 0000000..e275fa0
--- /dev/null
+++ b/src/SoftwarePipelining/LICENSE
@@ -0,0 +1,19 @@
+Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.