From e0894caeb8b3c2cc841bade7e26581f6b206246f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 15 Sep 2021 15:54:09 +0100 Subject: Move license to the SoftwarePipelining directory --- LICENSE | 32 -------------------------------- src/SoftwarePipelining/LICENSE | 19 +++++++++++++++++++ 2 files changed, 19 insertions(+), 32 deletions(-) create mode 100644 src/SoftwarePipelining/LICENSE 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 . - --------------------------------------------------------------------------------- - -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/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. -- cgit From 26608d2d1798795844d8c140e37d75b26467e374 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 15 Sep 2021 16:00:58 +0100 Subject: Add more information about paper to README --- README.org | 112 +++++++++++++++++++++++++++++++++++-------------------------- 1 file 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:

 

-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 -- cgit From 0a00e01db267619c68ca223de2ba6b160163e6b6 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 15 Sep 2021 16:05:31 +0100 Subject: Fix linguist-vendored for repository statistics --- .gitattributes | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit From 4a02e02194f5d8f3aa83f69757b801a66939b839 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 15 Sep 2021 16:14:48 +0100 Subject: Add CITATION.cff --- CITATION.cff | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 CITATION.cff diff --git a/CITATION.cff b/CITATION.cff new file mode 100644 index 0000000..34911af --- /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.0000/00000" + journal: "Proc. ACM Program. Lang." + month: 11 + numpages: 30 + title: "Formal Verification of High-Level Synthesis" + volume: 5 + year: 2021 + number: OOPSLA + publisher: Association for Computing Machinery + address: New York, NY, USA -- cgit From 4def81ab50d8239320e7c8c71c80844050fb1111 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 15 Sep 2021 16:16:55 +0100 Subject: Add DOI to article --- CITATION.cff | 2 +- README.org | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/CITATION.cff b/CITATION.cff index 34911af..06d3364 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -34,7 +34,7 @@ preferred-citation: - family-names: "Wickerson" given-names: "John" orcid: "https://orcid.org/0000-0001-6735-5533" - doi: "10.0000/00000" + doi: "10.1145/3485494" journal: "Proc. ACM Program. Lang." month: 11 numpages: 30 diff --git a/README.org b/README.org index 26f94ee..02eb8c8 100644 --- a/README.org +++ b/README.org @@ -124,6 +124,7 @@ If you use Vericert in any ways, please cite it using our [[https://yannherklotz volume = {5}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, + doi = {10.1145/3485494} } #+end_src -- cgit From ac3682113bde3dc6fc496c2dc566a019b942af53 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 15 Sep 2021 16:22:31 +0100 Subject: Fix a typo in README.org --- README.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.org b/README.org index 02eb8c8..b199da5 100644 --- a/README.org +++ b/README.org @@ -110,7 +110,7 @@ following: ** Citation -If you use Vericert in any ways, please cite it using our [[https://yannherklotz.com/papers/fvhls_oopsla21.pdf][OOPSLA'21 paper]]: +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, -- cgit From 5e4c1c52cf8ab7fe6b8de4f06e8d4b5b518eed82 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 15 Sep 2021 16:31:01 +0100 Subject: Add number of pages correctly --- CITATION.cff | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CITATION.cff b/CITATION.cff index 06d3364..9328474 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -37,7 +37,7 @@ preferred-citation: doi: "10.1145/3485494" journal: "Proc. ACM Program. Lang." month: 11 - numpages: 30 + pages: 30 title: "Formal Verification of High-Level Synthesis" volume: 5 year: 2021 -- cgit From 67601d747e71e4fa1c8d0f9013593fef3f321426 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 16 Sep 2021 18:06:00 +0100 Subject: Update docs --- README.org | 4 ++-- docs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/README.org b/README.org index b199da5..4426561 100644 --- a/README.org +++ b/README.org @@ -130,11 +130,11 @@ If you use Vericert in any way, please cite it using our [[https://yannherklotz. ** 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~]]. +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 +- [[/src/SoftwarePipelining][/src/SoftwarePipelining]] :: MIT #+begin_src text Copyright (c) 2008,2009,2010 Jean-Baptiste Tristan and INRIA diff --git a/docs b/docs index f85153b..3b2ce14 160000 --- a/docs +++ b/docs @@ -1 +1 @@ -Subproject commit f85153b7335ebf99ab6bf6e696b5a08fef38b61b +Subproject commit 3b2ce146bc6e651df8ac9910d08da05d88c06fb6 -- cgit