diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-09-22 19:26:01 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-22 19:26:01 +0100 |
| commit | 2ff1316847b9d338a792f67b7b9f6364d4b65551 (patch) | |
| tree | 6aaf069a05f889d6f3fe012332a5e74dd8707429 | |
| parent | c114bd7a269824623f2dbb41322d95d5056fca02 (diff) | |
| parent | 8386bed39f413bb461c19debbad92e85f927c4b5 (diff) | |
| download | vericert-kvx-2ff1316847b9d338a792f67b7b9f6364d4b65551.tar.gz vericert-kvx-2ff1316847b9d338a792f67b7b9f6364d4b65551.zip | |
Merge remote-tracking branch 'origin/develop' into develop
90 files changed, 4575 insertions, 1650 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/CHANGELOG.org b/CHANGELOG.org index 52db994..af5e771 100644 --- a/CHANGELOG.org +++ b/CHANGELOG.org @@ -1,46 +1,56 @@ # -*- fill-column: 80 -*- +#+title: Vericert Changelog +#+author: Yann Herklotz +#+email: git@ymhg.org -* Vericert Changelog +* Unreleased -** Unreleased - -*** New Features +** New Features - Add *RTLBlock*, a basic block intermediate language that is based on CompCert's RTL. - Add *RTLPar*, which can execute groups of instructions in parallel. - Add scheduling pass to go from RTLBlock to RTLPar. -** v1.2.0 - 2021-04-07 +* 2021-07-12 - v1.2.1 + +Main release for OOPSLA'21 paper. + +- Add better documentation on how to run Vericert. +- Add =Dockerfile= with instructions on how to get figures of the paper. + +* 2021-04-07 - v1.2.0 + +** New Features -- Proper RAM inference support. +- Add memory inference capabilities in generated hardware. -** v1.1.0 - 2020-12-17 +* 2020-12-17 - v1.1.0 Add a stable release with all proofs completed. -** v1.0.1 - 2020-08-14 +* 2020-08-14 - v1.0.1 Release a new minor version fixing all proofs and fixing scripts to generate the badges. -*** Bug Fixes +** Fixes - Fix some of the proofs which were not passing. -** v1.0.0 - 2020-08-13 +* 2020-08-13 - v1.0.0 First release of a fully verified version of Vericert with support for the translation of many C constructs to Verilog. -*** New Features +** New Features - Most int instructions and operators. - Non-recursive function calls. - Local arrays, structs and unions of type int. - Pointer arithmetic with int. -** v0.1.0 - 2020-04-03 +* 2020-04-03 - v0.1.0 This is the first release with working HLS but without any proofs associated with it. 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 @@ -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. @@ -31,8 +31,10 @@ all: lib/COMPCERTSTAMP $(MAKE) proof $(MAKE) compile -lib/COMPCERTSTAMP: +lib/CompCert/Makefile.config: lib/CompCert/configure (cd lib/CompCert && ./configure --ignore-coq-version $(ARCH)) + +lib/COMPCERTSTAMP: lib/CompCert/Makefile.config $(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/CompCert touch $@ @@ -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> <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/benchmarks/README.md b/benchmarks/README.md index 59edf78..c10f357 100644 --- a/benchmarks/README.md +++ b/benchmarks/README.md @@ -1,14 +1,11 @@ -Hi, +# Benchmarks -I have collected a set of benchmarks that you may be interested in. The main idea is to run the existing HLS benchmarks to see if they work - they can only test correctness for a single set of input by a customised test bench. +The main idea is to run the existing HLS benchmarks to see if they work - they can only test correctness for a single set of input by a customised test bench. -* jacob_2d: a benchmark from Polybench -* sobel: a benchmark from LegUp HLS -* getTanh: a benchmark from DASS -* fft: a benchmark from MachSuite -* KMeans: a benchmark from Felix's work +- jacob_2d: a benchmark from Polybench +- sobel: a benchmark from LegUp HLS +- getTanh: a benchmark from DASS +- fft: a benchmark from MachSuite +- KMeans: a benchmark from Felix's work -Note all the benchmark set above (links included in the source code) should be all synthesisable in your case, so you may be show coverage instead of a single benchmark. - -Best, -Jianyi +Note all the benchmark set above (links included in the source code) should be all synthesisable, so you may be able to show coverage instead of a single benchmark. diff --git a/benchmarks/polybench-syn-div/Makefile b/benchmarks/polybench-syn-div/Makefile new file mode 100644 index 0000000..2c20246 --- /dev/null +++ b/benchmarks/polybench-syn-div/Makefile @@ -0,0 +1,15 @@ +all: + $(MAKE) -C stencils + $(MAKE) -C medley + $(MAKE) -C linear-algebra/blas + $(MAKE) -C linear-algebra/kernels + $(MAKE) -C linear-algebra/solvers + $(MAKE) -C data-mining + +clean: + $(MAKE) clean -C stencils + $(MAKE) clean -C medley + $(MAKE) clean -C linear-algebra/blas + $(MAKE) clean -C linear-algebra/kernels + $(MAKE) clean -C linear-algebra/solvers + $(MAKE) clean -C data-mining diff --git a/benchmarks/polybench-syn-div/benchmark-list-master b/benchmarks/polybench-syn-div/benchmark-list-master new file mode 100644 index 0000000..ef0d0d0 --- /dev/null +++ b/benchmarks/polybench-syn-div/benchmark-list-master @@ -0,0 +1,27 @@ +stencils/adi +stencils/heat-3d +stencils/fdtd-2d +stencils/jacobi-1d +stencils/seidel-2d +stencils/jacobi-2d +medley/nussinov +medley/floyd-warshall +linear-algebra/kernels/3mm +linear-algebra/kernels/2mm +linear-algebra/kernels/doitgen +linear-algebra/kernels/bicg +linear-algebra/kernels/mvt +linear-algebra/kernels/atas +linear-algebra/blas/syrk +linear-algebra/blas/gemver +linear-algebra/blas/symm +linear-algebra/blas/gesummv +linear-algebra/blas/gemm +linear-algebra/blas/trmm +linear-algebra/blas/syr2k +linear-algebra/solvers/cholesky +linear-algebra/solvers/trisolv +linear-algebra/solvers/lu +linear-algebra/solvers/ludcmp +linear-algebra/solvers/durbin +data-mining/covariance diff --git a/benchmarks/polybench-syn-div/common.mk b/benchmarks/polybench-syn-div/common.mk new file mode 100644 index 0000000..fbada0b --- /dev/null +++ b/benchmarks/polybench-syn-div/common.mk @@ -0,0 +1,33 @@ +VERICERT ?= vericert +VERICERT_OPTS ?= -DSYNTHESIS + +IVERILOG ?= iverilog +IVERILOG_OPTS ?= + +TARGETS ?= + +%.v: %.c + $(VERICERT) $(VERICERT_OPTS) $< -o $@ + +%.iver: %.v + $(IVERILOG) -o $@ $(IVERILOG_OPTS) $< + +%.gcc: %.c + $(CC) $(CFLAGS) $< -o $@ + +%: %.iver %.gcc + cp $< $@ + +all: $(TARGETS) + +clean: + rm -f *.iver + rm -f *.v + rm -f *.gcc + rm -f *.clog + rm -f *.tmp + rm -f $(TARGETS) + +.PRECIOUS: %.v %.gcc %.iver +.PHONY: all clean +.SUFFIXES: diff --git a/benchmarks/polybench-syn-div/data-mining/Makefile b/benchmarks/polybench-syn-div/data-mining/Makefile new file mode 100644 index 0000000..d4817a0 --- /dev/null +++ b/benchmarks/polybench-syn-div/data-mining/Makefile @@ -0,0 +1,3 @@ +TARGETS := covariance + +include ../common.mk diff --git a/benchmarks/polybench-syn-div/data-mining/covariance.c b/benchmarks/polybench-syn-div/data-mining/covariance.c new file mode 100644 index 0000000..88de67e --- /dev/null +++ b/benchmarks/polybench-syn-div/data-mining/covariance.c @@ -0,0 +1,113 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* covariance.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + + +#define plus(i) i = i + ONE +static +void init_array (int m, int n, + int *float_n, + int data[ 32 + 0][28 + 0]) +{ + int i, j; + int ONE = 1; + + *float_n = (int)n; + + for (i = 0; i < 32; plus(i)) + for (j = 0; j < 28; plus(j)) + data[i][j] = ((int) i*j) / (27+ONE); +} + + + + +static +int print_array(int m, + int cov[ 28 + 0][28 + 0]) + +{ + int i, j; + int ONE = 1; + int res = 0; + for (i = 0; i < m; plus(i)) + for (j = 0; j < m; plus(j)) { + res ^= cov[i][j]; + } +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif + return res; +} + + + + +static +void kernel_covariance(int m, int n, + int float_n, + int data[ 32 + 0][28 + 0], + int cov[ 28 + 0][28 + 0], + int mean[ 28 + 0]) +{ + int i, j, k; + int ONE = 1; + + for (j = 0; j < m; plus(j)) + { + mean[j] = 0; + for (i = 0; i < n; plus(i)) + mean[j] += data[i][j]; + mean[j] = mean[j] / float_n; + } + + for (i = 0; i < n; plus(i)) + for (j = 0; j < m; plus(j)) + data[i][j] -= mean[j]; + + for (i = 0; i < m; plus(i)) + for (j = i; j < m; plus(j)) + { + cov[i][j] = 0; + for (k = 0; k < n; plus(k)) + cov[i][j] += data[k][i] * data[k][j]; + cov[i][j] = cov[i][j] / (float_n - ONE); + cov[j][i] = cov[i][j]; + } + +} + + +int main() +{ + + int n = 32; + int m = 28; + + + int float_n; + int data[32 + 0][28 + 0]; + int mean[28 + 0]; + int cov[28 + 0][28 + 0]; + + init_array (m, n, &float_n, data); + + kernel_covariance (m, n, float_n, + data, + cov, + mean); + + return print_array(m, cov); + +} diff --git a/benchmarks/polybench-syn-div/exec.csv b/benchmarks/polybench-syn-div/exec.csv new file mode 100644 index 0000000..e28109b --- /dev/null +++ b/benchmarks/polybench-syn-div/exec.csv @@ -0,0 +1,27 @@ +adi,1422354 +heat-3d,580770 +fdtd-2d,901430 +jacobi-1d,19622 +seidel-2d,664780 +jacobi-2d,344072 +nussinov,954402 +floyd-warshall,5373798 +3mm,536114 +2mm,404478 +doitgen,351988 +bicg,53916 +mvt,70204 +atas,58424 +syrk,271816 +gemver,117394 +symm,240172 +gesummv,37700 +gemm,328104 +trmm,144688 +syr2k,436520 +cholesky,2535686 +trisolv,25192 +lu,2853646 +ludcmp,2601382 +durbin,22974 +covariance,288392 diff --git a/benchmarks/polybench-syn-div/include/misc.h b/benchmarks/polybench-syn-div/include/misc.h new file mode 100644 index 0000000..664677c --- /dev/null +++ b/benchmarks/polybench-syn-div/include/misc.h @@ -0,0 +1,105 @@ +unsigned int modulo(unsigned int x, unsigned int y) +{ + unsigned int r0, q0, y0, y1; + + r0 = x; + q0 = 0; + y0 = y; + y1 = y; + do + { + y1 = 2 * y1; + } + while (y1 <= x); + do + { + y1 = y1 / 2; + q0 = 2 * q0; + if (r0 >= y1) + { + r0 = r0 - y1; + q0 = q0 + 1; + } + } + while ((int)y1 != (int)y0); + return r0; +} + +int smodulo(int N, int D) { + if (D < 0) { + if (N < 0) + return modulo(-N, -D); + else + return -modulo(N, -D); + } else { + if (N < 0) + return -modulo(-N, D); + else + return modulo(N, D); + } +} + +unsigned divider_fast(unsigned x, unsigned y) { + unsigned r0, q0, y0, y1; + + r0 = x; + q0 = 0; + y0 = y; + y1 = y; + do { + y1 = 2 * y1; + } while (y1 <= x); + do { + y1 /= 2; + q0 *= 2; + if (r0 >= y1) { + r0 -= y1; + q0++; + } + } while ((int)y1 != (int)y0); + return q0; +} + +unsigned divider(unsigned x, unsigned y) { + unsigned q0, acc; + q0 = 0; + acc = y; + + while (acc <= x) { + q0++; + acc += y; + } + + return q0; +} + +/* + * Signed division operation for faster frequency division. + */ +int sdivider(int N, int D) { + if (D < 0) { + if (N < 0) + return divider(-N, -D); + else + return -divider(N, -D); + } else { + if (N < 0) + return -divider(-N, D); + else + return divider(N, D); + } +} + +int sdivider_fast(int N, int D) { + if (D < 0) { + if (N < 0) + return divider_fast(-N, -D); + else + return -divider_fast(N, -D); + } else { + if (N < 0) + return -divider_fast(-N, D); + else + return divider_fast(N, D); + } +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/blas/Makefile b/benchmarks/polybench-syn-div/linear-algebra/blas/Makefile new file mode 100644 index 0000000..e1f3b58 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/blas/Makefile @@ -0,0 +1,3 @@ +TARGETS := gemm gemver gesummv symm syr2k syrk trmm + +include ../../common.mk diff --git a/benchmarks/polybench-syn-div/linear-algebra/blas/gemm.c b/benchmarks/polybench-syn-div/linear-algebra/blas/gemm.c new file mode 100644 index 0000000..a2c507f --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/blas/gemm.c @@ -0,0 +1,115 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* gemm.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS + #include <stdio.h> +#endif +#define plus(i) i = i + ONE + static +void init_array(int ni, int nj, int nk, + int *alpha, + int *beta, + int C[ 20 + 0][25 + 0], + int A[ 20 + 0][30 + 0], + int B[ 30 + 0][25 + 0]) +{ + int i, j; + int ONE = 1; + + *alpha = 2; + *beta = 2; + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nj; plus(j)) + C[i][j] = (int) ((i*j+ONE) % ni) / ni; + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nk; plus(j)) + A[i][j] = (int) (((i*(j+ONE)) % nk) / nk); + for (i = 0; i < nk; plus(i)) + for (j = 0; j < nj; plus(j)) + B[i][j] = (int) (((i*(j+ONE+ONE)) % nj) / nj); +} + + + + + static +int print_array(int ni, int nj, + int C[ 20 + 0][25 + 0]) +{ + int i, j; + int ONE = 1; + int res = 0; + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nj; plus(j)) { + res ^= C[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + static +void kernel_gemm(int ni, int nj, int nk, + int alpha, + int beta, + int C[ 20 + 0][25 + 0], + int A[ 20 + 0][30 + 0], + int B[ 30 + 0][25 + 0]) +{ + int i, j, k; + int ONE = 1; + + for (i = 0; i < ni; plus(i)) { + for (j = 0; j < nj; plus(j)) + C[i][j] *= beta; + for (k = 0; k < nk; plus(k)) { + for (j = 0; j < nj; plus(j)) + C[i][j] += alpha * A[i][k] * B[k][j]; + } + } + +} + + +int main() +{ + + int ni = 20; + int nj = 25; + int nk = 30; + + + int alpha; + int beta; + int C[20 + 0][25 + 0]; + int A[20 + 0][30 + 0]; + int B[30 + 0][25 + 0]; + + + init_array (ni, nj, nk, &alpha, &beta, + C, + A, + B); + + + kernel_gemm (ni, nj, nk, + alpha, beta, + C, + A, + B); + + + return + print_array(ni, nj, C); + + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/blas/gemver.c b/benchmarks/polybench-syn-div/linear-algebra/blas/gemver.c new file mode 100644 index 0000000..de8dd04 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/blas/gemver.c @@ -0,0 +1,155 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* gemver.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS + #include <stdio.h> +#endif +#define plus(i) i = i + ONE +static +void init_array (int n, + int *alpha, + int *beta, + int A[ 40 + 0][40 + 0], + int u1[ 40 + 0], + int v1[ 40 + 0], + int u2[ 40 + 0], + int v2[ 40 + 0], + int w[ 40 + 0], + int x[ 40 + 0], + int y[ 40 + 0], + int z[ 40 + 0]) +{ + int i, j; + int ONE = 1; + + *alpha = 3; + *beta = 2; + + int fn = (int)n; + + for (i = 0; i < n; plus(i)) + { + u1[i] = i; + u2[i] = ((i+ONE)/(fn*2)); + v1[i] = ((i+ONE)/(fn*4)); + v2[i] = ((i+ONE)/(fn*6)); + y[i] = ((i+ONE)/(fn*8)); + z[i] = ((i+ONE)/(fn*9)); + x[i] = 0; + w[i] = 0; + for (j = 0; j < n; plus(j)) + A[i][j] = (int) (((i*j) % n) / n); + } +} + + + + +static +int print_array(int n, + int w[ 40 + 0]) +{ + int i; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) { + res ^= w[i]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_gemver(int n, + int alpha, + int beta, + int A[ 40 + 0][40 + 0], + int u1[ 40 + 0], + int v1[ 40 + 0], + int u2[ 40 + 0], + int v2[ 40 + 0], + int w[ 40 + 0], + int x[ 40 + 0], + int y[ 40 + 0], + int z[ 40 + 0]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + A[i][j] = A[i][j] + u1[i] * v1[j] + u2[i] * v2[j]; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + x[i] = x[i] + beta * A[j][i] * y[j]; + + for (i = 0; i < n; plus(i)) + x[i] = x[i] + z[i]; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + w[i] = w[i] + alpha * A[i][j] * x[j]; + +} + + +int main() +{ + + int n = 40; + + + int alpha; + int beta; + int A[40 + 0][40 + 0]; + int u1[40 + 0]; + int v1[40 + 0]; + int u2[40 + 0]; + int v2[40 + 0]; + int w[40 + 0]; + int x[40 + 0]; + int y[40 + 0]; + int z[40 + 0]; + + + + init_array (n, &alpha, &beta, + A, + u1, + v1, + u2, + v2, + w, + x, + y, + z); + + kernel_gemver (n, alpha, beta, + A, + u1, + v1, + u2, + v2, + w, + x, + y, + z); + + return print_array(n, w); + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/blas/gesummv.c b/benchmarks/polybench-syn-div/linear-algebra/blas/gesummv.c new file mode 100644 index 0000000..457d6a8 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/blas/gesummv.c @@ -0,0 +1,116 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* gesummv.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS + #include <stdio.h> +#endif + +#define plus(i) i = i + ONE + + static +void init_array(int n, + int *alpha, + int *beta, + int A[ 30 + 0][30 + 0], + int B[ 30 + 0][30 + 0], + int x[ 30 + 0]) +{ + int i, j; + int ONE = 1; + + *alpha = 3; + *beta = 2; + for (i = 0; i < n; plus(i)) + { + x[i] = (int) ((i % n) / n); + for (j = 0; j < n; plus(j)) { + A[i][j] = (int) (((i*j+ONE) % n) / n); + B[i][j] = (int) (((i*j+ONE+ONE) % n) / n); + } + } +} + + + static +int print_array(int n, + int y[ 30 + 0]) + +{ + int i; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) { + res ^= y[i]; + } +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif + return res; +} + + static +void kernel_gesummv(int n, + int alpha, + int beta, + int A[ 30 + 0][30 + 0], + int B[ 30 + 0][30 + 0], + int tmp[ 30 + 0], + int x[ 30 + 0], + int y[ 30 + 0]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + { + tmp[i] = 0; + y[i] = 0; + for (j = 0; j < n; plus(j)) + { + tmp[i] = A[i][j] * x[j] + tmp[i]; + y[i] = B[i][j] * x[j] + y[i]; + } + y[i] = alpha * tmp[i] + beta * y[i]; + } +} + + +int main() +{ + + int n = 30; + + + int alpha; + int beta; + int A[30 + 0][30 + 0]; + int B[30 + 0][30 + 0]; + int tmp[30 + 0]; + int x[30 + 0]; + int y[30 + 0]; + + init_array (n, &alpha, &beta, + A, + B, + x); + + kernel_gesummv (n, alpha, beta, + A, + B, + tmp, + x, + y); + + + return print_array(n, y); + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/blas/symm.c b/benchmarks/polybench-syn-div/linear-algebra/blas/symm.c new file mode 100644 index 0000000..6c20b5b --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/blas/symm.c @@ -0,0 +1,114 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* symm.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS + #include <stdio.h> +#endif +#define plus(i) i = i + ONE +static +void init_array(int m, int n, + int *alpha, + int *beta, + int C[ 20 + 0][30 + 0], + int A[ 20 + 0][20 + 0], + int B[ 20 + 0][30 + 0]) +{ + int i, j; + int ONE = 1; + int HUND = 100; + + *alpha = 3; + *beta = 2; + for (i = 0; i < m; plus(i)) + for (j = 0; j < n; plus(j)) { + C[i][j] = (int) (((i+j) % HUND) / m); + B[i][j] = (int) (((n+i-j) % HUND) / m); + } + for (i = 0; i < m; plus(i)) { + for (j = 0; j <=i; plus(j)) + A[i][j] = (int) (((i+j) % HUND) / m); + for (j = i+ONE; j < m; plus(j)) + A[i][j] = -999; + } +} + +static +int print_array(int m, int n, + int C[ 20 + 0][30 + 0]) +{ + int i, j; + int ONE = 1; + int res = 0; + + for (i = 0; i < m; plus(i)) + for (j = 0; j < n; plus(j)) { + res ^= C[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + +static +void kernel_symm(int m, int n, + int alpha, + int beta, + int C[ 20 + 0][30 + 0], + int A[ 20 + 0][20 + 0], + int B[ 20 + 0][30 + 0]) +{ + int ONE = 1; + int i, j, k; + int temp2; + for (i = 0; i < m; plus(i)) + for (j = 0; j < n; plus(j) ) + { + temp2 = 0; + for (k = 0; k < i; plus(k)) { + C[k][j] += alpha*B[i][j] * A[i][k]; + temp2 += B[k][j] * A[i][k]; + } + C[i][j] = beta * C[i][j] + alpha*B[i][j] * A[i][i] + alpha * temp2; + } + +} + + +int main() +{ + + int m = 20; + int n = 30; + + int alpha; + int beta; + int C[20 + 0][30 + 0]; + int A[20 + 0][20 + 0]; + int B[20 + 0][30 + 0]; + + + init_array (m, n, &alpha, &beta, + C, + A, + B); + + kernel_symm (m, n, + alpha, beta, + C, + A, + B); + + return + print_array(m, n, C); + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/blas/syr2k.c b/benchmarks/polybench-syn-div/linear-algebra/blas/syr2k.c new file mode 100644 index 0000000..a1c0934 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/blas/syr2k.c @@ -0,0 +1,123 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* syr2k.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS + #include <stdio.h> +#endif +#define plus(i) i = i + ONE +static +void init_array(int n, int m, + int *alpha, + int *beta, + int C[ 30 + 0][30 + 0], + int A[ 30 + 0][20 + 0], + int B[ 30 + 0][20 + 0]) +{ + int i, j; + int ONE = 1; + + *alpha = 3; + *beta = 2; + for (i = 0; i < n; plus(i)) + for (j = 0; j < m; plus(j)) { + A[i][j] = (int) (((i*j+ONE) % n) / n); + B[i][j] = (int) (((i*j+ONE+ONE) % m) / m); + } + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) { + C[i][j] = (int) (((i*j+4-ONE) % n) / m); + } +} + + + + +static +int print_array(int n, + int C[ 30 + 0][30 + 0]) +{ + int i, j; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) { + res ^= C[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + +static +void kernel_syr2k(int n, int m, + int alpha, + int beta, + int C[ 30 + 0][30 + 0], + int A[ 30 + 0][20 + 0], + int B[ 30 + 0][20 + 0]) +{ + int i, j, k; + int ONE = 1; + + for (i = 0; i < n; plus(i)) { + for (j = 0; j <= i; plus(j)) + C[i][j] *= beta; + for (k = 0; k < m; plus(k)) + for (j = 0; j <= i; plus(j)) + { + C[i][j] += A[j][k]*alpha*B[i][k] + B[j][k]*alpha*A[i][k]; + } + } + +} + + +int main() +{ + + int n = 30; + int m = 20; + + + int alpha; + int beta; + int C[30 + 0][30 + 0]; + int A[30 + 0][20 + 0]; + int B[30 + 0][20 + 0]; + + + init_array (n, m, &alpha, &beta, + C, + A, + B); + + + ; + + + kernel_syr2k (n, m, + alpha, beta, + C, + A, + B); + + + ; + ; + + + + return print_array(n, C); + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/blas/syrk.c b/benchmarks/polybench-syn-div/linear-algebra/blas/syrk.c new file mode 100644 index 0000000..46ae322 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/blas/syrk.c @@ -0,0 +1,109 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* syrk.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS + #include <stdio.h> +#endif +#define plus(i) i = i + ONE +static +void init_array(int n, int m, + int *alpha, + int *beta, + int C[ 30 + 0][30 + 0], + int A[ 30 + 0][20 + 0]) +{ + int i, j; + int ONE = 1; + + *alpha = 3; + *beta = 2; + for (i = 0; i < n; plus(i)) + for (j = 0; j < m; plus(j)) + A[i][j] = (int) (((i*j+ONE) % n) / n); + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + C[i][j] = (int) (((i*j+ONE+ONE) % m) / m); +} + + +static +int print_array(int n, + int C[ 30 + 0][30 + 0]) +{ + int i, j; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) { + res ^= C[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_syrk(int n, int m, + int alpha, + int beta, + int C[ 30 + 0][30 + 0], + int A[ 30 + 0][20 + 0]) +{ + int i, j, k; + int ONE = 1; + + for (i = 0; i < n; plus(i)) { + for (j = 0; j <= i; plus(j)) + C[i][j] *= beta; + for (k = 0; k < m; plus(k)) { + for (j = 0; j <= i; plus(j)) + C[i][j] += alpha * A[i][k] * A[j][k]; + } + } + +} + + +int main() +{ + + int n = 30; + int m = 20; + + + int alpha; + int beta; + int C[30 + 0][30 + 0]; + int A[30 + 0][20 + 0]; + + + init_array (n, m, &alpha, &beta, C, A); + + + ; + + + kernel_syrk (n, m, alpha, beta, C, A); + + + ; + ; + + + + return print_array(n, C); + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/blas/trmm.c b/benchmarks/polybench-syn-div/linear-algebra/blas/trmm.c new file mode 100644 index 0000000..3fdbc45 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/blas/trmm.c @@ -0,0 +1,99 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* trmm.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS + #include <stdio.h> +#endif +#define plus(i) i = i + ONE + static +void init_array(int m, int n, + int *alpha, + int A[ 20 + 0][20 + 0], + int B[ 20 + 0][30 + 0]) +{ + int i, j; + int ONE = 1; + + *alpha = 3; + for (i = 0; i < m; plus(i)) { + for (j = 0; j < i; plus(j)) { + A[i][j] = (int) (((i+j) % m) / m); + } + A[i][i] = 1; + for (j = 0; j < n; plus(j)) { + B[i][j] = (int)(((n+i-j) % n) / n); + } + } + +} + + + + + static +int print_array(int m, int n, + int B[ 20 + 0][30 + 0]) +{ + int i, j; + int ONE = 1; + int res = 0; + + for (i = 0; i < m; plus(i)) + for (j = 0; j < n; plus(j)) { + res ^= B[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + + static +void kernel_trmm(int m, int n, + int alpha, + int A[ 20 + 0][20 + 0], + int B[ 20 + 0][30 + 0]) +{ + int i, j, k; + int ONE = 1; + for (i = 0; i < m; plus(i)) + for (j = 0; j < n; plus(j)) { + for (k = i+ONE; k < m; plus(k)) + B[i][j] += A[k][i] * B[k][j]; + B[i][j] = alpha * B[i][j]; + } + +} + + +int main() +{ + + int m = 20; + int n = 30; + + + int alpha; + int A[20 + 0][20 + 0]; + int B[20 + 0][30 + 0]; + + + init_array (m, n, &alpha, A, B); + + + kernel_trmm (m, n, alpha, A, B); + + return print_array(m, n, B); + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/kernels/2mm.c b/benchmarks/polybench-syn-div/linear-algebra/kernels/2mm.c new file mode 100644 index 0000000..0b6677f --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/kernels/2mm.c @@ -0,0 +1,132 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* 2mm.c: this file is part of PolyBench/C */ + + +#ifndef SYNTHESIS + #include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array(int ni, int nj, int nk, int nl, + int *alpha, + int *beta, + int A[ 16 + 0][22 + 0], + int B[ 22 + 0][18 + 0], + int C[ 18 + 0][24 + 0], + int D[ 16 + 0][24 + 0]) +{ + int i, j; + int ONE = 1; + + *alpha = 2; + *beta = 2; + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nk; plus(j)) + A[i][j] = (int) (((i*j+ONE) % ni) / ni); + for (i = 0; i < nk; plus(i)) + for (j = 0; j < nj; plus(j)) + B[i][j] = (int) (((i*(j+ONE)) % nj) / nj); + for (i = 0; i < nj; plus(i)) + for (j = 0; j < nl; plus(j)) + C[i][j] = (int) (((i*(j+ONE+ONE+ONE)+ONE) % nl) / nl); + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nl; plus(j)) + D[i][j] = (int) (((i*(j+ONE+ONE)) % nk) / nk); +} + +static +int print_array(int ni, int nl, + int D[ 16 + 0][24 + 0]) +{ + int i, j; + int ONE = 1; + int res = 0; + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nl; plus(j)) { + res ^= D[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_2mm(int ni, int nj, int nk, int nl, + int alpha, + int beta, + int tmp[ 16 + 0][18 + 0], + int A[ 16 + 0][22 + 0], + int B[ 22 + 0][18 + 0], + int C[ 18 + 0][24 + 0], + int D[ 16 + 0][24 + 0]) +{ + int ONE = 1; + int i, j, k; + + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nj; plus(j)) + { + tmp[i][j] = 0; + for (k = 0; k < nk; plus(k)) + tmp[i][j] += alpha * A[i][k] * B[k][j]; + } + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nl; plus(j)) + { + D[i][j] *= beta; + for (k = 0; k < nj; plus(k)) + D[i][j] += tmp[i][k] * C[k][j]; + } + +} + + +int main() +{ + + int ni = 16; + int nj = 18; + int nk = 22; + int nl = 24; + + int alpha; + int beta; + int tmp[16 + 0][18 + 0]; + int A[16 + 0][22 + 0]; + int B[22 + 0][18 + 0]; + int C[18 + 0][24 + 0]; + int D[16 + 0][24 + 0]; + + + init_array (ni, nj, nk, nl, &alpha, &beta, + A, + B, + C, + D); + + + kernel_2mm (ni, nj, nk, nl, + alpha, beta, + tmp, + A, + B, + C, + D); + + + return print_array(ni, nl, D); + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/kernels/3mm.c b/benchmarks/polybench-syn-div/linear-algebra/kernels/3mm.c new file mode 100644 index 0000000..d0b086b --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/kernels/3mm.c @@ -0,0 +1,142 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* 3mm.c: this file is part of PolyBench/C */ + + +#ifndef SYNTHESIS + #include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array(int ni, int nj, int nk, int nl, int nm, + int A[ 16 + 0][20 + 0], + int B[ 20 + 0][18 + 0], + int C[ 18 + 0][24 + 0], + int D[ 24 + 0][22 + 0]) +{ + int i, j; + int ONE = 1; + int TWO = 2; + int THREE = 3; + + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nk; plus(j)) + A[i][j] = (int) (((i*j+ONE) % ni) / (5*ni)); + for (i = 0; i < nk; plus(i)) + for (j = 0; j < nj; plus(j)) + B[i][j] = (int) (((i*(j+ONE)+TWO) % nj) / (5*nj)); + for (i = 0; i < nj; plus(i)) + for (j = 0; j < nm; plus(j)) + C[i][j] = (int) (((i*(j+THREE)) % nl) / (5*nl)); + for (i = 0; i < nm; plus(i)) + for (j = 0; j < nl; plus(j)) + D[i][j] = (int) (((i*(j+TWO)+TWO) % nk) / (5*nk)); +} + + +static +int print_array(int ni, int nl, + int G[ 16 + 0][22 + 0]) +{ + int i, j; + int ONE = 1; + int res = 0; + + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nl; plus(j)) { + res ^= G[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_3mm(int ni, int nj, int nk, int nl, int nm, + int E[ 16 + 0][18 + 0], + int A[ 16 + 0][20 + 0], + int B[ 20 + 0][18 + 0], + int F[ 18 + 0][22 + 0], + int C[ 18 + 0][24 + 0], + int D[ 24 + 0][22 + 0], + int G[ 16 + 0][22 + 0]) +{ + int ONE = 1; + int i, j, k; + + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nj; plus(j)) + { + E[i][j] = 0; + for (k = 0; k < nk; plus(k)) + E[i][j] += A[i][k] * B[k][j]; + } + + for (i = 0; i < nj; plus(i)) + for (j = 0; j < nl; plus(j)) + { + F[i][j] = 0; + for (k = 0; k < nm; plus(k)) + F[i][j] += C[i][k] * D[k][j]; + } + + for (i = 0; i < ni; plus(i)) + for (j = 0; j < nl; plus(j)) + { + G[i][j] = 0; + for (k = 0; k < nj; plus(k)) + G[i][j] += E[i][k] * F[k][j]; + } + +} + +int main() +{ + + int ni = 16; + int nj = 18; + int nk = 20; + int nl = 22; + int nm = 24; + + + int E[16 + 0][18 + 0]; + int A[16 + 0][20 + 0]; + int B[20 + 0][18 + 0]; + int F[18 + 0][22 + 0]; + int C[18 + 0][24 + 0]; + int D[24 + 0][22 + 0]; + int G[16 + 0][22 + 0]; + + + init_array (ni, nj, nk, nl, nm, + A, + B, + C, + D); + + kernel_3mm (ni, nj, nk, nl, nm, + E, + A, + B, + F, + C, + D, + G); + + + return print_array(ni, nl, G); + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/kernels/Makefile b/benchmarks/polybench-syn-div/linear-algebra/kernels/Makefile new file mode 100644 index 0000000..4b7f6e1 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/kernels/Makefile @@ -0,0 +1,3 @@ +TARGETS := 2mm 3mm atas bicg doitgen mvt + +include ../../common.mk diff --git a/benchmarks/polybench-syn-div/linear-algebra/kernels/atas.c b/benchmarks/polybench-syn-div/linear-algebra/kernels/atas.c new file mode 100644 index 0000000..970465b --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/kernels/atas.c @@ -0,0 +1,103 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* atax.c: this file is part of PolyBench/C */ + +#include "../../include/misc.h" + +#ifndef SYNTHESIS + #include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int m, int n, + int A[ 38 + 0][42 + 0], + int x[ 42 + 0]) +{ + int ONE = 1; + int i, j; + int fn; + fn = (int)n; + + for (i = 0; i < n; plus(i)) + x[i] = ONE + (i / fn); + for (i = 0; i < m; plus(i)) + for (j = 0; j < n; plus(j)) + A[i][j] = (int) (((i+j) % n) / (5*m)); +} + + +static +int print_array(int n, + int y[ 42 + 0]) + +{ + int i; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) { + res ^= y[i]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + +static +void kernel_atax(int m, int n, + int A[ 38 + 0][42 + 0], + int x[ 42 + 0], + int y[ 42 + 0], + int tmp[ 38 + 0]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + y[i] = 0; + for (i = 0; i < m; plus(i)) + { + tmp[i] = 0; + for (j = 0; j < n; plus(j)) + tmp[i] = tmp[i] + A[i][j] * x[j]; + for (j = 0; j < n; plus(j)) + y[j] = y[j] + A[i][j] * tmp[i]; + } + +} + + +int main() +{ + + int m = 38; + int n = 42; + + + int A[38 + 0][42 + 0]; + int x[42 + 0]; + int y[42 + 0]; + int tmp[38 + 0]; + + init_array (m, n, A, x); + + kernel_atax (m, n, + A, + x, + y, + tmp); + + + return print_array(n, y); + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/kernels/bicg.c b/benchmarks/polybench-syn-div/linear-algebra/kernels/bicg.c new file mode 100644 index 0000000..4d1f9b6 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/kernels/bicg.c @@ -0,0 +1,120 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* bicg.c: this file is part of PolyBench/C */ + + +#ifndef SYNTHESIS + #include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int m, int n, + int A[ 42 + 0][38 + 0], + int r[ 42 + 0], + int p[ 38 + 0]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < m; plus(i)) + p[i] = ((i % m) / m); + for (i = 0; i < n; plus(i)) { + r[i] = ((i % n) / n); + for (j = 0; j < m; plus(j)) + A[i][j] = (((i*(j+ONE)) % n) / n); + } +} + + + + +static +int print_array(int m, int n, + int s[ 38 + 0], + int q[ 42 + 0]) + +{ + int i; + int ONE = 1; + int res = 0; + + for (i = 0; i < m; plus(i)) { + res ^= s[i]; + } + for (i = 0; i < n; plus(i)) { + res ^= q[i]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_bicg(int m, int n, + int A[ 42 + 0][38 + 0], + int s[ 38 + 0], + int q[ 42 + 0], + int p[ 38 + 0], + int r[ 42 + 0]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < m; plus(i)) + s[i] = 0; + for (i = 0; i < n; plus(i)) + { + q[i] = 0; + for (j = 0; j < m; plus(j)) + { + s[j] = s[j] + r[i] * A[i][j]; + q[i] = q[i] + A[i][j] * p[j]; + } + } + +} + + +int main() +{ + + int n = 42; + int m = 38; + + + int A[42 + 0][38 + 0]; + int s[38 + 0]; + int q[42 + 0]; + int p[38 + 0]; + int r[42 + 0]; + + + init_array (m, n, + A, + r, + p); + + kernel_bicg (m, n, + A, + s, + q, + p, + r); + + + return print_array(m, n, s, q); + + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/kernels/doitgen.c b/benchmarks/polybench-syn-div/linear-algebra/kernels/doitgen.c new file mode 100644 index 0000000..6eaef56 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/kernels/doitgen.c @@ -0,0 +1,105 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* doitgen.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS + #include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array(int nr, int nq, int np, + int A[ 10 + 0][8 + 0][12 + 0], + int C4[ 12 + 0][12 + 0]) +{ + int i, j, k; + int ONE = 1; + + for (i = 0; i < nr; plus(i)) + for (j = 0; j < nq; plus(j)) + for (k = 0; k < np; plus(k)) + A[i][j][k] = (int) (((i*j + k) % np) / np); + for (i = 0; i < np; plus(i)) + for (j = 0; j < np; plus(j)) + C4[i][j] = (int) (((i*j) % np) / np); +} + + +static +int print_array(int nr, int nq, int np, + int A[ 10 + 0][8 + 0][12 + 0]) +{ + int i, j, k; + int ONE = 1; + int res = 0; + + for (i = 0; i < nr; plus(i)) + for (j = 0; j < nq; plus(j)) + for (k = 0; k < np; plus(k)) { + res ^= A[i][j][k]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +void kernel_doitgen(int nr, int nq, int np, + int A[ 10 + 0][8 + 0][12 + 0], + int C4[ 12 + 0][12 + 0], + int sum[ 12 + 0]) +{ + int r, q, p, s; + int ONE = 1; + + for (r = 0; r < nr; plus(r)) + for (q = 0; q < nq; plus(q)) { + for (p = 0; p < np; plus(p)) { + sum[p] = 0; + for (s = 0; s < np; plus(s)) + sum[p] += A[r][q][s] * C4[s][p]; + } + for (p = 0; p < np; plus(p)) + A[r][q][p] = sum[p]; + } + +} + + +int main() +{ + + int nr = 10; + int nq = 8; + int np = 12; + + + int A[10 + 0][8 + 0][12 + 0]; + int sum[12 + 0]; + int C4[12 + 0][12 + 0]; + + + init_array (nr, nq, np, + A, + C4); + + + kernel_doitgen (nr, nq, np, + A, + C4, + sum); + + + + return print_array(nr, nq, np, A); +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/kernels/mvt.c b/benchmarks/polybench-syn-div/linear-algebra/kernels/mvt.c new file mode 100644 index 0000000..4548ca5 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/kernels/mvt.c @@ -0,0 +1,124 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* mvt.c: this file is part of PolyBench/C */ + +#include "../../include/misc.h" + +#ifndef SYNTHESIS + #include <stdio.h> +#endif + +#define plus(i) i = i + ONE + +static +void init_array(int n, + int x1[ 40 + 0], + int x2[ 40 + 0], + int y_1[ 40 + 0], + int y_2[ 40 + 0], + int A[ 40 + 0][40 + 0]) +{ + int i, j; + int ONE = 1; + int THREE = 3; + + for (i = 0; i < n; plus(i)) + { + x1[i] = (int) ((i % n) / n); + x2[i] = (int) (((i + ONE) % n) / n); + y_1[i] = (int) (((i + THREE) % n) / n); + y_2[i] = (int) (((i + 4) % n) / n); + for (j = 0; j < n; plus(j)) + A[i][j] = (int) (((i*j) % n) / n); + } +} + + + + + static +int print_array(int n, + int x1[ 40 + 0], + int x2[ 40 + 0]) + +{ + int i; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) { + res ^= x1[i]; + } + + for (i = 0; i < n; plus(i)) { + res ^= x2[i]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_mvt(int n, + int x1[ 40 + 0], + int x2[ 40 + 0], + int y_1[ 40 + 0], + int y_2[ 40 + 0], + int A[ 40 + 0][40 + 0]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + x1[i] = x1[i] + A[i][j] * y_1[j]; + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + x2[i] = x2[i] + A[j][i] * y_2[j]; + +} + + +int main() +{ + + int n = 40; + + + int A[40 + 0][40 + 0]; + int x1[40 + 0]; + int x2[40 + 0]; + int y_1[40 + 0]; + int y_2[40 + 0]; + + + + init_array (n, + x1, + x2, + y_1, + y_2, + A); + + + kernel_mvt (n, + x1, + x2, + y_1, + y_2, + A); + + return print_array(n, x1, x2); + +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/solvers/Makefile b/benchmarks/polybench-syn-div/linear-algebra/solvers/Makefile new file mode 100644 index 0000000..146620b --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/solvers/Makefile @@ -0,0 +1,3 @@ +TARGETS := cholesky durbin lu ludcmp trisolv + +include ../../common.mk diff --git a/benchmarks/polybench-syn-div/linear-algebra/solvers/cholesky.c b/benchmarks/polybench-syn-div/linear-algebra/solvers/cholesky.c new file mode 100644 index 0000000..5f10ab9 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/solvers/cholesky.c @@ -0,0 +1,129 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* cholesky.c: this file is part of PolyBench/C */ + +#include "../../include/misc.h" + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +# define SQRT_FUN(x) sqrtf(x) + +#define plus(i) i = i + ONE +static +void init_array(int n, + int A[40][40]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + { + for (j = 0; j <= i; plus(j)) + A[i][j] = (int)(((-j) % n) / n) + ONE; + for (j = i + ONE; j < n; plus(j)) { + A[i][j] = 0; + } + A[i][i] = 1; + } + + + int r,s,t; + int B[40][40]; + for (r = 0; r < n; ++r) + for (s = 0; s < n; ++s) + B[r][s] = 0; + for (t = 0; t < n; ++t) + for (r = 0; r < n; ++r) + for (s = 0; s < n; ++s) + B[r][s] += A[r][t] * A[s][t]; + for (r = 0; r < n; ++r) + for (s = 0; s < n; ++s) + A[r][s] = B[r][s]; + +} + + + + +static +int check_array(int n, + int A[40][40]) + +{ + int res = 0; + int ONE = 1; + int i, j; + + for (i = 0; i < n; plus(i)) + for (j = 0; j <= i; plus(j)) { + if(A[i][j]!=0) res = 1; + } + #ifndef SYNTHESIS + printf("finished: %u\n", res); + #endif + + return res; +} + + + + +static +void kernel_cholesky(int n, + int A[40][40]) +{ + int i, j, k; + int ONE = 1; + + for (i = 0; i < n; plus(i)) { + + for (j = 0; j < i; plus(j)) { + for (k = 0; k < j; plus(k)) { + A[i][j] -= A[i][k] * A[j][k]; + } + A[i][j] = (A[i][j] / A[j][j]); + } + + for (k = 0; k < i; plus(k)) { + A[i][i] -= A[i][k] * A[i][k]; + } + int sq = 0; int val = 0; int cmp = A[i][i]; + while(sq <= cmp) { + val = val + ONE; + sq = val * val; + } + A[i][i] = val; + } + +} + + +int main() +{ + + int n = 40; + + + int A[40][40]; + + + init_array (n, A); + + + kernel_cholesky (n, A); + + + return check_array(n, A); + + + return 0; +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/solvers/durbin.c b/benchmarks/polybench-syn-div/linear-algebra/solvers/durbin.c new file mode 100644 index 0000000..5646e6e --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/solvers/durbin.c @@ -0,0 +1,98 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* durbin.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE +/* Include polybench common header. */ +static +void init_array (int n, + int r[ 40 + 0]) +{ + int ONE = 1; + int i; + + for (i = 0; i < n; plus(i)) + { + r[i] = (n+ONE-i); + } +} + + + +static +int print_array(int n, + int y[ 40 + 0]) + +{ + int ONE = 1; + int i; + int res = 0; + + for (i = 0; i < n; plus(i)) { + res ^= y[i]; + } + +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif + + return res; +} + +static +void kernel_durbin(int n, + int r[ 40 + 0], + int y[ 40 + 0]) +{ + int z[40]; + int alpha; + int beta; + int sum; + + int ONE = 1; + int i,k; + y[0] = -r[0]; + beta = 1; + alpha = -r[0]; + + for (k = 1; k < n; plus(k)) { + beta = (ONE-alpha*alpha)*beta; + sum = 0; + for (i=0; i<k; plus(i)) { + sum += r[k-i-ONE]*y[i]; + } + alpha = - (r[k] + sum / beta); + + for (i=0; i<k; plus(i)) { + z[i] = y[i] + alpha*y[k-i-ONE]; + } + for (i=0; i<k; plus(i)) { + y[i] = z[i]; + } + y[k] = alpha; + } +} + + +int main() +{ + int n = 40; + int r[40 + 0]; + int y[40 + 0]; + + init_array (n, r); + kernel_durbin (n, r, y); + + return print_array(n, y); +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/solvers/lu.c b/benchmarks/polybench-syn-div/linear-algebra/solvers/lu.c new file mode 100644 index 0000000..e0e8bfb --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/solvers/lu.c @@ -0,0 +1,116 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* lu.c: this file is part of PolyBench/C */ + +//#include <stdio.h> +//#include <unistd.h> +//#include <string.h> +//#include <math.h> + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE + +static +void init_array (int n, + int A[40][40]) +{ + int ONE = 1; + int i, j; + + for (i = 0; i < n; plus(i)) + { + for (j = 0; j <= i; plus(j)) + A[i][j] = (((-j) % n) / n) + ONE; + for (j = i+1; j < n; plus(j)) { + A[i][j] = 0; + } + A[i][i] = 1; + } + + + + int r,s,t; + int B[40][40]; // B = (int(*)[40 + 0][40 + 0])polybench_alloc_data ((40 + 0) * (40 + 0), sizeof(int));; + for (r = 0; r < n; plus(r)) + for (s = 0; s < n; plus(s)) + B[r][s] = 0; + for (t = 0; t < n; plus(t)) + for (r = 0; r < n; plus(r)) + for (s = 0; s < n; plus(s)) + B[r][s] += A[r][t] * A[s][t]; + for (r = 0; r < n; plus(r)) + for (s = 0; s < n; plus(s)) + A[r][s] = B[r][s]; + //free((void*)B);; + +} + +static +void kernel_lu(int n, + int A[ 40][40]) +{ + int i, j, k; + int ONE = 1; + + for (i = 0; i < n; plus(i)) { + for (j = 0; j <i; plus(j)) { + for (k = 0; k < j; plus(k)) { + A[i][j] -= A[i][k] * A[k][j]; + } + A[i][j] = (A[i][j] / A[j][j]); + } + for (j = i; j < n; plus(j)) { + for (k = 0; k < i; plus(k)) { + A[i][j] -= A[i][k] * A[k][j]; + } + } + } +} + +static +int check_array(int n, + int A[40][40]) +{ + int res = 0; + int i, j; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + if(A[i][j] !=0) res = 1; + #ifndef SYNTHESIS + printf("finished: %u\n", res); + #endif + + return res; +} + + +int main() +{ + + int n = 40; + + + int A[40][40]; //A = (int(*)[40 + 0][40 + 0])polybench_alloc_data ((40 + 0) * (40 + 0), sizeof(int));; + + + init_array (n, A); + + kernel_lu (n, A); + + return check_array(n, A); + return 0; + + //free((void*)A);; +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/solvers/ludcmp.c b/benchmarks/polybench-syn-div/linear-algebra/solvers/ludcmp.c new file mode 100644 index 0000000..bd8804c --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/solvers/ludcmp.c @@ -0,0 +1,163 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* ludcmp.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE + + static +void init_array (int n, + int A[ 40 + 0][40 + 0], + int b[ 40 + 0], + int x[ 40 + 0], + int y[ 40 + 0]) +{ + int i, j; + int ONE = 1; + int fn = (int)n; + + for (i = 0; i < n; plus(i)) + { + x[i] = 0; + y[i] = 0; + b[i] = ((i+1) / (fn*2)) + 4; + } + + for (i = 0; i < n; plus(i)) + { + for (j = 0; j <= i; plus(j)) + A[i][j] = (int)(((-j) % n) / n) + 1; + for (j = i+ONE; j < n; plus(j)) { + A[i][j] = 0; + } + A[i][i] = 1; + } + + + + int r,s,t; + int B[40 + 0][40 + 0]; + for (r = 0; r < n; plus(r)) + for (s = 0; s < n; plus(s)) + B[r][s] = 0; + for (t = 0; t < n; plus(t)) + for (r = 0; r < n; plus(r)) + for (s = 0; s < n; plus(s)) + B[r][s] += A[r][t] * A[s][t]; + for (r = 0; r < n; plus(r)) + for (s = 0; s < n; plus(s)) + A[r][s] = B[r][s]; + +} + + + + + static +int check_array(int n, + int x[ 40 + 0]) + +{ + int i; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) { + res ^= x[i]; + } +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif + return res; +} + + + + + static +void kernel_ludcmp(int n, + int A[ 40 + 0][40 + 0], + int b[ 40 + 0], + int x[ 40 + 0], + int y[ 40 + 0]) +{ + int i, j, k; + int ONE = 1; + + int w; + + for (i = 0; i < n; plus(i)) { + for (j = 0; j <i; plus(j)) { + w = A[i][j]; + for (k = 0; k < j; plus(k)) { + w -= A[i][k] * A[k][j]; + } + A[i][j] = (w / A[j][j]); + } + for (j = i; j < n; plus(j)) { + w = A[i][j]; + for (k = 0; k < i; plus(k)) { + w -= A[i][k] * A[k][j]; + } + A[i][j] = w; + } + } + + for (i = 0; i < n; plus(i)) { + w = b[i]; + for (j = 0; j < i; plus(j)) + w -= A[i][j] * y[j]; + y[i] = w; + } + + for (i = n-ONE; i >=0; i=i-ONE) { + w = y[i]; + for (j = i+ONE; j < n; plus(j)) + w -= A[i][j] * x[j]; + x[i] = (w / A[i][i]); + } + +} + + +int main() +{ + + int n = 40; + + + int A[40 + 0][40 + 0]; + int b[40 + 0]; + int x[40 + 0]; + int y[40 + 0]; + + + + init_array (n, + A, + b, + x, + y); + + + kernel_ludcmp (n, + A, + b, + x, + y); + + return check_array(n, x); + + + return 0; +} diff --git a/benchmarks/polybench-syn-div/linear-algebra/solvers/trisolv.c b/benchmarks/polybench-syn-div/linear-algebra/solvers/trisolv.c new file mode 100644 index 0000000..f426853 --- /dev/null +++ b/benchmarks/polybench-syn-div/linear-algebra/solvers/trisolv.c @@ -0,0 +1,97 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* trisolv.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array(int n, + int L[ 40 ][40 ], + int x[ 40 ], + int b[ 40 ]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + { + x[i] = -999; + b[i] = i ; + for (j = 0; j <= i; plus(j)) + L[i][j] = (int) (((i+n-j+ONE)*(ONE+ONE)) / n); + } +} + + + + +static +int check_array(int n, + int x[ 40]) + +{ + int i; + int res = 0; + int ONE = 1; + for (i = 0; i < n; plus(i)) { + res ^= x[i]; + } + +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif + return res; +} + + + + +static +void kernel_trisolv(int n, + int L[ 40 + 0][40 + 0], + int x[ 40 + 0], + int b[ 40 + 0]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + { + x[i] = b[i]; + for (j = 0; j <i; plus(j)) + x[i] -= L[i][j] * x[j]; + + x[i] = (x[i] / L[i][i]); + + } + +} + + +int main() +{ + + int n = 40; + + + int L[40 + 0][40 + 0]; + int x[40 + 0]; + int b[40 + 0]; + + init_array (n, L, x, b); + kernel_trisolv (n, L, x, b); + + return check_array(n, x); + + return 0; +} diff --git a/benchmarks/polybench-syn-div/medley/Makefile b/benchmarks/polybench-syn-div/medley/Makefile new file mode 100644 index 0000000..01da9de --- /dev/null +++ b/benchmarks/polybench-syn-div/medley/Makefile @@ -0,0 +1,6 @@ +TARGETS := floyd-warshall nussinov + +include ../common.mk + +floyd-warshall.v: floyd-warshall.c + $(VERICERT) $(VERICERT_OPTS) -O0 -finline $< -o $@ diff --git a/benchmarks/polybench-syn-div/medley/floyd-warshall.c b/benchmarks/polybench-syn-div/medley/floyd-warshall.c new file mode 100644 index 0000000..776d95a --- /dev/null +++ b/benchmarks/polybench-syn-div/medley/floyd-warshall.c @@ -0,0 +1,91 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* floyd-warshall.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS + #include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int n, + int path[ 60 + 0][60 + 0]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) { + path[i][j] = i*(j % (ONE+6))+ONE; + //if (((i+j)%13 == ZERO || (i+j)%7== ZERO || (i+j)%11 == ZERO ) != 0 ) + if(((((i+j) % (12+ONE)) == (int)0 || ((i+j) % (ONE+6)) == (int)0)!=0 || ((i+j) % (10+ONE)) == (int)0 ) != 0) + path[i][j] = 999; + } +} + + + + +static +int print_array(int n, + int path[ 60 + 0][60 + 0]) + +{ + int i, j; + int res = 0; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) { + res ^= path[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_floyd_warshall(int n, + int path[ 60 + 0][60 + 0]) +{ + int i, j, k; + int ONE = 1; + + for (k = 0; k < n; plus(k)) + { + for(i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + path[i][j] = path[i][j] < path[i][k] + path[k][j] ? + path[i][j] : path[i][k] + path[k][j]; + } + +} + + +int main() +{ + + int n = 60; + + + int path[60 + 0][60 + 0]; + + init_array (n, path); + + kernel_floyd_warshall (n, path); + + return print_array(n, path); + + return 0; +} diff --git a/benchmarks/polybench-syn-div/medley/nussinov.c b/benchmarks/polybench-syn-div/medley/nussinov.c new file mode 100644 index 0000000..e2e06d3 --- /dev/null +++ b/benchmarks/polybench-syn-div/medley/nussinov.c @@ -0,0 +1,111 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* nussinov.c: this file is part of PolyBench/C */ + +typedef int base; + +#ifndef SYNTHESIS + #include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int n, + base seq[ 60 + 0], + int table[ 60 + 0][60 + 0]) +{ + int i, j; + int ONE = 1; + int FOUR = 4; + + + for (i=0; i <n; plus(i)) { + seq[i] = (base)(((i+ONE) % FOUR)); + } + + for (i=0; i <n; plus(i)) + for (j=0; j <n; plus(j)) + table[i][j] = 0; +} + + + + +static +int print_array(int n, + int table[ 60 + 0][60 + 0]) + +{ + int i, j; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) { + for (j = i; j < n; plus(j)) { + res ^= table[i][j]; + } + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + +static +void kernel_nussinov(int n, base seq[ 60 + 0], + int table[ 60 + 0][60 + 0]) +{ + int i, j, k; + int ZERO = 0; + int ONE = 1; + int THREE = 3; + + for (i = n-ONE; i >= ZERO; i=i-ONE) { + for (j=i+ONE; j<n; plus(j)) { + + if (j-ONE>=ZERO) + table[i][j] = ((table[i][j] >= table[i][j-ONE]) ? table[i][j] : table[i][j-ONE]); + if (i+ONE<n) + table[i][j] = ((table[i][j] >= table[i+ONE][j]) ? table[i][j] : table[i+ONE][j]); + + if ((j-ONE>=ZERO && i+ONE<n) != (int)0) { + + if (i<j-ONE) + table[i][j] = ((table[i][j] >= table[i+ONE][j-ONE]+(((seq[i])+(seq[j])) == THREE ? ONE : ZERO)) ? table[i][j] : table[i+ONE][j-ONE]+(((seq[i])+(seq[j])) == THREE ? ONE : ZERO)); + else + table[i][j] = ((table[i][j] >= table[i+ONE][j-ONE]) ? table[i][j] : table[i+ONE][j-ONE]); + } + + for (k=i+ONE; k<j; plus(k)) { + table[i][j] = ((table[i][j] >= table[i][k] + table[k+ONE][j]) ? table[i][j] : table[i][k] + table[k+ONE][j]); + } + } + } + +} + + +int main() +{ + + int n = 60; + + + base (seq)[60 + 0]; + int (table)[60 + 0][60 + 0]; + + + init_array (n, seq, table); + + kernel_nussinov (n, seq, table); + + return print_array(n, table); + +} diff --git a/benchmarks/polybench-syn-div/poly.csv b/benchmarks/polybench-syn-div/poly.csv new file mode 100644 index 0000000..fe71983 --- /dev/null +++ b/benchmarks/polybench-syn-div/poly.csv @@ -0,0 +1,26 @@ +benchmark,legupcycles,legupfreqMHz,leguplogicutilisation,legupregs,leguprams,legupdsps,legupcomptime,vericertcycles,vericertfreqMHz,vericertlogicutilisation,vericertregs,vericertrams,vericertdsps,vericertcomptime +durbin,15106,188.61,2509,4008,0,8,4.77,19852,199.2,3027,6168,0,8,0.077 +lu,482766,244.62,3116,4593,0,10,4.72,2634766,92.97,54806,106037,0,6,0.097 +ludcmp,470843,249.69,3605,5397,0,15,4.87,2401354,83.52,57145,111408,0,10,0.132 +trisolv,35382,213.9,2412,3749,0,3,4.73,33550,112.59,28101,55109,0,2,0.086 +2mm,60088,226.5,1114,1936,0,7,4.80,427098,116.9,32600,63212,0,18,0.136 +3mm,204195,188.96,4210,4801,0,43,4.88,539430,97.13,45073,89719,0,18,0.147 +atas,126288,193.24,3026,3719,0,10,4.80,92000,130.41,28603,56646,0,6,0.069 +bicg,11907,303.4,308,537,0,6,4.78,121134,122.74,30091,58799,0,8,0.097 +mvt,16806,384.47,372,597,0,4,4.79,139194,119.93,30753,60450,0,6,0.130 +doitgen,57199,252.14,909,1402,0,2,5.05,350302,126.18,19898,38461,0,4,0.105 +symm,64903,284.41,2155,3170,0,10,4.63,248930,113.92,27693,54514,0,14,0.115 +syrk,57395,278.01,598,976,0,2,4.73,309018,87.15,76889,57816,0,8,0.094 +syr2k,125705,240.85,3149,3679,0,6,4.85,478040,78.6,120116,82032,0,12,0.116 +trmm,41432,281.61,610,990,0,4,4.71,147528,105.61,64031,40502,0,4,0.089 +gemm,83676,192.68,1029,1544,0,35,4.79,360772,121.61,31853,62126,0,16,0.104 +gemver,28087,303.49,1854,2380,0,8,4.68,175326,107.27,32615,64118,0,14,0.099 +gesummv,6634,310.46,298,504,0,4,4.77,111094,79.97,113876,72908,0,10,0.101 +covariance,109992,245.16,2098,3096,0,5,4.77,297450,110.57,28729,56660,0,4,0.083 +fdtd-2d,214153,262.61,2736,3801,0,2,4.73,831912,108.23,31333,61421,0,6,0.116 +heat-3d,41059,115.54,3132,2910,0,60,4.92,555930,110.42,33915,67273,0,9,0.181 +jacobi-1d,6914,386.25,1355,1885,0,0,4.72,16606,277.93,1636,3305,0,0,0.071 +jacobi-2d,84609,240.79,2347,3185,0,2,4.81,357100,113.53,30393,59782,0,4,0.079 +seidel-2d,345294,232.4,2128,3337,0,2,4.68,875758,127.99,26948,53133,0,2,0.091 +floyd-warshall,1238764,235.52,1869,2367,0,2,4.71,4762766,109.4,59859,118101,0,2,0.094 +nussinov,216467,273.07,1078,1431,0,2,4.79,837958,90.73,60663,119303,0,0,0.080 diff --git a/benchmarks/polybench-syn-div/quartus_synth.tcl b/benchmarks/polybench-syn-div/quartus_synth.tcl new file mode 100644 index 0000000..6edbf0c --- /dev/null +++ b/benchmarks/polybench-syn-div/quartus_synth.tcl @@ -0,0 +1,35 @@ +# PRiME pre-KAPow kernel flow +# Performs pre-KAPow run steps for instrumenting arbitrary Verilog for power monitoring +# James Davis, 2015 + +load_package flow + +project_new -overwrite syn +set_global_assignment -name FAMILY "Arria 10" +set_global_assignment -name DEVICE 10AX115H4F34E3LG +set_global_assignment -name SYSTEMVERILOG_FILE top.v +set_global_assignment -name TOP_LEVEL_ENTITY main +#set_global_assignment -name SDC_FILE syn.sdc +#set_global_assignment -name auto_resource_sharing on +#set_global_assignment -name enable_state_machine_inference on +#set_global_assignment -name optimization_technique area +#set_global_assignment -name synthesis_effort fast +#set_global_assignment -name AUTO_RAM_RECOGNITION on +#set_global_assignment -name remove_duplicate_registers on +#set_instance_assignment -name RAMSTYLE_ATTRIBUTE LOGIC -to ram + +execute_module -tool map + +execute_module -tool fit + +execute_module -tool sta + +#execute_module -tool eda -args "--simulation --tool=vcs" + +# set_global_assignment -name POWER_OUTPUT_SAF_NAME ${kernel}.asf +# set_global_assignment -name POWER_DEFAULT_INPUT_IO_TOGGLE_RATE "12.5 %" +# set_global_assignment -name POWER_REPORT_SIGNAL_ACTIVITY ON +# set_global_assignment -name POWER_REPORT_POWER_DISSIPATION ON +# execute_module -tool pow + +project_close diff --git a/benchmarks/polybench-syn-div/run-vericert.sh b/benchmarks/polybench-syn-div/run-vericert.sh new file mode 100755 index 0000000..6cf4cd9 --- /dev/null +++ b/benchmarks/polybench-syn-div/run-vericert.sh @@ -0,0 +1,41 @@ +#!/usr/bin/env bash + +rm exec.csv + +top=$(pwd) + #set up +while read benchmark ; do + echo "Running "$benchmark + ./$benchmark.gcc > $benchmark.clog + cresult=$(cat $benchmark.clog | cut -d' ' -f2) + echo "C output: "$cresult + ./$benchmark.iver > $benchmark.tmp + veriresult=$(tail -1 $benchmark.tmp | cut -d' ' -f2) + cycles=$(tail -2 $benchmark.tmp | head -1 | tr -s ' ' | cut -d' ' -f2) + echo "Verilog output: "$veriresult + + #Undefined checks + if test -z $veriresult + then + echo "FAIL: Verilog returned nothing" + #exit 0 + fi + + # Don't care checks + if [ $veriresult == "x" ] + then + echo "FAIL: Verilog returned don't cares" + #exit 0 + fi + + # unequal result check + if [ $cresult -ne $veriresult ] + then + echo "FAIL: Verilog and C output do not match!" + #exit 0 + else + echo "PASS" + fi + name=$(echo $benchmark | awk -v FS="/" '{print $NF}') + echo $name","$cycles >> exec.csv +done < benchmark-list-master diff --git a/benchmarks/polybench-syn-div/script.R b/benchmarks/polybench-syn-div/script.R new file mode 100644 index 0000000..0be16da --- /dev/null +++ b/benchmarks/polybench-syn-div/script.R @@ -0,0 +1,29 @@ +library("psych") + +data = read.csv("poly.csv", header=TRUE) +leguptime = (data$legupcycles/data$legupfreqMHz) +veritime = data$vericertcycles/data$vericertfreqMHz +print(lm(veritime ~ leguptime)) +leguputil = data$leguplogicutilisation/427200*100 +veriutil = data$vericertlogicutilisation/427200*100 +print(lm (veriutil ~ leguputil)) +legupct = data$legupcomptime +verict = data$vericertcomptime +print(lm ( verict ~ legupct )) + +cycleslowdown=data$vericertcycles/data$legupcycles + +print("Cycle count slow down") +print(geometric.mean(cycleslowdown)) +print("Wall clock slow down") +print(geometric.mean(veritime/leguptime)) +print("Area overhead") +print(geometric.mean(veriutil/leguputil)) +print("Compilation time speedup") +print(geometric.mean(legupct/verict)) +print("LegUp RAM use") +print(geometric.mean(data$legupregs)) +print("Vericert RAM use") +print(geometric.mean(data$vericertregs)) +print("Area overhead") +print(geometric.mean(data$vericertregs/data$legupregs)) diff --git a/benchmarks/polybench-syn-div/setup-syn-vericert.sh b/benchmarks/polybench-syn-div/setup-syn-vericert.sh new file mode 100755 index 0000000..22356f7 --- /dev/null +++ b/benchmarks/polybench-syn-div/setup-syn-vericert.sh @@ -0,0 +1,24 @@ +#! /bin/bash + +top=$(pwd) + #set up + basedir=poly-syn + sshhost=$1 + ssh $sshhost "cd ~; rm -r $basedir" + ssh $sshhost "cd ~; mkdir $basedir" + scp quartus_synth.tcl $sshhost:$basedir + scp syn-remote.sh $sshhost:$basedir + rm syn-list + + while read benchmark ; + do + echo "Copying "$benchmark" over" + name=$(echo $benchmark | awk -v FS="/" '{print $NF}') + echo "Name: "$name + benchdir="~/$basedir/$name" + scp $benchmark.v $sshhost:~/$basedir + echo $name >> syn-list + done < benchmark-list-master + + # copy list over + scp syn-list $sshhost:$basedir diff --git a/benchmarks/polybench-syn-div/stencils/Makefile b/benchmarks/polybench-syn-div/stencils/Makefile new file mode 100644 index 0000000..d2e1c9b --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/Makefile @@ -0,0 +1,6 @@ +TARGETS := adi fdtd-2d heat-3d jacobi-1d jacobi-2d seidel-2d + +include ../common.mk + +adi.v: adi.c + $(VERICERT) $(VERICERT_OPTS) -O0 -finline $< -o $@ diff --git a/benchmarks/polybench-syn-div/stencils/adi.c b/benchmarks/polybench-syn-div/stencils/adi.c new file mode 100644 index 0000000..be2b766 --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/adi.c @@ -0,0 +1,125 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* adi.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +static +void init_array (int n, int u[ 20 + 0][20 + 0]) +{ + int i, j; + + for (i = 0; i < n; i++) + for (j = 0; j < n; j++) + { + u[i][j] = (((int)(i + n-j)) / n); + } +} + + + + +static +int print_array(int n, int u[ 20 + 0][20 + 0]) +{ + int i, j; + int res = 0; + + for (i = 0; i < n; i++) + for (j = 0; j < n; j++) { + res ^= u[i][j]; + } +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif + + return res; +} +static +void kernel_adi(int tsteps, int n, + int u[ 20 + 0][20 + 0], + int v[ 20 + 0][20 + 0], + int p[ 20 + 0][20 + 0], + int q[ 20 + 0][20 + 0]) +{ + int t, i, j; + int B1, B2; + int mul1, mul2; + int a, b, c, d, e, f; + + B1 = 2; + B2 = 1; + mul1 = ((B1 * n * n) / tsteps); + mul2 = ((B2 * n * n) /tsteps); + + a = -((mul1 / 2)); + b = 1+mul1; + c = a; + d = -((mul2 / 2)); + e = 1+mul2; + f = d; + int ZERO = 0; + + for (t=1; t<=tsteps; t++) { + + for (i=1; i<n-1; i++) { + v[ZERO][i] = 1; + p[i][ZERO] = 0; + q[i][ZERO] = v[ZERO][i]; + for (j=1; j<n-1; j++) { + p[i][j] = -(c / (a*p[i][j-1]+b)); + q[i][j] = -((-d*u[j][i-1]+(1+2*d)*u[j][i] - f*u[j][i+1]-a*q[i][j-1]) / (a*p[i][j-1]+b)); + } + + v[n-1][i] = 1; + for (j=n-2; j>=1; j--) { + v[j][i] = p[i][j] * v[j+1][i] + q[i][j]; + } + } + + for (i=1; i<n-1; i++) { + u[i][ZERO] = 1; + p[i][ZERO] = 0; + q[i][ZERO] = u[i][ZERO]; + for (j=1; j<n-1; j++) { + p[i][j] = -(f / (d*p[i][j-1]+e)); + q[i][j] = ((-a*v[i-1][j]+(1+2*a)*v[i][j] - c*v[i+1][j]-d*q[i][j-1]) / (d*p[i][j-1]+e)); + } + u[i][n-1] = 1; + for (j=n-2; j>=1; j--) { + u[i][j] = p[i][j] * u[i][j+1] + q[i][j]; + } + } + } +} + +int main() +{ + + int n = 20; + int tsteps = 20; + + + int u[20 + 0][20 + 0]; + int v[20 + 0][20 + 0]; + int p[20 + 0][20 + 0]; + int q[20 + 0][20 + 0]; + + + + init_array (n, u); + + kernel_adi (tsteps, n, u, v, p, q); + + return print_array(n, u); + +} diff --git a/benchmarks/polybench-syn-div/stencils/fdtd-2d.c b/benchmarks/polybench-syn-div/stencils/fdtd-2d.c new file mode 100644 index 0000000..2c5cdb2 --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/fdtd-2d.c @@ -0,0 +1,134 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* fdtd-2d.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int tmax, + int nx, + int ny, + int ex[ 20 + 0][30 + 0], + int ey[ 20 + 0][30 + 0], + int hz[ 20 + 0][30 + 0], + int _fict_[ 20 + 0]) +{ + int i, j; + int ONE = 1; + + for (i = 0; i < tmax; plus(i)) + _fict_[i] = (int) i; + for (i = 0; i < nx; plus(i)) + for (j = 0; j < ny; plus(j)) + { + ex[i][j] = ((i*(j+1)) / nx); + ey[i][j] = ((i*(j+2)) / ny); + hz[i][j] = ((i*(j+3)) / nx); + } + +} + + + + +static +int print_array(int nx, + int ny, + int ex[ 20 + 0][30 + 0], + int ey[ 20 + 0][30 + 0], + int hz[ 20 + 0][30 + 0]) +{ + int i, j; + int res = 0; + int ONE = 1; + + for (i = 0; i < nx; plus(i)) + for (j = 0; j < ny; plus(j)) { + res ^= ex[i][j]; + } + for (i = 0; i < nx; plus(i)) + for (j = 0; j < ny; plus(j)) { + res ^= ey[i][j]; + } + for (i = 0; i < nx; plus(i)) + for (j = 0; j < ny; plus(j)) { + res ^= hz[i][j]; + } + +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif + + return res; +} + + +static +void kernel_fdtd_2d(int tmax, + int nx, + int ny, + int ex[ 20 + 0][30 + 0], + int ey[ 20 + 0][30 + 0], + int hz[ 20 + 0][30 + 0], + int _fict_[ 20 + 0]) +{ + int t, i, j; + int ONE = 1; + + for(t = 0; t < tmax; t=t+ONE) + { + for (j = 0; j < ny; plus(j)) + ey[0][j] = _fict_[t]; + for (i = 1; i < nx; plus(i)) + for (j = 0; j < ny; plus(j)) + ey[i][j] = ey[i][j] - ((hz[i][j]-((hz[i-ONE][j])>>1))); + for (i = 0; i < nx; plus(i)) + for (j = 1; j < ny; plus(j)) + ex[i][j] = ex[i][j] - ((hz[i][j]-((hz[i][j-ONE])>>1))); + for (i = 0; i < nx - ONE; plus(i)) + for (j = 0; j < ny - ONE; plus(j)){ + int tmp = (ex[i][j+ONE] - ex[i][j] + + ey[i+ONE][j] - ey[i][j]); + hz[i][j] = hz[i][j] - (tmp >> 1) - (tmp >> 2); + } + } + +} + + +int main() +{ + + int tmax = 20; + int nx = 20; + int ny = 30; + + + int ex[20 + 0][30 + 0]; + int ey[20 + 0][30 + 0]; + int hz[20 + 0][30 + 0]; + int _fict_[20 + 0]; + + init_array (tmax, nx, ny, + ex, + ey, + hz, + _fict_); + kernel_fdtd_2d (tmax, nx, ny, + ex, + ey, + hz, + _fict_); + + return print_array(nx, ny, ex, ey, hz); +} diff --git a/benchmarks/polybench-syn-div/stencils/heat-3d.c b/benchmarks/polybench-syn-div/stencils/heat-3d.c new file mode 100644 index 0000000..f93082e --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/heat-3d.c @@ -0,0 +1,112 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* heat-3d.c: this file is part of PolyBench/C */ + +#include "../include/misc.h" + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int n, + int A[ 10 + 0][10 + 0][10 + 0], + int B[ 10 + 0][10 + 0][10 + 0]) +{ + int i, j, k; + int ONE = 1; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + for (k = 0; k < n; plus(k)) + A[i][j][k] = B[i][j][k] = (int) (i + j + (n-k))* (10 / n); +} + + + + +static +int print_array(int n, + int A[ 10 + 0][10 + 0][10 + 0]) + +{ + int i, j, k; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + for (k = 0; k < n; plus(k)) { + res ^= A[i][j][k]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_heat_3d(int tsteps, + int n, + int A[ 10 + 0][10 + 0][10 + 0], + int B[ 10 + 0][10 + 0][10 + 0]) +{ + int t, i, j, k; + int ONE = 1; + int TWO = 2; + + for (t = 1; t <= 5; plus(t)) { + for (i = 1; i < n-ONE; plus(i)) { + for (j = 1; j < n-ONE; plus(j)) { + for (k = 1; k < n-ONE; plus(k)) { + B[i][j][k] = ((A[i+ONE][j][k] - TWO * A[i][j][k] + A[i-ONE][j][k]) >> 4) + + ((A[i][j+ONE][k] - TWO * A[i][j][k] + A[i][j-ONE][k]) >> 4) + + ((A[i][j][k+ONE] - TWO * A[i][j][k] + A[i][j][k-ONE]) >> 4) + + A[i][j][k] + ; + } + } + } + for (i = 1; i < n-ONE; plus(i)) { + for (j = 1; j < n-ONE; plus(j)) { + for (k = 1; k < n-ONE; plus(k)) { + A[i][j][k] = ((B[i+ONE][j][k] - TWO * B[i][j][k] + B[i-ONE][j][k]) >> 4 ) + + ((B[i][j+ONE][k] - TWO * B[i][j][k] + B[i][j-ONE][k]) >> 4 ) + + ((B[i][j][k+ONE] - TWO * B[i][j][k] + B[i][j][k-ONE]) >> 4 ) + + B[i][j][k]; + //; + } + } + } + } +} + + +int main() +{ + + int n = 10; + int tsteps = 20; + + + int A[10 + 0][10 + 0][10 + 0]; + int B[10 + 0][10 + 0][10 + 0]; + + init_array (n, A, B); + + kernel_heat_3d (tsteps, n, A, B); + + return print_array(n, A); + +} diff --git a/benchmarks/polybench-syn-div/stencils/jacobi-1d.c b/benchmarks/polybench-syn-div/stencils/jacobi-1d.c new file mode 100644 index 0000000..993773e --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/jacobi-1d.c @@ -0,0 +1,101 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* jacobi-1d.c: this file is part of PolyBench/C */ + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int n, + int A[ 30 + 0], + int B[ 30 + 0]) +{ + int i; + int ONE = 1; + int TWO = 2; + int THREE = 3; + + for (i = 0; i < n; plus(i)) + { + A[i] = (((int) i+TWO) / n); + B[i] = (((int) i+THREE) / n); + } +} + + + + +static +int print_array(int n, + int A[ 30 + 0]) + +{ + int i; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) + { + res ^= A[i]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_jacobi_1d(int tsteps, + int n, + int A[ 30 + 0], + int B[ 30 + 0]) +{ + int t, i; + int ONE = 1; + + for (t = 0; t < tsteps; plus(t)) + { + for (i = 1; i < n - ONE; plus(i)){ + B[i] = (A[i-ONE] + A[i] + A[i + ONE]); + B[i] = B[i] >> 2; + } + for (i = 1; i < n - ONE; plus(i)){ + A[i] = (B[i-ONE] + B[i] + B[i + ONE]); + A[i] = A[i] >> 2; + } + } + +} + + +int main() +{ + + int n = 30; + int tsteps = 20; + + + int A[30 + 0]; + int B[30 + 0]; + + + + init_array (n, A, B); + + kernel_jacobi_1d(tsteps, n, A, B); + + return print_array(n, A); + +} diff --git a/benchmarks/polybench-syn-div/stencils/jacobi-2d.c b/benchmarks/polybench-syn-div/stencils/jacobi-2d.c new file mode 100644 index 0000000..bb6afec --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/jacobi-2d.c @@ -0,0 +1,108 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* jacobi-2d.c: this file is part of PolyBench/C */ + +#include "../include/misc.h" + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + + +#define plus(i) i = i + ONE +static +void init_array (int n, + int A[ 30 + 0][30 + 0], + int B[ 30 + 0][30 + 0]) +{ + int i, j; + int ONE = 1; + int TWO = 2; + int THREE = 3; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + { + A[i][j] = (((int) i*(j+TWO) + TWO) / n); + B[i][j] = (((int) i*(j+THREE) + THREE) / n); + } +} + + + + +static +int print_array(int n, + int A[ 30 + 0][30 + 0]) + +{ + int i, j; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) { + res ^= A[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_jacobi_2d(int tsteps, + int n, + int A[ 30 + 0][30 + 0], + int B[ 30 + 0][30 + 0]) +{ + int t, i, j; + int ONE = 1; + int TWO = 2; + + for (t = 0; t < tsteps; plus(t)) + { + for (i = 1; i < n - ONE; plus(i)) + for (j = 1; j < n - ONE; plus(j)){ + B[i][j] = (A[i][j] + A[i][j-ONE] + A[i][ONE+j] + A[ONE+i][j] + A[i-ONE][j]); + B[i][j] = B[i][j] >> TWO; + } + for (i = 1; i < n - ONE; plus(i)) + for (j = 1; j < n - ONE; plus(j)){ + A[i][j] = (B[i][j] + B[i][j-ONE] + B[i][ONE+j] + B[ONE+i][j] + B[i-ONE][j]); + A[i][j] = A[i][j] >> TWO; + } + } + +} + + +int main() +{ + + int n = 30; + int tsteps = 5; + + + int A[30 + 0][30 + 0]; + int B[30 + 0][30 + 0]; + + + + init_array (n, A, B); + + kernel_jacobi_2d(tsteps, n, A, B); + + return print_array(n, A); + +} diff --git a/benchmarks/polybench-syn-div/stencils/seidel-2d.c b/benchmarks/polybench-syn-div/stencils/seidel-2d.c new file mode 100644 index 0000000..4a3b1ac --- /dev/null +++ b/benchmarks/polybench-syn-div/stencils/seidel-2d.c @@ -0,0 +1,92 @@ +/** + * This version is stamped on May 10, 2016 + * + * Contact: + * Louis-Noel Pouchet <pouchet.ohio-state.edu> + * Tomofumi Yuki <tomofumi.yuki.fr> + * + * Web address: http://polybench.sourceforge.net + */ +/* seidel-2d.c: this file is part of PolyBench/C */ + +#include "../include/misc.h" + +#ifndef SYNTHESIS +#include <stdio.h> +#endif + +#define plus(i) i = i + ONE +static +void init_array (int n, + int A[ 40 + 0][40 + 0]) +{ + int i, j; + int ONE = 1; + int TWO = 2; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) + A[i][j] = (((int) i*(j+TWO) + TWO) / n); +} + + + + +static +int print_array(int n, + int A[ 40 + 0][40 + 0]) + +{ + int i, j; + int ONE = 1; + int res = 0; + + for (i = 0; i < n; plus(i)) + for (j = 0; j < n; plus(j)) { + res ^= A[i][j]; + } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; +} + + + + +static +void kernel_seidel_2d(int tsteps, + int n, + int A[ 40 + 0][40 + 0]) +{ + int t, i, j; + int ONE = 1; + int TWO = 2; + int NINE = 9; + + for (t = 0; t <= tsteps - ONE; plus(t)) + for (i = ONE; i<= n - TWO; plus(i)) + for (j = ONE; j <= n - TWO; plus(j)) + A[i][j] = ((A[i-ONE][j-ONE] + A[i-ONE][j] + A[i-ONE][j+ONE] + + A[i][j-ONE] + A[i][j] + A[i][j+ONE] + + A[i+ONE][j-ONE] + A[i+ONE][j] + A[i+ONE][j+ONE]) / NINE); + +} + + +int main() +{ + + int n = 40; + int tsteps = 5; + + + int A[40 + 0][40 + 0]; + + init_array (n, A); + + kernel_seidel_2d (tsteps, n, A); + + return print_array(n, A); + +} diff --git a/benchmarks/polybench-syn-div/syn-remote.sh b/benchmarks/polybench-syn-div/syn-remote.sh new file mode 100755 index 0000000..879db2e --- /dev/null +++ b/benchmarks/polybench-syn-div/syn-remote.sh @@ -0,0 +1,51 @@ +#! /bin/bash + +#setup +while read benchmark ; +do +echo "Setting up "$benchmark +rm -r $benchmark +mkdir $benchmark +cp $benchmark.v $benchmark/top.v + +done < syn-list + +#synthesis + +count=0 +while read benchmark ; + +do +echo "Synthesising "$benchmark +cd $benchmark +quartus_sh -t ../quartus_synth.tcl & +let "count=count+1" +cd .. + +if [ $count -eq 4 ] +then +echo "I am here" +wait +count=0 +fi + +done < syn-list + +if [ $count -lt 4 ] +then +wait +fi + +#extract +while read benchmark ; do + cd $benchmark + echo $(pwd) + freq=$(grep MHz syn.sta.rpt | tail -2 | head -1 | awk '{print $2}') + lut=$(sed -n -e 8p syn.fit.summary | awk '{print $6}' | sed 's/,//g') + regs=$(sed -n -e 9p syn.fit.summary | awk '{print $4}') + bram=$(sed -n -e 13p syn.fit.summary | awk '{print $5}') + dsp=$(sed -n -e 14p syn.fit.summary | awk '{print $5}') + cd .. + echo $benchmark","$freq","$lut","$regs","$bram","$dsp >> results +done < syn-list + diff --git a/benchmarks/polybench-syn/Makefile b/benchmarks/polybench-syn/Makefile new file mode 100644 index 0000000..2c20246 --- /dev/null +++ b/benchmarks/polybench-syn/Makefile @@ -0,0 +1,15 @@ +all: + $(MAKE) -C stencils + $(MAKE) -C medley + $(MAKE) -C linear-algebra/blas + $(MAKE) -C linear-algebra/kernels + $(MAKE) -C linear-algebra/solvers + $(MAKE) -C data-mining + +clean: + $(MAKE) clean -C stencils + $(MAKE) clean -C medley + $(MAKE) clean -C linear-algebra/blas + $(MAKE) clean -C linear-algebra/kernels + $(MAKE) clean -C linear-algebra/solvers + $(MAKE) clean -C data-mining diff --git a/benchmarks/polybench-syn/common.mk b/benchmarks/polybench-syn/common.mk new file mode 100644 index 0000000..fbada0b --- /dev/null +++ b/benchmarks/polybench-syn/common.mk @@ -0,0 +1,33 @@ +VERICERT ?= vericert +VERICERT_OPTS ?= -DSYNTHESIS + +IVERILOG ?= iverilog +IVERILOG_OPTS ?= + +TARGETS ?= + +%.v: %.c + $(VERICERT) $(VERICERT_OPTS) $< -o $@ + +%.iver: %.v + $(IVERILOG) -o $@ $(IVERILOG_OPTS) $< + +%.gcc: %.c + $(CC) $(CFLAGS) $< -o $@ + +%: %.iver %.gcc + cp $< $@ + +all: $(TARGETS) + +clean: + rm -f *.iver + rm -f *.v + rm -f *.gcc + rm -f *.clog + rm -f *.tmp + rm -f $(TARGETS) + +.PRECIOUS: %.v %.gcc %.iver +.PHONY: all clean +.SUFFIXES: diff --git a/benchmarks/polybench-syn/data-mining/Makefile b/benchmarks/polybench-syn/data-mining/Makefile new file mode 100644 index 0000000..d4817a0 --- /dev/null +++ b/benchmarks/polybench-syn/data-mining/Makefile @@ -0,0 +1,3 @@ +TARGETS := covariance + +include ../common.mk diff --git a/benchmarks/polybench-syn/linear-algebra/blas/Makefile b/benchmarks/polybench-syn/linear-algebra/blas/Makefile new file mode 100644 index 0000000..e1f3b58 --- /dev/null +++ b/benchmarks/polybench-syn/linear-algebra/blas/Makefile @@ -0,0 +1,3 @@ +TARGETS := gemm gemver gesummv symm syr2k syrk trmm + +include ../../common.mk diff --git a/benchmarks/polybench-syn/linear-algebra/blas/trmm.preproc.c b/benchmarks/polybench-syn/linear-algebra/blas/trmm.preproc.c deleted file mode 100644 index 9b8edfe..0000000 --- a/benchmarks/polybench-syn/linear-algebra/blas/trmm.preproc.c +++ /dev/null @@ -1,144 +0,0 @@ -/** - * This version is stamped on May 10, 2016 - * - * Contact: - * Louis-Noel Pouchet <pouchet.ohio-state.edu> - * Tomofumi Yuki <tomofumi.yuki.fr> - * - * Web address: http://polybench.sourceforge.net - */ -/* trmm.c: this file is part of PolyBench/C */ - -#include <stdio.h> -#include <unistd.h> -#include <string.h> -#include <math.h> - -/* Include polybench common header. */ -#include<polybench.h> -# 1 "trmm.c" -# 1 "<built-in>" 1 -# 1 "<built-in>" 3 -# 362 "<built-in>" 3 -# 1 "<command line>" 1 -# 1 "<built-in>" 2 -# 1 "trmm.c" 2 -# 1 "utilities/polybench.h" 1 -# 30 "utilities/polybench.h" -# 1 "/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/stdlib.h" 1 3 4 -# 31 "utilities/polybench.h" 2 -# 231 "utilities/polybench.h" -extern void* polybench_alloc_data(unsigned long long int n, int elt_size); -extern void polybench_free_data(void* ptr); - - - - -extern void polybench_flush_cache(); -extern void polybench_prepare_instruments(); -# 2 "trmm.c" 2 - - -# 1 "./linear-algebra/blas/trmm/trmm.h" 1 -# 5 "trmm.c" 2 - - - -static -void init_array(int m, int n, - int *alpha, - int A[ 20 + 0][20 + 0], - int B[ 20 + 0][30 + 0]) -{ - int i, j; - - *alpha = 1.5; - for (i = 0; i < m; i++) { - for (j = 0; j < i; j++) { - A[i][j] = (int)((i+j) % m)/m; - } - A[i][i] = 1.0; - for (j = 0; j < n; j++) { - B[i][j] = (int)((n+(i-j)) % n)/n; - } - } - -} - - - - -static -void print_array(int m, int n, - int B[ 20 + 0][30 + 0]) -{ - int i, j; - - fprintf(stderr, "==BEGIN DUMP_ARRAYS==\n"); - fprintf(stderr, "begin dump: %s", "B"); - for (i = 0; i < m; i++) - for (j = 0; j < n; j++) { - if ((i * m + j) % 20 == 0) fprintf (stderr, "\n"); - fprintf (stderr, "%d ", B[i][j]); - } - fprintf(stderr, "\nend dump: %s\n", "B"); - fprintf(stderr, "==END DUMP_ARRAYS==\n"); -} - - - - -static -void kernel_trmm(int m, int n, - int alpha, - int A[ 20 + 0][20 + 0], - int B[ 20 + 0][30 + 0]) -{ - int i, j, k; -# 68 "trmm.c" -#pragma scop - for (i = 0; i < m; i++) - for (j = 0; j < n; j++) { - for (k = i+1; k < m; k++) - B[i][j] += A[k][i] * B[k][j]; - B[i][j] = alpha * B[i][j]; - } -#pragma endscop - -} - - -int main(int argc, char** argv) -{ - - int m = 20; - int n = 30; - - - int alpha; - int (*A)[20 + 0][20 + 0]; A = (int(*)[20 + 0][20 + 0])polybench_alloc_data ((20 + 0) * (20 + 0), sizeof(int));; - int (*B)[20 + 0][30 + 0]; B = (int(*)[20 + 0][30 + 0])polybench_alloc_data ((20 + 0) * (30 + 0), sizeof(int));; - - - init_array (m, n, &alpha, *A, *B); - - - ; - - - kernel_trmm (m, n, alpha, *A, *B); - - - ; - ; - - - - if (argc > 42 && ! strcmp(argv[0], "")) print_array(m, n, *B); - - - free((void*)A);; - free((void*)B);; - - return 0; -} diff --git a/benchmarks/polybench-syn/linear-algebra/kernels/Makefile b/benchmarks/polybench-syn/linear-algebra/kernels/Makefile new file mode 100644 index 0000000..4b7f6e1 --- /dev/null +++ b/benchmarks/polybench-syn/linear-algebra/kernels/Makefile @@ -0,0 +1,3 @@ +TARGETS := 2mm 3mm atas bicg doitgen mvt + +include ../../common.mk diff --git a/benchmarks/polybench-syn/linear-algebra/solvers/Makefile b/benchmarks/polybench-syn/linear-algebra/solvers/Makefile new file mode 100644 index 0000000..146620b --- /dev/null +++ b/benchmarks/polybench-syn/linear-algebra/solvers/Makefile @@ -0,0 +1,3 @@ +TARGETS := cholesky durbin lu ludcmp trisolv + +include ../../common.mk diff --git a/benchmarks/polybench-syn/medley/Makefile b/benchmarks/polybench-syn/medley/Makefile new file mode 100644 index 0000000..816a0ce --- /dev/null +++ b/benchmarks/polybench-syn/medley/Makefile @@ -0,0 +1,3 @@ +TARGETS := floyd-warshall nussinov + +include ../common.mk diff --git a/benchmarks/polybench-syn/run-vericert.sh b/benchmarks/polybench-syn/run-vericert.sh index 2f8097f..6cf4cd9 100755 --- a/benchmarks/polybench-syn/run-vericert.sh +++ b/benchmarks/polybench-syn/run-vericert.sh @@ -1,20 +1,18 @@ -#! /bin/bash +#!/usr/bin/env bash + +rm exec.csv top=$(pwd) #set up while read benchmark ; do echo "Running "$benchmark - clang -Wall -Werror -fsanitize=undefined $benchmark.c -o $benchmark.o - ./$benchmark.o > $benchmark.clog + ./$benchmark.gcc > $benchmark.clog cresult=$(cat $benchmark.clog | cut -d' ' -f2) echo "C output: "$cresult - { time ../../bin/vericert -DSYNTHESIS -finline -fschedule --debug-hls $benchmark.c -o $benchmark.v ; } 2> $benchmark.comp - iverilog -o $benchmark.iver -- $benchmark.v ./$benchmark.iver > $benchmark.tmp veriresult=$(tail -1 $benchmark.tmp | cut -d' ' -f2) cycles=$(tail -2 $benchmark.tmp | head -1 | tr -s ' ' | cut -d' ' -f2) - ctime=$(cat $benchmark.comp | head -2 | tail -1 | xargs | cut -d' ' -f2 | cut -d'm' -f2 | sed 's/s//g') - echo "Veri output: "$veriresult + echo "Verilog output: "$veriresult #Undefined checks if test -z $veriresult @@ -39,5 +37,5 @@ while read benchmark ; do echo "PASS" fi name=$(echo $benchmark | awk -v FS="/" '{print $NF}') - echo $name","$cycles","$ctime >> exec.csv + echo $name","$cycles >> exec.csv done < benchmark-list-master diff --git a/benchmarks/polybench-syn/stencils/Makefile b/benchmarks/polybench-syn/stencils/Makefile new file mode 100644 index 0000000..d2e1c9b --- /dev/null +++ b/benchmarks/polybench-syn/stencils/Makefile @@ -0,0 +1,6 @@ +TARGETS := adi fdtd-2d heat-3d jacobi-1d jacobi-2d seidel-2d + +include ../common.mk + +adi.v: adi.c + $(VERICERT) $(VERICERT_OPTS) -O0 -finline $< -o $@ diff --git a/benchmarks/polybench-syn/stencils/adi.c b/benchmarks/polybench-syn/stencils/adi.c index ec2bf2a..2f4aca3 100644 --- a/benchmarks/polybench-syn/stencils/adi.c +++ b/benchmarks/polybench-syn/stencils/adi.c @@ -15,28 +15,23 @@ #include <stdio.h> #endif -#define plus(i) i = i + ONE - static -void init_array (int n, - int u[ 20 + 0][20 + 0]) +void init_array (int n, int u[ 20 + 0][20 + 0]) { int i, j; for (i = 0; i < n; i++) for (j = 0; j < n; j++) - { - u[i][j] = divider((int)(i + n-j) ,n); - } + { + u[i][j] = divider((int)(i + n-j), n); + } } static -int print_array(int n, - int u[ 20 + 0][20 + 0]) - +int print_array(int n, int u[ 20 + 0][20 + 0]) { int i, j; int res = 0; @@ -53,10 +48,10 @@ int print_array(int n, } static void kernel_adi(int tsteps, int n, - int u[ 20 + 0][20 + 0], - int v[ 20 + 0][20 + 0], - int p[ 20 + 0][20 + 0], - int q[ 20 + 0][20 + 0]) + int u[ 20 + 0][20 + 0], + int v[ 20 + 0][20 + 0], + int p[ 20 + 0][20 + 0], + int q[ 20 + 0][20 + 0]) { int t, i, j; int B1, B2; diff --git a/default.nix b/default.nix index 8308389..1121469 100644 --- a/default.nix +++ b/default.nix @@ -1,35 +1,15 @@ -with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/269fc4ddb896c1c5994eb4bb8c750ec18cb3db82.tar.gz") {}; +with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/8dd8bd8be74879f9f7919b16a4cb5ab2a75f18e5.tar.gz") {}; let - ncoq = coq_8_12; - ncoqPackages = coqPackages_8_12; - bbv = ncoqPackages.callPackage - ( { coq, stdenv, fetchFromGitHub }: - stdenv.mkDerivation { - name = "coq${coq.coq-version}-bbv"; - - src = fetchFromGitHub { - owner = "mit-plv"; - repo = "bbv"; - rev = "5099237c52d2910f79a1a3ca9ae4dfa80129bf86"; - sha256 = "0qnha333h7dc8105prdxvmkgy6l8swvyf6kz9v5s5dk4dvr5nra8"; - }; - - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 ]; - propagatedBuildInputs = [ coq ]; - enableParallelBuilding = true; - - installPhase = '' - make -f Makefile.coq.all install COQLIB='$(out)/lib/coq/${coq.coq-version}/' - ''; - } ) { }; + ncoq = coq_8_13; + ncoqPackages = coqPackages_8_13; in stdenv.mkDerivation { name = "vericert"; src = ./.; buildInputs = [ ncoq dune_2 gcc - ocaml ocamlPackages.findlib ocamlPackages.menhir - ocamlPackages.ocamlgraph + ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir + ncoq.ocamlPackages.ocamlgraph ]; enableParallelBuilding = true; diff --git a/docs b/docs -Subproject a596c0c469d7c61b5ed8dfaf8805a926024a3a7 +Subproject 5508c21e064276aa4d5146b3af5b6f6e9a4c236 diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index 0706d79..1ea580f 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -65,7 +65,6 @@ let compile_c_file sourcename ifile ofile = set_dest Vericert.PrintClight.destination option_dclight ".light.c"; set_dest Vericert.PrintCminor.destination option_dcminor ".cm"; set_dest Vericert.PrintRTL.destination option_drtl ".rtl"; - set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock"; set_dest Vericert.PrintHTL.destination option_dhtl ".htl"; set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest Vericert.PrintLTL.destination option_dltl ".ltl"; @@ -93,7 +92,7 @@ let compile_c_file sourcename ifile ofile = end else begin let verilog = let translation = if !option_hls_schedule - then Vericert.Compiler0.transf_hls_temp + then Vericert.Compiler0.transf_hls else Vericert.Compiler0.transf_hls in match translation csyntax with diff --git a/ip/altera.v b/ip/altera.v new file mode 100644 index 0000000..3839cbe --- /dev/null +++ b/ip/altera.v @@ -0,0 +1,2 @@ +module ALTERA_MF_MEMORY_INITIALIZATION; +endmodule diff --git a/lib/CompCert b/lib/CompCert -Subproject 48a9dcbdc968bcf05b4eec17b8c7fd471fb8024 +Subproject 1daf96cdca4d828c333cea5c9a314ef86134298 diff --git a/scripts/convert.sh b/scripts/convert.sh new file mode 100755 index 0000000..c2ef311 --- /dev/null +++ b/scripts/convert.sh @@ -0,0 +1,14 @@ +file=$1 +benchmark=$(echo $1 | sed 's:.*/\([^/]\+\)/encode_report.xml:\1:') + +lut_flip_flop=$(sed -n "s/.*XILINX_LUT_FLIP_FLOP_PAIRS_USED.*\"\([0-9.]*\)\".*/\1/p" $file) +slice=$(sed -n "s/.*XILINX_SLICE\".*\"\([0-9.]*\)\".*/\1/p" $file) +regs=$(sed -n "s/.*XILINX_SLICE_REGISTERS.*\"\([0-9.]*\)\".*/\1/p" $file) +luts=$(sed -n "s/.*XILINX_SLICE_LUTS.*\"\([0-9.]*\)\".*/\1/p" $file) +ramfifo=$(sed -n "s/.*XILINX_BLOCK_RAMFIFO.*\"\([0-9.]*\)\".*/\1/p" $file) +iopin=$(sed -n "s/.*XILINX_IOPIN.*\"\([0-9.]*\)\".*/\1/p" $file) +dsps=$(sed -n "s/.*XILINX_DSPS.*\"\([0-9.]*\)\".*/\1/p" $file) +power=$(sed -n "s/.*XILINX_POWER.*\"\([0-9.]*\)\".*/\1/p" $file) +delay=$(sed -n "s/.*XILINX_DESIGN_DELAY.*\"\([0-9.]*\)\".*/\1/p" $file) + +echo $benchmark,$lut_flip_flop,$slice,$regs,$luts,$ramfifo,$iopin,$dsps,$power,$delay >>synth.csv diff --git a/scripts/docker/Dockerfile b/scripts/docker/Dockerfile new file mode 100644 index 0000000..c66df6d --- /dev/null +++ b/scripts/docker/Dockerfile @@ -0,0 +1,19 @@ +FROM nixos/nix + +RUN nix-channel --add https://nixos.org/channels/nixpkgs-unstable nixpkgs +RUN nix-channel --update + +RUN nix-env -i yosys git tmux vim gcc iverilog + +ADD legup_polybench_syn.tar.gz /data/legup-polybench-syn +ADD legup_polybench_syn_div.tar.gz /data/legup-polybench-syn-div +ADD data.tar.gz /data + +RUN git clone --recursive https://github.com/ymherklotz/vericert + +WORKDIR /vericert +RUN git checkout oopsla21 +RUN nix-shell --run "make -j7" +RUN nix-shell --run "make install" + +RUN echo "export PATH=/vericert/bin:$PATH" >>/root/.bashrc diff --git a/scripts/docker/artifact.org b/scripts/docker/artifact.org new file mode 100644 index 0000000..fa0a936 --- /dev/null +++ b/scripts/docker/artifact.org @@ -0,0 +1,333 @@ +#+title: Vericert OOPSLA 2021 Artifact +#+options: toc:nil num:nil author:nil date:nil +#+latex_class: scrartcl + +This artifact should support the claims made in the paper "Formal Verification of High-Level Synthesis". In the paper, our tool Vericert was referred to as using the temporary name "HLSCert". The claims that can be verified by the paper are the following: + +- The mechanised proof of correctness of the translation from C into Verilog is provided and can be checked and rerun. +- All 27 PolyBench benchmarks can be recompiled using Vericert. +- The cycle counts of Vericert on the benchmarks can be checked and compared against LegUp 4.0. +- If Vivado is downloaded separately, then the whole performance section can be checked, including all the graphs that appear in the paper. + +** Artifact availability + +The artifact is available on Github, specifically on the ~oopsla21~ branch: + +https://github.com/ymherklotz/vericert + +#+latex: \noindent +This release is also archived on Zenodo permanently: + +http://doi.org/10.5281/zenodo.5093839 + +#+latex: \noindent +However, for the purposes of this artifact review, a Docker image has been set up: + +https://hub.docker.com/repository/docker/ymherklotz/vericert + +** Claims that are not supported by the artifact + +Unfortunately, we could not include our version of LegUp 4.0 in the artifact due to license restrictions. In addition to that, LegUp was recently bought by Microchip and renamed to SmartHLS[fn:1], which means that the most recent versions of LegUp are closed source and cannot be downloaded anymore. The original open source version of LegUp 4.0 is not currently available either at the moment. The LegUp team have advised us that this is due to server issues in Toronto.[fn:2] We have not heard back from them about whether it is ok for us to share our copy of LegUp 4.0 for artifact evaluation purposes, so we have not done so. + +Instead, we have included the net lists that LegUp generated from the benchmarks in the artifact, with all the optimisation levels that were tried, however, it does mean that these cannot be verified again and that other optimisation options cannot be tried. + +In addition to that, the Vivado synthesis tool by Xilinx[fn:3] is also commercial (but free to download), and therefore cannot be bundled into the artifact either. This synthesis tool was used to get accurate timing information about how the design would run on an FPGA, and also give the area that the design would take up on the FPGA. To be able to reproduce these results, it would therefore need Vivado to be set up so that the scripts can run. + +* Kick the tyres + +First, the docker image needs to be downloaded and run, which contains the git repository: + +#+begin_src shell +docker pull ymherklotz/vericert:1.0 +docker run -it ymherklotz/vericert:1.0 sh +#+end_src + +Then, one just has to go into the directory which contains the git repository (~/vericert~) and open a ~nix-shell~, which will load a shell with all the correct dependencies loaded: + +#+begin_src shell +cd /vericert +nix-shell +#+end_src + +Then, all commands can be run in this shell, as well as ~vericert~, which has already been compiled and can be found in the ~/vericert/bin~ directory. For a quick test that it is working, a few very simple examples in the ~/vericert/test~ directory can be run by using the following inside of the ~/vericert~ directory: + +#+begin_src shell +cd /vericert +make test +#+end_src + +If this finishes without errors, it means that Vericert is working correctly. + +Finally, to check that the benchmarks work correctly as well, we can quickly compile and run one as well: + +#+begin_src shell +cd /vericert/benchmarks/polybench-syn +make +./stencils/jacobi-1d +#+end_src + +This simulates the hardware design generated for the jacobi-1d benchmark in PolyBench/C, and should print the return value: 1, as well as the cycle count: 19996 as follows: + +#+begin_src shell +cycles: 19996 +finished: 1 +#+end_src + +* Step-by-Step instructions + +This section describes the detailed instructions to get the results for the different sections of the paper, first describing the structure of the proof and how to execute Vericert manually, to finally running Vericert on the benchmarks and get the cycle counts for the Vericert designs as well as the precompiled LegUp designs. + +** Directory structure of Vericert + +The main directory structure of Vericert is the following: + +- ~/src~ :: Contains all the Coq and OCaml source files used for Vericert. The whole proof of correctness is therefore in this directory. +- ~/lib~ :: This directory contains CompCert, on which Vericert is built upon. Vericert tries to separate CompCert and uses it only as a library, redefining a different top-level. +- ~/benchmarks~ :: Contains the PolyBench/C benchmarks used as an evaluation in the paper, which are stored under ~polybench-syn~ for the benchmarks without dividers, and ~polybench-syn-div~ for the benchmarks with dividers. +- ~/docs~ :: Contains a website and an ~org-mode~ file with some light documentation of the tool. +- ~/example~ :: Contains some interesting observations that were made during the development, which are not directly relevant to Vericert. +- ~/include~ :: Contains the divider implementation which can be imported and used in C files to get the better performance out of Vericert, instead of using native division. +- ~/ip~ :: Contains hardware divider implementations which will be used in the future instead of the software implementation that is currently used in ~/include~. +- ~/scripts~ :: Contains some miscellaneous scripts and the ~Dockerfile~ which has been added for this artifcat. +- ~/test~ :: Contains some very light test cases which are some minimal examples for working constructs. + +** Description of the proof + +The proof is mostly located in ~/src/hls~, which contains the proof of correctness of the 3AC to HTL transformation, as well as the transformation from HTL to Verilog. First, we will describe where each section of the paper is implemented, then a description of all the files in the src directory will be included. + +*** Implementation of paper sections + +When mentioning Coq source files, they will always be relative to the ~/vericert/src~ directory in the docker image. + +**** Section 2 + +- Figure 2 :: This example is not included in the repository or docker image, however, if the small C example in Figure 2a is copied into a file ~main.v~, it can be compiled using the following: + +#+begin_src shell +vericert -o main.v -O0 -drtl -dhtl main.c +#+end_src + +Where ~-O0~ means it will not apply any CompCert optimisations, ~-drtl~ means it will print the internal 3AC (also known as RTL) representation and ~-dhtl~ outputs the HTL representation. After running that command, Figure 2b should be the exact same as the ~main.rtl.7~ file that was generated, and Figure 2c should be the same as ~main.v~, with some slight modifications to some variable names and formatting. + +- Figure 3 :: After running the above command, Figure 3 will be a visual representation of ~main. + +- Section 2.2.2 :: The abstract RAM description and is used in HTL can be found in ~hls/HTL.v:139~. This also corresponds to Figure 7. This abstract description is then implemented as a concrete Verilog implementation shown in ~hls/Veriloggen.v:45~. The proof that the Verilog implementation is correct according to the HTL specification of it can be found in Lemma ~ram_exec_match~, ~hls/Veriloggenproof.v:284~. + +- Section 2.2.3 :: This proof is for Theorem ~shrx_shrx_alt_equiv~, ~common/Integer~\-~Extra.v:661~. + +**** Section 3 + +This Section is mainly implemented in ~hls/Verilog.v~. + +- Module execution rule :: The updated negative edge execution rule can be found in ~hls/Verilog.v:582~ which is called ~step_module~, and has a ~mis_stepp~ and ~mis_stepp_negedge~ for the steps of the positive and negative edge triggered always blocks. + +- Figure 5 :: This is implemented as all the other possible steps in one Verilog step, shown in ~hls/Verilog.v:581~. The Figure just uses some nicer notation for the inference rules. + +- Figure 6 :: Our dependenty typed arrays used for the memory model are implemented in ~hls/Array.v~, and is then integrated in the Verilog semantics properly using the ~arr_associations~ type, defined in ~hls/Verilog.v:60~, which is a blocking and nonblocking array where each element is an optional, as shown in Figure 6. + +**** Section 5 + +- Theorem 1 :: This is proven as Theorem ~transf_c_program_correct~ in ~Compiler.v~\-~:415~. + +- Lemma 1 :: This is proven as part of Theorem ~cstrategy_semantic_preservation~ in ~Compiler.v:334~, which also proves the backward simulation at the same time. + +- Lemma 2 :: The specification of the translation from 3AC to HTL is shown in Theorem ~transl_module_correct~ in ~hls/HTLgenspec.v:608~ and is called ~tr_module~ instead of ~spec_htl~ as in the paper, and ~tr_htl~ is called ~transl_~\-~module~ instead. + +- Section 4.1.2, ~match_states~ :: The ~match_states~ property to match two states in 3AC and HTL up is defined in ~hls/HTLgenproof.v:112~. + +- Lemma 3 :: Proven as Theorem ~transl_step_correct~ in ~hls/HTLgenproof.v:2856~ and describes the simulation diagram shown in the paper. + +- Section 4.2.1 :: The specification of the store is located in ~hls/Memorygen.v:2096~ and is called ~alt_store~. + +- Section 4.2.2, ~match_states~ :: The definition of matching states is defined in ~hls~\-~/Memory~\-~gen.v:314~, where ~ARRS_SIZE~ corresponds to the property of equally sized arrays at each step and ~DISABLE_RAM~ corresponds to the property that the RAM is always disabled by default. + +- Lemma 4 :: There is a small typo in the paper, and this Lemma should describe the forward simulation of the insertion of the RAM. This is proven in Theorem ~transf_program_correct~ in ~hls/Memorygen.v:3196~, and the simulation diagram for this translation is proven in Theorem ~transf_step_correct~ in ~hls/Memorygen.v:3000~. + +- Lemma 5 :: This is proven in Theorem ~transf_program_correct~ in ~hls/Veriloggen~\-~proof.v:537~. The assumption that the HTL module and Verilog module are related by ~transl_program~ (~tr_verilog~ in the paper) is given in the hypothesis ~TRANSL~ in ~hls/Veriloggenproof.v:343~. + +- Lemma 6 :: The determinism of the Verilog semantics is proven in ~semantics_deter~\-~minate~ in ~hls/Verilog.v:810~. + +- Table 1 :: These values were calculated by hand to separate specification, implementation and proof code. The raw results can be found in the last table in the ~/data/data/results.org~ file, or in the ~/data/data/code-count.csv~. + +*** Description of files + +- ~/src/Compiler.v~ :: The very top-level of the proof is located here and it contains the main proof of the compiler, which is the proof that the ~transf_hls~ function is correct, which takes C and outputs Verilog. The main proof of correctness is in the Theorem called ~transf_c_program_correct~, which says that if the ~transf_hls~ function succeeded, that the backward simulation should hold between C and Verilog. +- ~/src/common~ :: This directory contains some common library extensions and proofs that are used in other parts of Vericert. This includes the proof of correctness of Section 2.2.3, which is located in ~/src/common/IntegerExtra.v~ under the Theorem ~shrx_shrx_alt_equiv~. +- ~/src/hls/Verilog.v~ :: This file contains the whole Verilog semantics, together with the proof that the Verilog semantics are deterministic. This implements Section 3 from the paper. +- ~src/hls/Veriloggen.v~ :: This file contains the generation of Verilog from HTL. +- ~src/hls/Veriloggenproof.v~ :: This file contains the correctness proof of the generation of Verilog from HTL. +- ~/src/hls/HTL.v~ :: This file contains the definition of the HTL intermediate language, together with its semantics. +- ~/src/hls/HTLgen.v~ :: This file contains the generation of HTL from 3AC, which is the first step in the HLS transformation. +- ~/src/hls/HTLgenspec.v~ :: This file contains the high-level specification of the translation from 3AC into HTL, together with a proof of correctness of the specification. +- ~/src/hls/HTLgenproof.v~ :: This file contains the proof of correctness of the HTL generation from 3AC, where the main parts of the proof are the generation of Verilog operations, as well as the change in the memory model (load and store instructions). +- ~/src/hls/Memorygen.v~ :: This file contains the definition and proof of the transformation which replaces naïve loads and stores into a proper RAM, which is described in Section 2.2.2. +- ~/src/hls/ValueInt.v~ :: Contains our definition of values that are used in the Verilog semantics, and differ from the values used by CompCert, as they don't have a pointer type anymore. +- ~/src/hls/Array.v~ :: Contains our definition of the memory model, which is a dependently typed array, which encodes its length. This is much more concrete than CompCert's abstract memory model, and closer to how it is actually modelled in hardware. +- ~/src/hls/AssocMap.v~ :: Definition of association maps, which is the type that is used for $\Gamma$ and $\Delta$ in Section 3. + +** How to manually compile using Vericert + +To compile arbitrary C files, the following command can be used: + +#+begin_src shell +vericert main.c -o main.v +#+end_src + +Which will generate a Verilog file with a corresponding test bench. The Verilog file can then be simulated by using the Icarus Verilog simulator: + +#+begin_src shell +iverilog main.v -o main +./main +#+end_src + +This should print out the return value from the main function in addition to the number of cycles that it took to execute the hardware design. + +** Getting cycle counts for Vericert + +There are two benchmark sets for which the results are given in the paper: + +- ~/vericert/benchmarks/polybench-syn~ :: Contains the PolyBench/C benchmark without any dividers, and instead the dividers are replaced by calls to ~sdivider~ and ~smodulo~ in ~/vericert/include/hls.h~. +- ~/vericert/benchmarks/polybench-syn-div~ :: Contains the PolyBench/C benchmark with dividers. + +To get the cycle counts for Vericert from the benchmarks, the benchmarks can be compiled using the following: + +#+begin_src shell +cd /vericert/benchmarks/polybench-syn +#+end_src + +or + +#+begin_src shell +cd /vericert/benchmarks/polybench-syn-div +#+end_src + +depending on which benchmark should be run, and then running: + +#+begin_src shell +make +#+end_src + +This will generate all the binaries for the simulation and execution of the C code. The cycle counts of the hardware can then be gotten by running: + +#+begin_src shell +./run-vericert.sh +#+end_src + +This can take a while to complete, as simulation of hardware is quite slow. After around 30 minutes, there should be a ~exec.csv~ file which contains the cycle counts for each of the 27 benchmarks. + +** Getting the cycle counts for LegUp + +Unfortunately, the benchmarks cannot be compiled from C to Verilog using LegUp, as it could not be included in the artifact, and does not seem to be freely available anymore. + +However, our compiled Verilog designs from LegUp have been included for all the optimisation options that were tested for in the paper in Section 5. + +To get the cycle counts, it suffices to go into an arbitrary directory, and run the following script, where the command line arguments select which set of cycle counts to generate: + +#+begin_src shell +/vericert/scripts/run-legup.sh [syn|syn-div] \ + [opt|no_opt|no_chain|no_opt_no_chain] +#+end_src + +For example, to run the LegUp benchmarks with no LLVM optimisations and no operation chaining, on the PolyBench/C benchmark with no dividers, one can run the following command: + +#+begin_src shell +/vericert/scripts/run-legup.sh syn no_opt_no_chain +#+end_src + +This will take some 30 minutes to run as well, and will generate an ~exec_legup.csv~ file, with the name of the benchmark and it's cycle count. + +** Comparing the results + +To compare the results to the results presented in the paper, the main comparison that is supported by this artifact is to compare the cycle counts to the ones used to generate the graphs in the evaluation section of the paper. + +The ~/data/data~ directory contains all the raw data which was used to generate the graphs in Section 5. This data can therefore be used to examine the cycle counts used to draw the graphs. This raw data can be examined better in ~/data/data/results.org~, which includes the tables in a nicer format. + +The ~legup-*~ csv files contain the raw size, timing and cycle count for the various LegUp configurations on the different benchmarks. ~vericert-*~ is the equivalent but for Vericert. Then, to draw the graphs, the actual csv files that are used are: + +- ~rel-size-*~ :: This contains the relative size of each run (denoted by slice in the csv files) compared to fully optimised LegUp. This is obtained by taking the slice value of the tool being considered (LegUp with some optimisation turned off, or Vericert), and dividing that by the number of slices present in fully optimised LegUp. + +\[\frac{\text{slice}_t}{\text{slice}_{\text{legup\_opt}}}\] + +- ~rel-time-*~ :: This performs the same computation as for the size comparison, comparing to LegUp with all optimisations turned on, but instead compares the following values: cycles $\times$ delay: + +\[\frac{\text{cycles}_t \times \text{delay}_t}{\text{cycles}_{\text{legup\_opt}} \times \text{delay}_{\text{legup\_opt}}}\] + +Where $t$ is the tool being considered. + +*** Compiling the graph + +A tex file is included in the ~/data/data~ directory, which unfortunately can only be compiled outside of the docker file, but will recreate the graphs from the paper using the csv files in the directory. This can be achieved using the following commands: + +#+begin_src shell +docker create ymherklotz/vericert:v1.0 # returns container ID +docker cp $container_id:/data/data . +docker rm $container_id +cd data +pdflatex graphs +#+end_src + +** Running with Vivado + +Finally, for the adventurous that downloaded Vivado, there are some short instructions for running it on single examples. Running synthesis on a benchmark will normally take around 20 minutes to an hour depending on the benchmark, so it might take a long time to complete. + +First, create a new directory and copy the synthesis script into it, as well as the Verilog file that should be synthesisd. For example, once ~make~ was run in the benchmarks folder, one of the benchmarks can be selected for Vericert, such as ~jacobi-1d~: + +#+begin_src shell +mkdir synthesis +cd synthesis +cp /vericert/scripts/synth.tcl . +cp /vericert/benchmarks/polybench-syn/stencils/jacobi-1d.v main.v +#+end_src + +Then Vivado can be run in batch mode in that directory to generate the report: + +#+begin_src shell +vivado -mode batch -source synth.tcl +#+end_src + +Once this completes, the important results of the synthesis should be available in ~encode_report.xml~, where each field will also be present in the relevant CSV file, which is this case is ~/data/data/vericert-nodiv.csv~. + +** Rebuilding the Docker image + +The docker image can be completely rebuilt from scratch as well, by using the Dockerfile that is located in the Vericert repository at ~/vericert/scripts/docker/Dockerfile~, which also contains this document. + +To rebuild the docker image, one first needs to download the LegUp results for the benchmarks without divider[fn:4] and with divider[fn:5], as well as the csv folder with all the raw results[fn:6]. The tar files should be placed into the same directory as the ~Dockerfile~. Then, in the ~docker~ directory, the following will build the docker image, which might take around 20 minutes: + +#+begin_src shell +docker build . +#+end_src + +Then, using the hash it can be run in the same way as the docker container that was linked to this artifact: + +#+begin_src shell +docker run -it <hash> sh +#+end_src + +** Building from git without Docker. + +The only dependency that is require is nix[fn:7]. Once that is installed, we can clone the Github repository and checkout the ~oopsla21~ branch: + +#+begin_src shell +git clone https://github.com/ymherklotz/vericert +cd vericert +git checkout oopsla21 +#+end_src + +Then, it can be compiled and installed using: + +#+begin_src shell +nix-shell --run "make -j7" +nix-shell --run "make install" +nix-shell --run "./bin/vericert ./test/add.c -o add.v" +#+end_src + +* Footnotes + + +[fn:7] https://nixos.org/download.html +[fn:6] https://imperialcollegelondon.box.com/s/nqoaquk7j5mj70db16s6bdbhg44zjn52 +[fn:5] https://imperialcollegelondon.box.com/s/94clcbjowla3987opf3icjz087ozoi1o +[fn:4] https://imperialcollegelondon.box.com/s/ril1utuk2n88fhoq3375oxiqcgw42b8a +[fn:3] https://www.xilinx.com/support/download.html +[fn:2] https://legup.eecg.utoronto.ca +[fn:1] https://www.microsemi.com/product-directory/fpga-design-tools/5590-hls#software-download diff --git a/scripts/docker/artifact.pdf b/scripts/docker/artifact.pdf Binary files differnew file mode 100644 index 0000000..05ec4fd --- /dev/null +++ b/scripts/docker/artifact.pdf diff --git a/scripts/run-legup.sh b/scripts/run-legup.sh new file mode 100644 index 0000000..3b6f60f --- /dev/null +++ b/scripts/run-legup.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash + +top=$(pwd) +vericert=/vericert +rm $top/exec_legup.csv +legup_dir=/data/legup-polybench-$1/legup/legup_$2 + +echo benchmark,cycles >$top/exec_legup.csv + +while read benchmark ; do + echo -n "compiling $(basename "$benchmark"): " + cd $legup_dir/$benchmark + iverilog -o run -s main_tb $vericert/ip/* legup.v + cycles=$(./run | sed -n 3p | sed -E -e 's/[^0-9]+([0-9]+)/\1/') + echo "$(basename "$benchmark"),$cycles" >>$top/exec_legup.csv + echo $cycles cycles +done < benchmark-list-master diff --git a/scripts/run-vivado.sh b/scripts/run-vivado.sh new file mode 100755 index 0000000..117054d --- /dev/null +++ b/scripts/run-vivado.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +benchmark=./$1/$2 +echo $benchmark + + cp ./synth.tcl $benchmark/. 2>/dev/null + cd $benchmark || exit 1 + vivado -mode batch -source synth.tcl >vivado.log 2>&1 diff --git a/scripts/synth.tcl b/scripts/synth.tcl new file mode 100644 index 0000000..e5151e8 --- /dev/null +++ b/scripts/synth.tcl @@ -0,0 +1,109 @@ +proc dump_statistics { } { + set util_rpt [report_utilization -return_string] + set LUTFFPairs 0 + set SliceRegisters 0 + set Slice 0 + set SliceLUTs 0 + set SliceLUTs1 0 + set BRAMFIFO36 0 + set BRAMFIFO18 0 + set BRAMFIFO36_star 0 + set BRAMFIFO18_star 0 + set BRAM18 0 + set BRAMFIFO 0 + set BIOB 0 + set DSPs 0 + set TotPower 0 + set design_slack 0 + set design_req 0 + set design_delay 0 + regexp -- {\s*LUT Flip Flop Pairs\s*\|\s*([^[:blank:]]+)} $util_rpt ignore LUTFFPairs + regexp -- {\s*Slice Registers\s*\|\s*([^[:blank:]]+)} $util_rpt ignore SliceRegisters + regexp -- {\s*Slice\s*\|\s*([^[:blank:]]+)} $util_rpt ignore Slice + regexp -- {\s*Slice LUTs\s*\|\s*([^[:blank:]]+)} $util_rpt ignore SliceLUTs + regexp -- {\s*Slice LUTs\*\s*\|\s*([^[:blank:]]+)} $util_rpt ignore SliceLUTs1 + if { [expr {$LUTFFPairs == 0}] } { + set LUTFFPairs $SliceLUTs1 + puts $SliceLUTs1 + } + if { [expr {$SliceLUTs == 0}] } { + set SliceLUTs $SliceLUTs1 + } + regexp -- {\s*RAMB36/FIFO36\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BRAMFIFO36 + regexp -- {\s*RAMB18/FIFO18\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BRAMFIFO18 + regexp -- {\s*RAMB36/FIFO\*\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BRAMFIFO36_star + regexp -- {\s*RAMB18/FIFO\*\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BRAMFIFO18_star + regexp -- {\s*RAMB18\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BRAM18 + set BRAMFIFO [expr {(2 *$BRAMFIFO36) + $BRAMFIFO18 + (2*$BRAMFIFO36_star) + $BRAMFIFO18_star + $BRAM18}] + regexp -- {\s*Bonded IOB\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BIOB + regexp -- {\s*DSPs\s*\|\s*([^[:blank:]]+)} $util_rpt ignore DSPs + set power_rpt [report_power -return_string] + regexp -- {\s*Total On-Chip Power \(W\)\s*\|\s*([^[:blank:]]+)} $power_rpt ignore TotPower + set Timing_Paths [get_timing_paths -max_paths 1 -nworst 1 -setup] + if { [expr {$Timing_Paths == ""}] } { + set design_slack 0 + set design_req 0 + } else { + set design_slack [get_property SLACK $Timing_Paths] + set design_req [get_property REQUIREMENT $Timing_Paths] + } + if { [expr {$design_slack == ""}] } { + set design_slack 0 + } + if { [expr {$design_req == ""}] } { + set design_req 0 + } + set design_delay [expr {$design_req - $design_slack}] + file delete -force encode_report.xml + set ofile_report [open encode_report.xml w] + puts $ofile_report "<?xml version=\"1.0\"?>" + puts $ofile_report "<document>" + puts $ofile_report " <application>" + puts $ofile_report " <section stringID=\"XILINX_SYNTHESIS_SUMMARY\">" + puts $ofile_report " <item stringID=\"XILINX_LUT_FLIP_FLOP_PAIRS_USED\" value=\"$LUTFFPairs\"/>" + puts $ofile_report " <item stringID=\"XILINX_SLICE\" value=\"$Slice\"/>" + puts $ofile_report " <item stringID=\"XILINX_SLICE_REGISTERS\" value=\"$SliceRegisters\"/>" + puts $ofile_report " <item stringID=\"XILINX_SLICE_LUTS\" value=\"$SliceLUTs\"/>" + puts $ofile_report " <item stringID=\"XILINX_BLOCK_RAMFIFO\" value=\"$BRAMFIFO\"/>" + puts $ofile_report " <item stringID=\"XILINX_IOPIN\" value=\"$BIOB\"/>" + puts $ofile_report " <item stringID=\"XILINX_DSPS\" value=\"$DSPs\"/>" + puts $ofile_report " <item stringID=\"XILINX_POWER\" value=\"$TotPower\"/>" + puts $ofile_report " <item stringID=\"XILINX_DESIGN_DELAY\" value=\"$design_delay\"/>" + puts $ofile_report " </section>" + puts $ofile_report " </application>" + puts $ofile_report "</document>" + close $ofile_report +}; #END PROC +set outputDir . +create_project -in_memory -part xc7z020clg484-1 -force +read_verilog main.v +synth_design -mode out_of_context -no_iobuf -top main -part xc7z020clg484-1 +write_checkpoint -force $outputDir/post_synth.dcp +report_timing_summary -file $outputDir/post_synth_timing_summary.rpt +report_utilization -file $outputDir/post_synth_util.rpt +create_clock -name clk -period 10.000 [get_ports clk] +dump_statistics +opt_design +dump_statistics +report_utilization -file $outputDir/post_opt_design_util.rpt +place_design -directive Explore +report_clock_utilization -file $outputDir/clock_util.rpt +# Optionally run optimization if there are timing violations after placement +if {[get_property SLACK [get_timing_paths -max_paths 1 -nworst 1 -setup]] < 0.5} { + puts "Found setup timing violations => running physical optimization" + phys_opt_design +} +write_checkpoint -force $outputDir/post_place.dcp +report_utilization -file $outputDir/post_place_util.rpt +report_timing_summary -file $outputDir/post_place_timing_summary.rpt +dump_statistics +route_design -directive Explore +write_checkpoint -force $outputDir/post_route.dcp +report_route_status -file $outputDir/post_route_status.rpt +report_timing_summary -file $outputDir/post_route_timing_summary.rpt +report_power -file $outputDir/post_route_power.rpt +report_drc -file $outputDir/post_imp_drc.rpt +report_utilization -file $outputDir/post_route_util.rpt +dump_statistics +close_design +close_project diff --git a/src/Compiler.v b/src/Compiler.v index 61adad1..de29889 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -214,7 +214,9 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := .. coq:: none |*) -Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := +(* This is an unverified version of transf_hls with some experimental additions such as scheduling +that aren't completed yet. *) +(*Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@@ SimplLocals.transf_program @@ -243,7 +245,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@@ RTLPargen.transl_program @@@ HTLPargen.transl_program @@ print print_HTL - @@ Veriloggen.transl_program. + @@ Veriloggen.transl_program.*) (*| Correctness Proof 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. diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 00a1f00..6abe4e0 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -179,7 +179,7 @@ Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". Extract Constant Pipeline.pipeline => "SoftwarePipelining.pipeline". Extract Constant RTLBlockgen.partition => "Partition.partition". -Extract Constant RTLPargen.schedule => "Schedule.schedule_fn". +(*Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".*) (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. @@ -187,11 +187,11 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction Verilog.module vericert.Compiler.transf_hls - vericert.Compiler.transf_hls_temp - RTLBlockgen.transl_program RTLBlockInstr.successors_instr +(* vericert.Compiler.transf_hls_temp*) +(* RTLBlockgen.transl_program RTLBlockInstr.successors_instr*) HTLgen.tbl_to_case_expr Pipeline.pipeline - RTLBlockInstr.sat_pred_temp +(* RTLBlockInstr.sat_pred_temp*) Verilog.stmnt_to_list Compiler.transf_c_program Compiler.transf_cminor_program diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 9746f92..40d1dcc 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -641,9 +641,9 @@ Definition add_control_instr_force_state_incr : s.(st_arrdecls) s.(st_datapath) (AssocMap.set n st s.(st_controllogic))). -Admitted. +Abort. -Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := +(*Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := fun s => OK tt (mkstate s.(st_st) @@ -708,7 +708,7 @@ Lemma create_new_state_state_incr: s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)). -Admitted. +Abort. Definition create_new_state (p: node): mon node := fun s => OK s.(st_freshstate) @@ -876,3 +876,4 @@ Definition transl_program (p : RTLBlockInstr.program) : Errors.res HTL.program : if main_is_internal p then transform_partial_program transl_fundef p else Errors.Error (Errors.msg "Main function is not Internal."). +*) diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml deleted file mode 100644 index 19c6048..0000000 --- a/src/hls/Partition.ml +++ /dev/null @@ -1,124 +0,0 @@ - (* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see <https://www.gnu.org/licenses/>. - *) - -open Printf -open Clflags -open Camlcoq -open Datatypes -open Coqlib -open Maps -open AST -open Kildall -open Op -open RTLBlockInstr -open RTLBlock - -(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass - [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *) -let find_edge i n = - let succ = RTL.successors_instr i in - let filt = List.filter (fun s -> P.lt n s || P.lt s (P.pred n)) succ in - ((match filt with [] -> [] | _ -> [n]), filt) - -let find_edges c = - PTree.fold (fun l n i -> - let f = find_edge i n in - (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], []) - -let prepend_instr i = function - | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e} - -let translate_inst = function - | RTL.Inop _ -> Some RBnop - | RTL.Iop (op, ls, dst, _) -> Some (RBop (None, op, ls, dst)) - | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (None, m, addr, ls, dst)) - | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (None, m, addr, ls, src)) - | _ -> None - -let translate_cfi = function - | RTL.Icall (s, r, ls, dst, n) -> Some (RBcall (s, r, ls, dst, n)) - | RTL.Itailcall (s, r, ls) -> Some (RBtailcall (s, r, ls)) - | RTL.Ibuiltin (e, ls, r, n) -> Some (RBbuiltin (e, ls, r, n)) - | RTL.Icond (c, ls, dst1, dst2) -> Some (RBcond (c, ls, dst1, dst2)) - | RTL.Ijumptable (r, ls) -> Some (RBjumptable (r, ls)) - | RTL.Ireturn r -> Some (RBreturn r) - | _ -> None - -let rec next_bblock_from_RTL is_start e (c : RTL.code) s i = - let succ = List.map (fun i -> (i, PTree.get i c)) (RTL.successors_instr i) in - let trans_inst = (translate_inst i, translate_cfi i) in - match trans_inst, succ with - | (None, Some i'), _ -> - if List.exists (fun x -> x = s) (snd e) && not is_start then - Errors.OK { bb_body = []; bb_exit = RBgoto s } - else - Errors.OK { bb_body = []; bb_exit = i' } - | (Some i', None), (s', Some i_n)::[] -> - if List.exists (fun x -> x = s) (fst e) then - Errors.OK { bb_body = [i']; bb_exit = RBgoto s' } - else if List.exists (fun x -> x = s) (snd e) && not is_start then - Errors.OK { bb_body = []; bb_exit = RBgoto s } - else begin - match next_bblock_from_RTL false e c s' i_n with - | Errors.OK bb -> - Errors.OK (prepend_instr i' bb) - | Errors.Error msg -> Errors.Error msg - end - | _, _ -> - Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong.")) - -let rec traverseacc f l c = - match l with - | [] -> Errors.OK c - | x::xs -> - match f x c with - | Errors.Error msg -> Errors.Error msg - | Errors.OK x' -> - match traverseacc f xs x' with - | Errors.Error msg -> Errors.Error msg - | Errors.OK xs' -> Errors.OK xs' - -let rec translate_all edge c s res = - let c_bb, translated = res in - if List.exists (fun x -> P.eq x s) translated then Errors.OK (c_bb, translated) else - (match PTree.get s c with - | None -> Errors.Error (Errors.msg (coqstring_of_camlstring "Could not translate all.")) - | Some i -> - match next_bblock_from_RTL true edge c s i with - | Errors.Error msg -> Errors.Error msg - | Errors.OK {bb_body = bb; bb_exit = e} -> - let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in - (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with - | Errors.Error msg -> Errors.Error msg - | Errors.OK (c', t') -> - Errors.OK (PTree.set s {bb_body = bb; bb_exit = e} c', t'))) - -(* Partition a function and transform it into RTLBlock. *) -let function_from_RTL f = - let e = find_edges f.RTL.fn_code in - match translate_all e f.RTL.fn_code f.RTL.fn_entrypoint (PTree.empty, []) with - | Errors.Error msg -> Errors.Error msg - | Errors.OK (c, _) -> - Errors.OK { fn_sig = f.RTL.fn_sig; - fn_stacksize = f.RTL.fn_stacksize; - fn_params = f.RTL.fn_params; - fn_entrypoint = f.RTL.fn_entrypoint; - fn_code = c - } - -let partition = function_from_RTL diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml deleted file mode 100644 index 8fef401..0000000 --- a/src/hls/PrintRTLBlock.ml +++ /dev/null @@ -1,72 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Pretty-printers for RTL code *) - -open Printf -open Camlcoq -open Datatypes -open Maps -open AST -open RTLBlockInstr -open RTLBlock -open PrintAST -open PrintRTLBlockInstr - -(* Printing of RTL code *) - -let reg pp r = - fprintf pp "x%d" (P.to_int r) - -let rec regs pp = function - | [] -> () - | [r] -> reg pp r - | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl - -let ros pp = function - | Coq_inl r -> reg pp r - | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) - -let print_bblock pp (pc, i) = - fprintf pp "%5d:{\n" pc; - List.iter (print_bblock_body pp) i.bb_body; - print_bblock_exit pp i.bb_exit; - fprintf pp "\t}\n\n" - -let print_function pp id f = - fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; - let instrs = - List.sort - (fun (pc1, _) (pc2, _) -> compare pc2 pc1) - (List.rev_map - (fun (pc, i) -> (P.to_int pc, i)) - (PTree.elements f.fn_code)) in - List.iter (print_bblock pp) instrs; - fprintf pp "}\n\n" - -let print_globdef pp (id, gd) = - match gd with - | Gfun(Internal f) -> print_function pp id f - | _ -> () - -let print_program pp (prog: program) = - List.iter (print_globdef pp) prog.prog_defs - -let destination : string option ref = ref None - -let print_if passno prog = - match !destination with - | None -> () - | Some f -> - let oc = open_out (f ^ "." ^ Z.to_string passno) in - print_program oc prog; - close_out oc diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml deleted file mode 100644 index ba7241b..0000000 --- a/src/hls/PrintRTLBlockInstr.ml +++ /dev/null @@ -1,87 +0,0 @@ -open Printf -open Camlcoq -open Datatypes -open Maps -open AST -open RTLBlockInstr -open PrintAST - -let reg pp r = - fprintf pp "x%d" (P.to_int r) - -let pred pp r = - fprintf pp "p%d" (Nat.to_int r) - -let rec regs pp = function - | [] -> () - | [r] -> reg pp r - | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl - -let ros pp = function - | Coq_inl r -> reg pp r - | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) - -let rec print_pred_op pp = function - | Pvar p -> pred pp p - | Pnot p -> fprintf pp "(~ %a)" print_pred_op p - | Pand (p1, p2) -> fprintf pp "(%a & %a)" print_pred_op p1 print_pred_op p2 - | Por (p1, p2) -> fprintf pp "(%a | %a)" print_pred_op p1 print_pred_op p2 - -let print_pred_option pp = function - | Some x -> fprintf pp "(%a)" print_pred_op x - | None -> () - -let print_bblock_body pp i = - fprintf pp "\t\t"; - match i with - | RBnop -> fprintf pp "nop\n" - | RBop(p, op, ls, dst) -> - fprintf pp "%a %a = %a\n" - print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls) - | RBload(p, chunk, addr, args, dst) -> - fprintf pp "%a %a = %s[%a]\n" - print_pred_option p reg dst (name_of_chunk chunk) - (PrintOp.print_addressing reg) (addr, args) - | RBstore(p, chunk, addr, args, src) -> - fprintf pp "%a %s[%a] = %a\n" - print_pred_option p - (name_of_chunk chunk) - (PrintOp.print_addressing reg) (addr, args) - reg src - | RBsetpred (c, args, p) -> - fprintf pp "%a = %a\n" - pred p - (PrintOp.print_condition reg) (c, args) - -let rec print_bblock_exit pp i = - fprintf pp "\t\t"; - match i with - | RBcall(_, fn, args, res, _) -> - fprintf pp "%a = %a(%a)\n" - reg res ros fn regs args; - | RBtailcall(_, fn, args) -> - fprintf pp "tailcall %a(%a)\n" - ros fn regs args - | RBbuiltin(ef, args, res, _) -> - fprintf pp "%a = %s(%a)\n" - (print_builtin_res reg) res - (name_of_external ef) - (print_builtin_args reg) args - | RBcond(cond, args, s1, s2) -> - fprintf pp "if (%a) goto %d else goto %d\n" - (PrintOp.print_condition reg) (cond, args) - (P.to_int s1) (P.to_int s2) - | RBjumptable(arg, tbl) -> - let tbl = Array.of_list tbl in - fprintf pp "jumptable (%a)\n" reg arg; - for i = 0 to Array.length tbl - 1 do - fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i)) - done - | RBreturn None -> - fprintf pp "return\n" - | RBreturn (Some arg) -> - fprintf pp "return %a\n" reg arg - | RBgoto n -> - fprintf pp "goto %d\n" (P.to_int n) - | RBpred_cf (p, c1, c2) -> - fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2 diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index a2700a1..a5fa554 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -75,7 +75,7 @@ let pprint_binop l r = let unop = function | Vneg -> " - " - | Vnot -> " ! " + | Vnot -> " ~ " let register a = match PMap.find_opt a !name_map with diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index aaa3c6c..bf5c37a 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -60,7 +60,7 @@ Section RELSEM. | exec_bblock: forall s f sp pc rs rs' m m' t s' bb pr pr', f.(fn_code)!pc = Some bb -> - step_instr_list sp (InstrState rs pr m) bb.(bb_body) (InstrState rs' pr' m') -> + step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> step (State s f sp pc rs pr m) t s' | exec_function_internal: diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index c1d74b5..8cd3468 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -183,36 +183,36 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : | Pvar p' => Some (exist _ (((true, Pos.to_nat p') :: nil) :: nil) _) | Pand p1 p2 => match trans_pred n p1, trans_pred n p2 with - | Some (exist p1' _), Some (exist p2' _) => + | Some (exist _ p1' _), Some (exist _ p2' _) => Some (exist _ (p1' ++ p2') _) | _, _ => None end | Por p1 p2 => match trans_pred n p1, trans_pred n p2 with - | Some (exist p1' _), Some (exist p2' _) => + | Some (exist _ p1' _), Some (exist _ p2' _) => Some (exist _ (mult p1' p2') _) | _, _ => None end - | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _) + | Pnot (Pvar p') => Some (exist _ (((false, Pos.to_nat p') :: nil) :: nil) _) | Pnot (Pnot p') => match trans_pred n p' with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end | Pnot (Pand p1 p2) => match trans_pred n (Por (Pnot p1) (Pnot p2)) with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end | Pnot (Por p1 p2) => match trans_pred n (Pand (Pnot p1) (Pnot p2)) with - | Some (exist p1' _) => Some (exist _ p1' _) + | Some (exist _ p1' _) => Some (exist _ p1' _) | None => None end end end); split; intros; simpl in *; auto. - inv H. inv H0; auto. - - split; auto. destruct (a p') eqn:?; crush. + - split; auto. destruct (a (Pos.to_nat p')) eqn:?; crush. - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto. crush. - rewrite negb_involutive in H. apply i in H. auto. @@ -239,9 +239,9 @@ Definition sat_pred (bound: nat) (p: pred_op) : + {forall a : asgn, sat_predicate p a = false}). refine ( match trans_pred bound p with - | Some (exist fm _) => + | Some (exist _ fm _) => match boundedSat bound fm with - | Some (inleft (exist a _)) => Some (inleft (exist _ a _)) + | Some (inleft (exist _ a _)) => Some (inleft (exist _ a _)) | Some (inright _) => Some (inright _) | None => None end @@ -255,7 +255,7 @@ Qed. Definition sat_pred_simple (bound: nat) (p: pred_op) := match sat_pred bound p with - | Some (inleft (exist al _)) => Some (Some al) + | Some (inleft (exist _ al _)) => Some (Some al) | Some (inright _) => Some None | None => None end. @@ -347,12 +347,11 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := | _, _ => Regmap.init Vundef end. -Inductive instr_state : Type := -| InstrState: - forall (rs: regset) - (pr: predset) - (m: mem), - instr_state. +Record instr_state := mk_instr_state { + instr_st_regset: regset; + instr_st_predset: predset; + instr_st_mem: mem; +}. Section DEFINITION. @@ -440,11 +439,11 @@ Section RELSEM. | eval_pred_true: forall (pr: predset) p rs pr m i, eval_predf pr p = true -> - eval_pred (Some p) (InstrState rs pr m) i i + eval_pred (Some p) (mk_instr_state rs pr m) i i | eval_pred_false: forall (pr: predset) p rs pr m i, eval_predf pr p = false -> - eval_pred (Some p) (InstrState rs pr m) i (InstrState rs pr m) + eval_pred (Some p) (mk_instr_state rs pr m) i (mk_instr_state rs pr m) | eval_pred_none: forall i i', eval_pred None i i' i. @@ -456,25 +455,25 @@ Section RELSEM. | exec_RBop: forall op v res args rs m sp p ist pr, eval_operation ge sp op rs##args m = Some v -> - eval_pred p (InstrState rs pr m) (InstrState (rs#res <- v) pr m) ist -> - step_instr sp (InstrState rs pr m) (RBop p op args res) ist + eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist -> + step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist | exec_RBload: forall addr rs args a chunk m v dst sp p pr ist, eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> - eval_pred p (InstrState rs pr m) (InstrState (rs#dst <- v) pr m) ist -> - step_instr sp (InstrState rs pr m) (RBload p chunk addr args dst) ist + eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist -> + step_instr sp (mk_instr_state rs pr m) (RBload p chunk addr args dst) ist | exec_RBstore: forall addr rs args a chunk m src m' sp p pr ist, eval_addressing ge sp addr rs##args = Some a -> Mem.storev chunk m a rs#src = Some m' -> - eval_pred p (InstrState rs pr m) (InstrState rs pr m') ist -> - step_instr sp (InstrState rs pr m) (RBstore p chunk addr args src) ist + eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist -> + step_instr sp (mk_instr_state rs pr m) (RBstore p chunk addr args src) ist | exec_RBsetpred: forall sp rs pr m p c b args, Op.eval_condition c rs##args m = Some b -> - step_instr sp (InstrState rs pr m) (RBsetpred c args p) - (InstrState rs (PMap.set p b pr) m). + step_instr sp (mk_instr_state rs pr m) (RBsetpred c args p) + (mk_instr_state rs (PMap.set p b pr) m). Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop := | exec_RBcall: diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 9d5fc77..4986cff 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -82,7 +82,7 @@ Section RELSEM. | exec_bblock: forall s f sp pc rs rs' m m' t s' bb pr pr', f.(fn_code)!pc = Some bb -> - step_instr_block sp (InstrState rs pr m) bb.(bb_body) (InstrState rs' pr' m') -> + step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> step (State s f sp pc rs pr m) t s' | exec_function_internal: diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 00adc32..09eabc9 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -31,6 +31,8 @@ Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLPar. Require Import vericert.hls.RTLBlockInstr. +#[local] Open Scope positive. + (*| Schedule Oracle =============== @@ -216,26 +218,27 @@ Inductive expression : Type := | Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression | Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression | Esetpred : predicate -> Op.condition -> expression_list -> expression -> expression -| Econd : expr_pred_list -> expression with expression_list : Type := | Enil : expression_list | Econs : expression -> expression_list -> expression_list -with expr_pred_list : Type := -| EPnil : expr_pred_list -| EPcons : pred_op -> expression -> expr_pred_list -> expr_pred_list . +Inductive pred_expr : Type := +| PEsingleton : option pred_op -> expression -> pred_expr +| PEcons : pred_op -> expression -> pred_expr -> pred_expr. + Definition pred_list_wf l : Prop := forall a b, In a l -> In b l -> a <> b -> unsat (Pand a b). -Fixpoint expr_pred_list_to_list e := - match e with - | EPnil => nil - | EPcons p e l => (p, e) :: expr_pred_list_to_list l +Fixpoint pred_expr_list (p: pred_expr) := + match p with + | PEsingleton None _ => nil + | PEsingleton (Some pr) e => (pr, e) :: nil + | PEcons pr e p' => (pr, e) :: pred_expr_list p' end. -Definition pred_list_wf_ep l : Prop := - pred_list_wf (map fst (expr_pred_list_to_list l)). +Definition pred_list_wf_ep (l: pred_expr) : Prop := + pred_list_wf (map fst (pred_expr_list l)). Lemma unsat_correct1 : forall a b c, @@ -380,11 +383,11 @@ identified as positive numbers. Module Rtree := ITree(R_indexed). -Definition forest : Type := Rtree.t expression. +Definition forest : Type := Rtree.t pred_expr. -Definition get_forest v f := +Definition get_forest v (f: forest) := match Rtree.get v f with - | None => Ebase v + | None => PEsingleton None (Ebase v) | Some v' => v' end. @@ -397,9 +400,9 @@ Definition maybe {A: Type} (vo: A) (pr: predset) p (v: A) := | None => v end. -Definition get_pr i := match i with InstrState a b c => b end. +Definition get_pr i := match i with mk_instr_state a b c => b end. -Definition get_m i := match i with InstrState a b c => c end. +Definition get_m i := match i with mk_instr_state a b c => c end. Definition eval_predf_opt pr p := match p with Some p' => eval_predf pr p' | None => true end. @@ -417,13 +420,13 @@ Inductive sem_value : val -> instr_state -> expression -> val -> Prop := | Sbase_reg: forall sp rs r m pr, - sem_value sp (InstrState rs pr m) (Ebase (Reg r)) (rs !! r) + sem_value sp (mk_instr_state rs pr m) (Ebase (Reg r)) (rs !! r) | Sop: forall rs m op args v lv sp m' mem_exp pr, - sem_mem sp (InstrState rs pr m) mem_exp m' -> - sem_val_list sp (InstrState rs pr m) args lv -> + sem_mem sp (mk_instr_state rs pr m) mem_exp m' -> + sem_val_list sp (mk_instr_state rs pr m) args lv -> Op.eval_operation genv sp op lv m' = Some v -> - sem_value sp (InstrState rs pr m) (Eop op args mem_exp) v + sem_value sp (mk_instr_state rs pr m) (Eop op args mem_exp) v | Sload : forall st mem_exp addr chunk args a v m' lv sp, sem_mem sp st mem_exp m' -> @@ -431,21 +434,17 @@ Inductive sem_value : Op.eval_addressing genv sp addr lv = Some a -> Memory.Mem.loadv chunk m' a = Some v -> sem_value sp st (Eload chunk addr args mem_exp) v -| Scond : - forall sp st e v, - sem_val_ep_list sp st e v -> - sem_value sp st (Econd e) v with sem_pred : val -> instr_state -> expression -> bool -> Prop := | Spred: - forall st mem_exp args p c lv m m' v sp, - sem_mem sp st mem_exp m' -> + forall st pred_exp args p c lv m m' v sp, + sem_pred sp st pred_exp m' -> sem_val_list sp st args lv -> Op.eval_condition c lv m = Some v -> - sem_pred sp st (Esetpred p c args mem_exp) v + sem_pred sp st (Esetpred p c args pred_exp) v | Sbase_pred: forall rs pr m p sp, - sem_pred sp (InstrState rs pr m) (Ebase (Pred p)) (PMap.get p pr) + sem_pred sp (mk_instr_state rs pr m) (Ebase (Pred p)) (PMap.get p pr) with sem_mem : val -> instr_state -> expression -> Memory.mem -> Prop := | Sstore : @@ -458,7 +457,7 @@ with sem_mem : sem_mem sp st (Estore mem_exp chunk addr args val_exp) m'' | Sbase_mem : forall rs m sp pr, - sem_mem sp (InstrState rs pr m) (Ebase Mem) m + sem_mem sp (mk_instr_state rs pr m) (Ebase Mem) m with sem_val_list : val -> instr_state -> expression_list -> list val -> Prop := | Snil : @@ -469,35 +468,51 @@ with sem_val_list : sem_value sp st e v -> sem_val_list sp st l lv -> sem_val_list sp st (Econs e l) (v :: lv) -with sem_val_ep_list : - val -> instr_state -> expr_pred_list -> val -> Prop := -| SPnil : - forall sp rs r m pr, - sem_val_ep_list sp (InstrState rs pr m) EPnil (rs !! r) -| SPconsTrue : - forall pr p sp rs m e v el, - eval_predf pr p = true -> - sem_value sp (InstrState rs pr m) e v -> - sem_val_ep_list sp (InstrState rs pr m) (EPcons p e el) v -| SPconsFalse : - forall pr p sp rs m e v el, - eval_predf pr p = false -> - sem_val_ep_list sp (InstrState rs pr m) el v -> - sem_val_ep_list sp (InstrState rs pr m) (EPcons p e el) v . +Inductive sem_pred_expr {A: Type} (sem: val -> instr_state -> expression -> A -> Prop): + val -> instr_state -> pred_expr -> A -> Prop := +| sem_pred_expr_base : + forall sp st e v, + sem sp st e v -> + sem_pred_expr sem sp st (PEsingleton None e) v +| sem_pred_expr_p : + forall sp st e p v, + eval_predf (instr_st_predset st) p = true -> + sem sp st e v -> + sem_pred_expr sem sp st (PEsingleton (Some p) e) v +| sem_pred_expr_cons_true : + forall sp st e pr p' v, + eval_predf (instr_st_predset st) pr = true -> + sem sp st e v -> + sem_pred_expr sem sp st (PEcons pr e p') v +| sem_pred_expr_cons_false : + forall sp st e pr p' v, + eval_predf (instr_st_predset st) pr = false -> + sem_pred_expr sem sp st p' v -> + sem_pred_expr sem sp st (PEcons pr e p') v +. + +Definition collapse_pe (p: pred_expr) : option expression := + match p with + | PEsingleton None p => Some p + | _ => None + end. + Inductive sem_predset : val -> instr_state -> forest -> predset -> Prop := | Spredset: forall st f sp rs', - (forall x, sem_pred sp st (f # (Pred x)) (PMap.get x rs')) -> + (forall pe x, + collapse_pe (f # (Pred x)) = Some pe -> + sem_pred sp st pe (PMap.get x rs')) -> sem_predset sp st f rs'. Inductive sem_regset : val -> instr_state -> forest -> regset -> Prop := | Sregset: forall st f sp rs', - (forall x, sem_value sp st (f # (Reg x)) (rs' !! x)) -> + (forall x, sem_pred_expr sem_value sp st (f # (Reg x)) (rs' !! x)) -> sem_regset sp st f rs'. Inductive sem : @@ -506,8 +521,8 @@ Inductive sem : forall st rs' m' f sp pr', sem_regset sp st f rs' -> sem_predset sp st f pr' -> - sem_mem sp st (f # Mem) m' -> - sem sp st f (InstrState rs' pr' m'). + sem_pred_expr sem_mem sp st (f # Mem) m' -> + sem sp st f (mk_instr_state rs' pr' m'). End SEMANTICS. @@ -534,7 +549,6 @@ Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := then if condition_eq c1 c2 then if beq_expression_list el1 el2 then beq_expression m1 m2 else false else false else false - | Econd el1, Econd el2 => beq_expr_pred_list el1 el2 | _, _ => false end with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := @@ -543,17 +557,10 @@ with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := | Econs e1 t1, Econs e2 t2 => beq_expression e1 e2 && beq_expression_list t1 t2 | _, _ => false end -with beq_expr_pred_list (el1 el2: expr_pred_list) {struct el1} : bool := - match el1, el2 with - | EPnil, EPnil => true - | EPcons p1 e1 el1', EPcons p2 e2 el2' => true - | _, _ => false - end . Scheme expression_ind2 := Induction for expression Sort Prop with expression_list_ind2 := Induction for expression_list Sort Prop - with expr_pred_list_ind2 := Induction for expr_pred_list Sort Prop . Lemma beq_expression_correct: @@ -564,38 +571,116 @@ Proof. (P := fun (e1 : expression) => forall e2, beq_expression e1 e2 = true -> e1 = e2) (P0 := fun (e1 : expression_list) => - forall e2, beq_expression_list e1 e2 = true -> e1 = e2) - (P1 := fun (e1 : expr_pred_list) => - forall e2, beq_expr_pred_list e1 e2 = true -> e1 = e2); simplify; - repeat match goal with - | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? - | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? - end; subst; f_equal; crush. - eauto using Peqb_true_eq. -Qed. + forall e2, beq_expression_list e1 e2 = true -> e1 = e2); + try solve [repeat match goal with + | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? + | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? + end; subst; f_equal; crush; eauto using Peqb_true_eq]. + destruct e2; try discriminate. eauto. +Abort. + +Definition hash_tree := PTree.t expression. + +Definition find_tree (el: expression) (h: hash_tree) : option positive := + match filter (fun x => beq_expression el (snd x)) (PTree.elements h) with + | (p, _) :: nil => Some p + | _ => None + end. -Definition empty : forest := Rtree.empty _. +Definition combine_option {A} (a b: option A) : option A := + match a, b with + | Some a', _ => Some a' + | _, Some b' => Some b' + | _, _ => None + end. -(*| -This function checks if all the elements in [fa] are in [fb], but not the other way round. -|*) +Definition max_key {A} (t: PTree.t A) := + fold_right Pos.max 1%positive (map fst (PTree.elements t)). + +Definition hash_expr (max: predicate) (e: expression) (h: hash_tree): predicate * hash_tree := + match find_tree e h with + | Some p => (p, h) + | None => + let nkey := Pos.max max (max_key h) + 1 in + (nkey, PTree.set nkey e h) + end. + +Fixpoint encode_expression (max: predicate) (pe: pred_expr) (h: hash_tree): pred_op * hash_tree := + match pe with + | PEsingleton None e => + let (p, h') := hash_expr max e h in + (Pvar p, h') + | PEsingleton (Some p) e => + let (p', h') := hash_expr max e h in + (Por (Pnot p) (Pvar p'), h') + | PEcons p e pe' => + let (p', h') := hash_expr max e h in + let (p'', h'') := encode_expression max pe' h' in + (Pand (Por (Pnot p) (Pvar p')) p'', h'') + end. + +Fixpoint max_predicate (p: pred_op) : positive := + match p with + | Pvar p => p + | Pand a b => Pos.max (max_predicate a) (max_predicate b) + | Por a b => Pos.max (max_predicate a) (max_predicate b) + | Pnot a => max_predicate a + end. + +Fixpoint max_pred_expr (pe: pred_expr) : positive := + match pe with + | PEsingleton None _ => 1 + | PEsingleton (Some p) _ => max_predicate p + | PEcons p _ pe' => Pos.max (max_predicate p) (max_pred_expr pe') + end. + +Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool := + match pe1, pe2 with + (*| PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2 + | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 => + if beq_expression e1 e2 + then match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with + | Some None => true + | _ => false + end + else false + | PEsingleton (Some p) e1, PEsingleton None e2 + | PEsingleton None e1, PEsingleton (Some p) e2 => + if beq_expression e1 e2 + then match sat_pred_simple bound (Pnot p) with + | Some None => true + | _ => false + end + else false*) + | pe1, pe2 => + let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in + let (p1, h) := encode_expression max pe1 (PTree.empty _) in + let (p2, h') := encode_expression max pe2 h in + match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with + | Some None => true + | _ => false + end + end. -Definition check := Rtree.beq beq_expression. +Definition empty : forest := Rtree.empty _. + +Definition check := Rtree.beq (beq_pred_expr 10000). Lemma check_correct: forall (fa fb : forest), check fa fb = true -> (forall x, fa # x = fb # x). Proof. - unfold check, get_forest; intros; + (*unfold check, get_forest; intros; pose proof beq_expression_correct; match goal with [ Hbeq : context[Rtree.beq], y : Rtree.elt |- _ ] => apply (Rtree.beq_sound beq_expression fa fb) with (x := y) in Hbeq end; repeat destruct_match; crush. -Qed. +Qed.*) + Abort. Lemma get_empty: - forall r, empty#r = Ebase r. + forall r, empty#r = PEsingleton None (Ebase r). Proof. intros; unfold get_forest; destruct_match; auto; [ ]; @@ -647,16 +732,11 @@ Proof. apply IHm1_2. intros; apply (H (xI x)). Qed. -Lemma map0: - forall r, - empty # r = Ebase r. -Proof. intros; eapply get_empty. Qed. - Lemma map1: forall w dst dst', dst <> dst' -> - (empty # dst <- w) # dst' = Ebase dst'. -Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply map0. Qed. + (empty # dst <- w) # dst' = PEsingleton None (Ebase dst'). +Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed. Lemma genmap1: forall (f : forest) w dst dst', @@ -665,7 +745,7 @@ Lemma genmap1: Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed. Lemma map2: - forall (v : expression) x rs, + forall (v : pred_expr) x rs, (rs # x <- v) # x = v. Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. @@ -692,24 +772,24 @@ Inductive match_states : instr_state -> instr_state -> Prop := forall rs rs' m m', (forall x, rs !! x = rs' !! x) -> m = m' -> - match_states (InstrState rs m) (InstrState rs' m'). + match_states (mk_instr_state rs m) (mk_instr_state rs' m'). Inductive match_states_ld : instr_state -> instr_state -> Prop := | match_states_ld_intro: forall rs rs' m m', regs_lessdef rs rs' -> Mem.extends m m' -> - match_states_ld (InstrState rs m) (InstrState rs' m'). + match_states_ld (mk_instr_state rs m) (mk_instr_state rs' m'). Lemma sems_det: forall A ge tge sp st f, ge_preserved ge tge -> forall v v' mv mv', - (@sem_value A ge sp st f v /\ @sem_value A tge sp st f v' -> v = v') /\ - (@sem_mem A ge sp st f mv /\ @sem_mem A tge sp st f mv' -> mv = mv'). -Proof. Admitted. + (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\ + (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv'). +Proof. Abort. -Lemma sem_value_det: +(*Lemma sem_value_det: forall A ge tge sp st f v v', ge_preserved ge tge -> @sem_value A ge sp st f v -> @@ -717,7 +797,7 @@ Lemma sem_value_det: v = v'. Proof. intros. destruct st. - generalize (sems_det A ge tge sp (InstrState rs m) f H v v' + generalize (sems_det A ge tge sp (mk_instr_state rs m) f H v v' m m); crush. Qed. @@ -740,7 +820,7 @@ Lemma sem_mem_det: m = m'. Proof. intros. destruct st. - generalize (sems_det A ge tge sp (InstrState rs m0) f H sp sp m m'); + generalize (sems_det A ge tge sp (mk_instr_state rs m0) f H sp sp m m'); crush. Qed. Hint Resolve sem_mem_det : rtlpar. @@ -884,14 +964,14 @@ Abstract computations ===================== |*) -Definition is_regs i := match i with InstrState rs _ => rs end. -Definition is_mem i := match i with InstrState _ m => m end. +Definition is_regs i := match i with mk_instr_state rs _ => rs end. +Definition is_mem i := match i with mk_instr_state _ m => m end. Inductive state_lessdef : instr_state -> instr_state -> Prop := state_lessdef_intro : forall rs1 rs2 m1, (forall x, rs1 !! x = rs2 !! x) -> - state_lessdef (InstrState rs1 m1) (InstrState rs2 m1). + state_lessdef (mk_instr_state rs1 m1) (mk_instr_state rs2 m1). (*| RTLBlock to abstract translation @@ -1133,9 +1213,9 @@ Lemma sem_update_Op : forall A ge sp st f st' r l o0 o m rs v, @sem A ge sp st f st' -> Op.eval_operation ge sp o0 rs ## l m = Some v -> - match_states st' (InstrState rs m) -> + match_states st' (mk_instr_state rs m) -> exists tst, - sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (InstrState (Regmap.set r v rs) m) tst. + sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (mk_instr_state (Regmap.set r v rs) m) tst. Proof. intros. inv H1. simplify. destruct st. @@ -1157,10 +1237,10 @@ Lemma sem_update_load : @sem A ge sp st f st' -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.loadv m m0 a0 = Some v -> - match_states st' (InstrState rs m0) -> + match_states st' (mk_instr_state rs m0) -> exists tst : instr_state, sem ge sp st (update f (RBload o m a l r)) tst - /\ match_states (InstrState (Regmap.set r v rs) m0) tst. + /\ match_states (mk_instr_state (Regmap.set r v rs) m0) tst. Proof. intros. inv H2. pose proof H. inv H. inv H9. destruct st. @@ -1182,9 +1262,9 @@ Lemma sem_update_store : @sem A ge sp st f st' -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.storev m m0 a0 rs !! r = Some m' -> - match_states st' (InstrState rs m0) -> + match_states st' (mk_instr_state rs m0) -> exists tst, sem ge sp st (update f (RBstore o m a l r)) tst - /\ match_states (InstrState rs m') tst. + /\ match_states (mk_instr_state rs m') tst. Proof. intros. inv H2. pose proof H. inv H. inv H9. destruct st. @@ -1214,9 +1294,9 @@ Qed. Lemma sem_update2_Op : forall A ge sp st f r l o0 o m rs v, - @sem A ge sp st f (InstrState rs m) -> + @sem A ge sp st f (mk_instr_state rs m) -> Op.eval_operation ge sp o0 rs ## l m = Some v -> - sem ge sp st (update f (RBop o o0 l r)) (InstrState (Regmap.set r v rs) m). + sem ge sp st (update f (RBop o o0 l r)) (mk_instr_state (Regmap.set r v rs) m). Proof. intros. destruct st. constructor. inv H. inv H6. @@ -1231,10 +1311,10 @@ Qed. Lemma sem_update2_load : forall A ge sp st f r o m a l m0 rs v a0, - @sem A ge sp st f (InstrState rs m0) -> + @sem A ge sp st f (mk_instr_state rs m0) -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.loadv m m0 a0 = Some v -> - sem ge sp st (update f (RBload o m a l r)) (InstrState (Regmap.set r v rs) m0). + sem ge sp st (update f (RBload o m a l r)) (mk_instr_state (Regmap.set r v rs) m0). Proof. intros. simplify. inv H. inv H7. constructor. { constructor; intros. destruct (Pos.eq_dec r x); subst. @@ -1247,10 +1327,10 @@ Qed. Lemma sem_update2_store : forall A ge sp a0 m a l r o f st m' rs m0, - @sem A ge sp st f (InstrState rs m0) -> + @sem A ge sp st f (mk_instr_state rs m0) -> Op.eval_addressing ge sp a rs ## l = Some a0 -> Mem.storev m m0 a0 rs !! r = Some m' -> - sem ge sp st (update f (RBstore o m a l r)) (InstrState rs m'). + sem ge sp st (update f (RBstore o m a l r)) (mk_instr_state rs m'). Proof. intros. simplify. inv H. inv H7. constructor; simplify. { econstructor; intros. rewrite genmap1; crush. } @@ -1563,6 +1643,7 @@ Qed. Proof. intros.*) + (*| Top-level functions =================== @@ -1585,3 +1666,4 @@ Definition transl_fundef := transf_partial_fundef transl_function. Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program := transform_partial_program transl_fundef p. +*) diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index c610ff0..bb1cf97 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -Require Import compcert.backend.Registers. +(*Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Errors. Require Import compcert.common.Linking. @@ -377,3 +377,4 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Qed. End CORRECTNESS. +*) diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml deleted file mode 100644 index c6c8bf4..0000000 --- a/src/hls/Schedule.ml +++ /dev/null @@ -1,801 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see <https://www.gnu.org/licenses/>. - *) - -open Printf -open Clflags -open Camlcoq -open Datatypes -open Coqlib -open Maps -open AST -open Kildall -open Op -open RTLBlockInstr -open RTLBlock -open HTL -open Verilog -open HTLgen -open HTLMonad -open HTLMonadExtra - -module SS = Set.Make(P) - -type svtype = - | BBType of int - | VarType of int * int - -type sv = { - sv_type: svtype; - sv_num: int; -} - -let print_sv v = - match v with - | { sv_type = BBType bbi; sv_num = n } -> sprintf "bb%d_%d" bbi n - | { sv_type = VarType (bbi, i); sv_num = n } -> sprintf "var%dn%d_%d" bbi i n - -module G = Graph.Persistent.Digraph.ConcreteLabeled(struct - type t = sv - let compare = compare - let equal = (=) - let hash = Hashtbl.hash -end)(struct - type t = int - let compare = compare - let hash = Hashtbl.hash - let equal = (=) - let default = 0 -end) - -module GDot = Graph.Graphviz.Dot(struct - let graph_attributes _ = [] - let default_vertex_attributes _ = [] - let vertex_name = print_sv - let vertex_attributes _ = [] - let get_subgraph _ = None - let default_edge_attributes _ = [] - let edge_attributes _ = [] - - include G - end) - -module DFG = Graph.Persistent.Digraph.ConcreteLabeled(struct - type t = int * instr - let compare = compare - let equal = (=) - let hash = Hashtbl.hash -end)(struct - type t = int - let compare = compare - let hash = Hashtbl.hash - let equal = (=) - let default = 0 -end) - -let reg r = sprintf "r%d" (P.to_int r) -let print_pred r = sprintf "p%d" (Nat.to_int r) - -let print_instr = function - | RBnop -> "" - | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r) - | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r) - | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p) - | RBop (_, op, args, d) -> - (match op, args with - | Omove, _ -> "mov" - | Ointconst n, _ -> sprintf "%s=%ld" (reg d) (camlint_of_coqint n) - | Olongconst n, _ -> sprintf "%s=%LdL" (reg d) (camlint64_of_coqint n) - | Ofloatconst n, _ -> sprintf "%s=%.15F" (reg d) (camlfloat_of_coqfloat n) - | Osingleconst n, _ -> sprintf "%s=%.15Ff" (reg d) (camlfloat_of_coqfloat32 n) - | Oindirectsymbol id, _ -> sprintf "%s=&%s" (reg d) (extern_atom id) - | Ocast8signed, [r1] -> sprintf "%s=int8signed(%s)" (reg d) (reg r1) - | Ocast8unsigned, [r1] -> sprintf "%s=int8unsigned(%s)" (reg d) (reg r1) - | Ocast16signed, [r1] -> sprintf "%s=int16signed(%s)" (reg d) (reg r1) - | Ocast16unsigned, [r1] -> sprintf "%s=int16unsigned(%s)" (reg d) (reg r1) - | Oneg, [r1] -> sprintf "%s=-%s" (reg d) (reg r1) - | Osub, [r1;r2] -> sprintf "%s=%s-%s" (reg d) (reg r1) (reg r2) - | Omul, [r1;r2] -> sprintf "%s=%s*%s" (reg d) (reg r1) (reg r2) - | Omulimm n, [r1] -> sprintf "%s=%s*%ld" (reg d) (reg r1) (camlint_of_coqint n) - | Omulhs, [r1;r2] -> sprintf "%s=mulhs(%s,%s)" (reg d) (reg r1) (reg r2) - | Omulhu, [r1;r2] -> sprintf "%s=mulhu(%s,%s)" (reg d) (reg r1) (reg r2) - | Odiv, [r1;r2] -> sprintf "%s=%s /s %s" (reg d) (reg r1) (reg r2) - | Odivu, [r1;r2] -> sprintf "%s=%s /u %s" (reg d) (reg r1) (reg r2) - | Omod, [r1;r2] -> sprintf "%s=%s %%s %s" (reg d) (reg r1) (reg r2) - | Omodu, [r1;r2] -> sprintf "%s=%s %%u %s" (reg d) (reg r1) (reg r2) - | Oand, [r1;r2] -> sprintf "%s=%s & %s" (reg d) (reg r1) (reg r2) - | Oandimm n, [r1] -> sprintf "%s=%s & %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oor, [r1;r2] -> sprintf "%s=%s | %s" (reg d) (reg r1) (reg r2) - | Oorimm n, [r1] -> sprintf "%s=%s | %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oxor, [r1;r2] -> sprintf "%s=%s ^ %s" (reg d) (reg r1) (reg r2) - | Oxorimm n, [r1] -> sprintf "%s=%s ^ %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Onot, [r1] -> sprintf "%s=not(%s)" (reg d) (reg r1) - | Oshl, [r1;r2] -> sprintf "%s=%s << %s" (reg d) (reg r1) (reg r2) - | Oshlimm n, [r1] -> sprintf "%s=%s << %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshr, [r1;r2] -> sprintf "%s=%s >>s %s" (reg d) (reg r1) (reg r2) - | Oshrimm n, [r1] -> sprintf "%s=%s >>s %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshrximm n, [r1] -> sprintf "%s=%s >>x %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshru, [r1;r2] -> sprintf "%s=%s >>u %s" (reg d) (reg r1) (reg r2) - | Oshruimm n, [r1] -> sprintf "%s=%s >>u %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Ororimm n, [r1] -> sprintf "%s=%s ror %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshldimm n, [r1;r2] -> sprintf "%s=(%s, %s) << %ld" (reg d) (reg r1) (reg r2) (camlint_of_coqint n) - | Olea addr, args -> sprintf "%s=addr" (reg d) - | Omakelong, [r1;r2] -> sprintf "%s=makelong(%s,%s)" (reg d) (reg r1) (reg r2) - | Olowlong, [r1] -> sprintf "%s=lowlong(%s)" (reg d) (reg r1) - | Ohighlong, [r1] -> sprintf "%s=highlong(%s)" (reg d) (reg r1) - | Ocast32signed, [r1] -> sprintf "%s=long32signed(%s)" (reg d) (reg r1) - | Ocast32unsigned, [r1] -> sprintf "%s=long32unsigned(%s)" (reg d) (reg r1) - | Onegl, [r1] -> sprintf "%s=-l %s" (reg d) (reg r1) - | Osubl, [r1;r2] -> sprintf "%s=%s -l %s" (reg d) (reg r1) (reg r2) - | Omull, [r1;r2] -> sprintf "%s=%s *l %s" (reg d) (reg r1) (reg r2) - | Omullimm n, [r1] -> sprintf "%s=%s *l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) - | Omullhs, [r1;r2] -> sprintf "%s=mullhs(%s,%s)" (reg d) (reg r1) (reg r2) - | Omullhu, [r1;r2] -> sprintf "%s=mullhu(%s,%s)" (reg d) (reg r1) (reg r2) - | Odivl, [r1;r2] -> sprintf "%s=%s /ls %s" (reg d) (reg r1) (reg r2) - | Odivlu, [r1;r2] -> sprintf "%s=%s /lu %s" (reg d) (reg r1) (reg r2) - | Omodl, [r1;r2] -> sprintf "%s=%s %%ls %s" (reg d) (reg r1) (reg r2) - | Omodlu, [r1;r2] -> sprintf "%s=%s %%lu %s" (reg d) (reg r1) (reg r2) - | Oandl, [r1;r2] -> sprintf "%s=%s &l %s" (reg d) (reg r1) (reg r2) - | Oandlimm n, [r1] -> sprintf "%s=%s &l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) - | Oorl, [r1;r2] -> sprintf "%s=%s |l %s" (reg d) (reg r1) (reg r2) - | Oorlimm n, [r1] -> sprintf "%s=%s |l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) - | Oxorl, [r1;r2] -> sprintf "%s=%s ^l %s" (reg d) (reg r1) (reg r2) - | Oxorlimm n, [r1] -> sprintf "%s=%s ^l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) - | Onotl, [r1] -> sprintf "%s=notl(%s)" (reg d) (reg r1) - | Oshll, [r1;r2] -> sprintf "%s=%s <<l %s" (reg d) (reg r1) (reg r2) - | Oshllimm n, [r1] -> sprintf "%s=%s <<l %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshrl, [r1;r2] -> sprintf "%s=%s >>ls %s" (reg d) (reg r1) (reg r2) - | Oshrlimm n, [r1] -> sprintf "%s=%s >>ls %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshrxlimm n, [r1] -> sprintf "%s=%s >>lx %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oshrlu, [r1;r2] -> sprintf "%s=%s >>lu %s" (reg d) (reg r1) (reg r2) - | Oshrluimm n, [r1] -> sprintf "%s=%s >>lu %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Ororlimm n, [r1] -> sprintf "%s=%s rorl %ld" (reg d) (reg r1) (camlint_of_coqint n) - | Oleal addr, args -> sprintf "%s=addr" (reg d) - | Onegf, [r1] -> sprintf "%s=negf(%s)" (reg d) (reg r1) - | Oabsf, [r1] -> sprintf "%s=absf(%s)" (reg d) (reg r1) - | Oaddf, [r1;r2] -> sprintf "%s=%s +f %s" (reg d) (reg r1) (reg r2) - | Osubf, [r1;r2] -> sprintf "%s=%s -f %s" (reg d) (reg r1) (reg r2) - | Omulf, [r1;r2] -> sprintf "%s=%s *f %s" (reg d) (reg r1) (reg r2) - | Odivf, [r1;r2] -> sprintf "%s=%s /f %s" (reg d) (reg r1) (reg r2) - | Onegfs, [r1] -> sprintf "%s=negfs(%s)" (reg d) (reg r1) - | Oabsfs, [r1] -> sprintf "%s=absfs(%s)" (reg d) (reg r1) - | Oaddfs, [r1;r2] -> sprintf "%s=%s +fs %s" (reg d) (reg r1) (reg r2) - | Osubfs, [r1;r2] -> sprintf "%s=%s -fs %s" (reg d) (reg r1) (reg r2) - | Omulfs, [r1;r2] -> sprintf "%s=%s *fs %s" (reg d) (reg r1) (reg r2) - | Odivfs, [r1;r2] -> sprintf "%s=%s /fs %s" (reg d) (reg r1) (reg r2) - | Osingleoffloat, [r1] -> sprintf "%s=singleoffloat(%s)" (reg d) (reg r1) - | Ofloatofsingle, [r1] -> sprintf "%s=floatofsingle(%s)" (reg d) (reg r1) - | Ointoffloat, [r1] -> sprintf "%s=intoffloat(%s)" (reg d) (reg r1) - | Ofloatofint, [r1] -> sprintf "%s=floatofint(%s)" (reg d) (reg r1) - | Ointofsingle, [r1] -> sprintf "%s=intofsingle(%s)" (reg d) (reg r1) - | Osingleofint, [r1] -> sprintf "%s=singleofint(%s)" (reg d) (reg r1) - | Olongoffloat, [r1] -> sprintf "%s=longoffloat(%s)" (reg d) (reg r1) - | Ofloatoflong, [r1] -> sprintf "%s=floatoflong(%s)" (reg d) (reg r1) - | Olongofsingle, [r1] -> sprintf "%s=longofsingle(%s)" (reg d) (reg r1) - | Osingleoflong, [r1] -> sprintf "%s=singleoflong(%s)" (reg d) (reg r1) - | Ocmp c, args -> sprintf "%s=cmp" (reg d) - | Osel (c, ty), r1::r2::args -> sprintf "%s=sel" (reg d) - | _, _ -> sprintf "N/a") - -module DFGDot = Graph.Graphviz.Dot(struct - let graph_attributes _ = [] - let default_vertex_attributes _ = [] - let vertex_name = function (i, instr) -> sprintf "\"%d:%s\"" i (print_instr instr) - let vertex_attributes _ = [] - let get_subgraph _ = None - let default_edge_attributes _ = [] - let edge_attributes _ = [] - - include DFG - end) - -module IMap = Map.Make (struct - type t = int - - let compare = compare -end) - -let gen_vertex instrs i = (i, List.nth instrs i) - -(** The DFG type defines a list of instructions with their data dependencies as [edges], which are - the pairs of integers that represent the index of the instruction in the [nodes]. The edges - always point from left to right. *) - -let print_list f out_chan a = - fprintf out_chan "[ "; - List.iter (fprintf out_chan "%a " f) a; - fprintf out_chan "]" - -let print_tuple out_chan a = - let l, r = a in - fprintf out_chan "(%d,%d)" l r - -(*let print_dfg out_chan dfg = - fprintf out_chan "{ nodes = %a, edges = %a }" - (print_list PrintRTLBlockInstr.print_bblock_body) - dfg.nodes (print_list print_tuple) dfg.edges*) - -let print_dfg = DFGDot.output_graph - -let read_process command = - let buffer_size = 2048 in - let buffer = Buffer.create buffer_size in - let string = Bytes.create buffer_size in - let in_channel = Unix.open_process_in command in - let chars_read = ref 1 in - while !chars_read <> 0 do - chars_read := input in_channel string 0 buffer_size; - Buffer.add_substring buffer (Bytes.to_string string) 0 !chars_read - done; - ignore (Unix.close_process_in in_channel); - Buffer.contents buffer - -let comb_delay = function - | RBnop -> 0 - | RBop (_, op, _, _) -> - (match op with - | Omove -> 0 - | Ointconst _ -> 0 - | Olongconst _ -> 0 - | Ocast8signed -> 0 - | Ocast8unsigned -> 0 - | Ocast16signed -> 0 - | Ocast16unsigned -> 0 - | Oneg -> 0 - | Onot -> 0 - | Oor -> 0 - | Oorimm _ -> 0 - | Oand -> 0 - | Oandimm _ -> 0 - | Oxor -> 0 - | Oxorimm _ -> 0 - | Omul -> 8 - | Omulimm _ -> 8 - | Omulhs -> 8 - | Omulhu -> 8 - | Odiv -> 72 - | Odivu -> 72 - | Omod -> 72 - | Omodu -> 72 - | _ -> 1) - | _ -> 1 - -let pipeline_stages = function - | RBop (_, op, _, _) -> - (match op with - | Odiv -> 32 - | Odivu -> 32 - | Omod -> 32 - | Omodu -> 32 - | _ -> 0) - | _ -> 0 - -(** Add a dependency if it uses a register that was written to previously. *) -let add_dep map i tree dfg curr = - match PTree.get curr tree with - | None -> dfg - | Some ip -> - let ipv = (List.nth map ip) in - DFG.add_edge_e dfg (ipv, comb_delay (snd ipv), List.nth map i) - -(** This function calculates the dependencies of each instruction. The nodes correspond to previous - registers that were allocated and show which instruction caused it. - - This function only gathers the RAW constraints, and will therefore only be active for operations - that modify registers, which is this case only affects loads and operations. *) -let accumulate_RAW_deps map dfg curr = - let i, dst_map, graph = dfg in - let acc_dep_instruction rs dst = - ( i + 1, - PTree.set dst i dst_map, - List.fold_left (add_dep map i dst_map) graph rs - ) - in - let acc_dep_instruction_nodst rs = - ( i + 1, - dst_map, - List.fold_left (add_dep map i dst_map) graph rs) - in - match curr with - | RBop (op, _, rs, dst) -> acc_dep_instruction rs dst - | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst - | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs) - | _ -> (i + 1, dst_map, graph) - -(** Finds the next write to the [dst] register. This is a small optimisation so that only one - dependency is generated for a data dependency. *) -let rec find_next_dst_write i dst i' curr = - let check_dst dst' curr' = - if dst = dst' then Some (i, i') - else find_next_dst_write i dst (i' + 1) curr' - in - match curr with - | [] -> None - | RBop (_, _, _, dst') :: curr' -> check_dst dst' curr' - | RBload (_, _, _, _, dst') :: curr' -> check_dst dst' curr' - | _ :: curr' -> find_next_dst_write i dst (i' + 1) curr' - -let rec find_all_next_dst_read i dst i' curr = - let check_dst rs curr' = - if List.exists (fun x -> x = dst) rs - then (i, i') :: find_all_next_dst_read i dst (i' + 1) curr' - else find_all_next_dst_read i dst (i' + 1) curr' - in - match curr with - | [] -> [] - | RBop (_, _, rs, _) :: curr' -> check_dst rs curr' - | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr' - | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr' - | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr' - | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr' - -let drop i lst = - let rec drop' i' lst' = - match lst' with - | _ :: ls -> if i' = i then ls else drop' (i' + 1) ls - | [] -> [] - in - if i = 0 then lst else drop' 1 lst - -let take i lst = - let rec take' i' lst' = - match lst' with - | l :: ls -> if i' = i then [ l ] else l :: take' (i' + 1) ls - | [] -> [] - in - if i = 0 then [] else take' 1 lst - -let rec next_store i = function - | [] -> None - | RBstore (_, _, _, _, _) :: _ -> Some i - | _ :: rst -> next_store (i + 1) rst - -let rec next_load i = function - | [] -> None - | RBload (_, _, _, _, _) :: _ -> Some i - | _ :: rst -> next_load (i + 1) rst - -let accumulate_RAW_mem_deps instrs dfg curri = - let i, curr = curri in - match curr with - | RBload (_, _, _, _, _) -> ( - match next_store 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -let accumulate_WAR_mem_deps instrs dfg curri = - let i, curr = curri in - match curr with - | RBstore (_, _, _, _, _) -> ( - match next_load 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -let accumulate_WAW_mem_deps instrs dfg curri = - let i, curr = curri in - match curr with - | RBstore (_, _, _, _, _) -> ( - match next_store 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -(** Predicate dependencies. *) - -let rec in_predicate p p' = - match p' with - | Pvar p'' -> Nat.to_int p = Nat.to_int p'' - | Pnot p'' -> in_predicate p p'' - | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2 - | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2 - -let get_predicate = function - | RBop (p, _, _, _) -> p - | RBload (p, _, _, _, _) -> p - | RBstore (p, _, _, _, _) -> p - | _ -> None - -let rec next_setpred p i = function - | [] -> None - | RBsetpred (_, _, p') :: rst -> - if in_predicate p' p then - Some i - else - next_setpred p (i + 1) rst - | _ :: rst -> next_setpred p (i + 1) rst - -let rec next_preduse p i instr= - let next p' rst = - if in_predicate p p' then - Some i - else - next_preduse p (i + 1) rst - in - match instr with - | [] -> None - | RBload (Some p', _, _, _, _) :: rst -> next p' rst - | RBstore (Some p', _, _, _, _) :: rst -> next p' rst - | RBop (Some p', _, _, _) :: rst -> next p' rst - | _ :: rst -> next_load (i + 1) rst - -let accumulate_RAW_pred_deps instrs dfg curri = - let i, curr = curri in - match get_predicate curr with - | Some p -> ( - match next_setpred p 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -let accumulate_WAR_pred_deps instrs dfg curri = - let i, curr = curri in - match curr with - | RBsetpred (_, _, p) -> ( - match next_preduse p 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -let accumulate_WAW_pred_deps instrs dfg curri = - let i, curr = curri in - match curr with - | RBsetpred (_, _, p) -> ( - match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with - | None -> dfg - | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) - | _ -> dfg - -(** This function calculates the WAW dependencies, which happen when two writes are ordered one - after another and therefore have to be kept in that order. This accumulation might be redundant - if register renaming is done before hand, because then these dependencies can be avoided. *) -let accumulate_WAW_deps instrs dfg curri = - let i, curr = curri in - let dst_dep dst = - match find_next_dst_write i dst (i + 1) (drop (i + 1) instrs) with - | Some (a, b) -> DFG.add_edge dfg (gen_vertex instrs a) (gen_vertex instrs b) - | _ -> dfg - in - match curr with - | RBop (_, _, _, dst) -> dst_dep dst - | RBload (_, _, _, _, dst) -> dst_dep dst - | RBstore (_, _, _, _, _) -> ( - match next_store (i + 1) (drop (i + 1) instrs) with - | None -> dfg - | Some i' -> DFG.add_edge dfg (gen_vertex instrs i) (gen_vertex instrs i') ) - | _ -> dfg - -let accumulate_WAR_deps instrs dfg curri = - let i, curr = curri in - let dst_dep dst = - let dep_list = find_all_next_dst_read i dst 0 (take i instrs |> List.rev) - |> List.map (function (d, d') -> (i - d' - 1, d)) - in - List.fold_left (fun g -> - function (d, d') -> DFG.add_edge g (gen_vertex instrs d) (gen_vertex instrs d')) dfg dep_list - in - match curr with - | RBop (_, _, _, dst) -> dst_dep dst - | RBload (_, _, _, _, dst) -> dst_dep dst - | _ -> dfg - -let assigned_vars vars = function - | RBnop -> vars - | RBop (_, _, _, dst) -> dst :: vars - | RBload (_, _, _, _, dst) -> dst :: vars - | RBstore (_, _, _, _, _) -> vars - | RBsetpred (_, _, _) -> vars - -let get_pred = function - | RBnop -> None - | RBop (op, _, _, _) -> op - | RBload (op, _, _, _, _) -> op - | RBstore (op, _, _, _, _) -> op - | RBsetpred (_, _, _) -> None - -let independant_pred p p' = - match sat_pred_temp (Nat.of_int 100000) (Pand (p, p')) with - | Some None -> true - | _ -> false - -let check_dependent op1 op2 = - match op1, op2 with - | Some p, Some p' -> not (independant_pred p p') - | _, _ -> true - -let remove_unnecessary_deps graph = - let is_dependent v1 v2 g = - let (_, instr1) = v1 in - let (_, instr2) = v2 in - if check_dependent (get_pred instr1) (get_pred instr2) - then g - else DFG.remove_edge g v1 v2 - in - DFG.fold_edges is_dependent graph graph - -(** All the nodes in the DFG have to come after the source of the basic block, and should terminate - before the sink of the basic block. After that, there should be constraints for data - dependencies between nodes. *) -let gather_bb_constraints debug bb = - let ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in - let dfg = List.fold_left (fun dfg v -> DFG.add_vertex dfg v) DFG.empty ibody in - let _, _, dfg' = - List.fold_left (accumulate_RAW_deps ibody) - (0, PTree.empty, dfg) - bb.bb_body - in - let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb.bb_body) dfg ibody) dfg' - [ accumulate_WAW_deps; - accumulate_WAR_deps; - accumulate_RAW_mem_deps; - accumulate_WAR_mem_deps; - accumulate_WAW_mem_deps; - accumulate_RAW_pred_deps; - accumulate_WAR_pred_deps; - accumulate_WAW_pred_deps - ] - in - let dfg''' = remove_unnecessary_deps dfg'' in - (List.length bb.bb_body, dfg''', successors_instr bb.bb_exit) - -let encode_var bbn n i = { sv_type = VarType (bbn, n); sv_num = i } -let encode_bb bbn i = { sv_type = BBType bbn; sv_num = i } - -let add_super_nodes n dfg = - DFG.fold_vertex (function v1 -> fun g -> - (if DFG.in_degree dfg v1 = 0 - then G.add_edge_e g (encode_bb n 0, 0, encode_var n (fst v1) 0) - else g) |> - (fun g' -> - if DFG.out_degree dfg v1 = 0 - then G.add_edge_e g' (encode_var n (fst v1) 0, 0, encode_bb n 1) - else g')) dfg - -let add_data_deps n = - DFG.fold_edges_e (function ((i1, _), l, (i2, _)) -> fun g -> - G.add_edge_e g (encode_var n i1 0, 0, encode_var n i2 0) - ) - -let add_ctrl_deps n succs constr = - List.fold_left (fun g n' -> - G.add_edge_e g (encode_bb n 1, -1, encode_bb n' 0) - ) constr succs - -module BFDFG = Graph.Path.BellmanFord(DFG)(struct - include DFG - type t = int - let weight = DFG.E.label - let compare = compare - let add = (+) - let zero = 0 - end) - -module TopoDFG = Graph.Topological.Make(DFG) - -let negate_graph constr = - DFG.fold_edges_e (function (v1, e, v2) -> fun g -> - DFG.add_edge_e g (v1, -e, v2) - ) constr DFG.empty - -let add_cycle_constr max n dfg constr = - let negated_dfg = negate_graph dfg in - let longest_path v = BFDFG.all_shortest_paths negated_dfg v - |> BFDFG.H.to_seq |> List.of_seq in - let constrained_paths = List.filter (function (v, m) -> - m > max) in - List.fold_left (fun g -> function (v, v', w) -> - G.add_edge_e g (encode_var n (fst v) 0, - - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int max))) - 1), - encode_var n (fst v') 0) - ) constr (DFG.fold_vertex (fun v l -> - List.append l (longest_path v |> constrained_paths - |> List.map (function (v', w) -> (v, v', - w))) - ) dfg []) - -type resource = - | Mem - | SDiv - | UDiv - -type resources = { - res_mem: DFG.V.t list; - res_udiv: DFG.V.t list; - res_sdiv: DFG.V.t list; -} - -let find_resource = function - | RBload _ -> Some Mem - | RBstore _ -> Some Mem - | RBop (_, op, _, _) -> - ( match op with - | Odiv -> Some SDiv - | Odivu -> Some UDiv - | Omod -> Some SDiv - | Omodu -> Some UDiv - | _ -> None ) - | _ -> None - -let add_resource_constr n dfg constr = - let res = TopoDFG.fold (function (i, instr) -> - function {res_mem = ml; res_sdiv = sdl; res_udiv = udl} as r -> - match find_resource instr with - | Some SDiv -> {r with res_sdiv = (i, instr) :: sdl} - | Some UDiv -> {r with res_udiv = (i, instr) :: udl} - | Some Mem -> {r with res_mem = (i, instr) :: ml} - | None -> r - ) dfg {res_mem = []; res_sdiv = []; res_udiv = []} - in - let get_constraints l g = List.fold_left (fun gv v' -> - match gv with - | (g, None) -> (g, Some v') - | (g, Some v) -> - (G.add_edge_e g (encode_var n (fst v) 0, -1, encode_var n (fst v') 0), Some v') - ) (g, None) l |> fst - in - get_constraints (List.rev res.res_mem) constr - |> get_constraints (List.rev res.res_udiv) - |> get_constraints (List.rev res.res_sdiv) - -let gather_cfg_constraints c constr curr = - let (n, dfg) = curr in - match PTree.get (P.of_int n) c with - | None -> assert false - | Some { bb_exit = ctrl; _ } -> - add_super_nodes n dfg constr - |> add_data_deps n dfg - |> add_ctrl_deps n (successors_instr ctrl - |> List.map P.to_int - |> List.filter (fun n' -> n' < n)) - |> add_cycle_constr 8 n dfg - |> add_resource_constr n dfg - -let rec intersperse s = function - | [] -> [] - | [ a ] -> [ a ] - | x :: xs -> x :: s :: intersperse s xs - -let print_objective constr = - let vars = G.fold_vertex (fun v1 l -> - match v1 with - | { sv_type = VarType _; sv_num = 0 } -> print_sv v1 :: l - | _ -> l - ) constr [] - in - "min: " ^ String.concat "" (intersperse " + " vars) ^ ";\n" - -let print_lp constr = - print_objective constr ^ - (G.fold_edges_e (function (e1, w, e2) -> fun s -> - s ^ sprintf "%s - %s <= %d;\n" (print_sv e1) (print_sv e2) w - ) constr "" |> - G.fold_vertex (fun v1 s -> - s ^ sprintf "int %s;\n" (print_sv v1) - ) constr) - -let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ] - -let parse_soln tree s = - let r = Str.regexp "var\\([0-9]+\\)n\\([0-9]+\\)_0[ ]+\\([0-9]+\\)" in - if Str.string_match r s 0 then - IMap.update - (Str.matched_group 1 s |> int_of_string) - (update_schedule - ( Str.matched_group 2 s |> int_of_string, - Str.matched_group 3 s |> int_of_string )) - tree - else tree - -let solve_constraints constr = - let oc = open_out "lpsolve.txt" in - fprintf oc "%s\n" (print_lp constr); - close_out oc; - - Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt") - |> drop 3 - |> List.fold_left parse_soln IMap.empty - -let subgraph dfg l = - let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in - List.fold_left (fun g v -> - List.fold_left (fun g' v' -> - let edges = DFG.find_all_edges dfg v v' in - List.fold_left (fun g'' e -> - DFG.add_edge_e g'' e - ) g' edges - ) g l - ) dfg' l - -let rec all_successors dfg v = - List.concat (List.fold_left (fun l v -> - all_successors dfg v :: l - ) [] (DFG.succ dfg v)) - -let order_instr dfg = - DFG.fold_vertex (fun v li -> - if DFG.in_degree dfg v = 0 - then (List.map snd (v :: all_successors dfg v)) :: li - else li - ) dfg [] - -let combine_bb_schedule schedule s = - let i, st = s in - IMap.update st (update_schedule i) schedule - -(** Should generate the [RTLPar] code based on the input [RTLBlock] description. *) -let transf_rtlpar c c' (schedule : (int * int) list IMap.t) = - let f i bb : RTLPar.bblock = - match bb with - | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c } - | { bb_body = bb_body'; bb_exit = ctrl_flow } -> - let dfg = match PTree.get i c' with None -> assert false | Some x -> x in - let i_sched = IMap.find (P.to_int i) schedule in - let i_sched_tree = - List.fold_left combine_bb_schedule IMap.empty i_sched - in - let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd - |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) - in - (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*) - let final_body2 = List.map (fun x -> subgraph dfg x - |> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x []) - |> List.rev) body - in - { bb_body = List.map (fun x -> [x]) final_body2; - bb_exit = ctrl_flow - } - in - PTree.map f c - -let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) = - let debug = true in - let transf_graph (_, dfg, _) = dfg in - let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in - (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in*) - let cgraph = PTree.elements c' - |> List.map (function (x, y) -> (P.to_int x, y)) - |> List.fold_left (gather_cfg_constraints c) G.empty - in - let graph = open_out "constr_graph.dot" in - fprintf graph "%a\n" GDot.output_graph cgraph; - close_out graph; - let schedule' = solve_constraints cgraph in - (**IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*) - (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*) - transf_rtlpar c c' schedule' - -let rec find_reachable_states c e = - match PTree.get e c with - | Some { bb_exit = ex; _ } -> - e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) [] - (successors_instr ex |> List.filter (fun x -> P.lt x e)) - | None -> assert false - -let add_to_tree c nt i = - match PTree.get i c with - | Some p -> PTree.set i p nt - | None -> assert false - -let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function = - let scheduled = schedule f.fn_entrypoint f.fn_code in - let reachable = find_reachable_states scheduled f.fn_entrypoint - |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in - { fn_sig = f.fn_sig; - fn_params = f.fn_params; - fn_stacksize = f.fn_stacksize; - fn_code = List.fold_left (add_to_tree scheduled) PTree.empty reachable; - fn_entrypoint = f.fn_entrypoint - } diff --git a/test/array.c b/test/array.c index 680acdf..a50cda4 100644 --- a/test/array.c +++ b/test/array.c @@ -1,128 +1,9 @@ -/* durbin.c: this file is part of PolyBench/C */ +int main() { + int a[10] = {0}; -#ifndef SYNTHESIS -#include <stdio.h> -#endif - -unsigned int divider(unsigned int x, unsigned int y) -{ - unsigned int r0, q0, y0, y1; - - r0 = x; - q0 = 0; - y0 = y; - y1 = y; - do - { - y1 = 2 * y1; - } while (y1 <= x); - do - { - y1 = y1 / 2; - q0 = 2 * q0; - if (r0 >= y1) - { - r0 = r0 - y1; - q0 = q0 + 1; - } - } while ((int)y1 != (int)y0); - return q0; -} - -int sdivider(int N, int D) { - if (D < 0) { - if (N < 0) - return divider(-N, -D); - else - return -divider(N, -D); - } else { - if (N < 0) - return -divider(-N, D); - else - return divider(N, D); - } -} - -#define plus(i) i = i + ONE -/* Include polybench common header. */ -static -void init_array (int n, - int r[ 40 + 0]) -{ - int ONE = 1; - int i; - - for (i = 0; i < n; plus(i)) - { - r[i] = (n+ONE-i); + for (int i = 1; i < 10; i++) { + a[i] = a[i-1] + i; } -} - - - -static -int print_array(int n, - int y[ 40 + 0]) - -{ - int ONE = 1; - int i; - int res = 0; - - for (i = 0; i < n; plus(i)) { - res ^= y[i]; - } - -#ifndef SYNTHESIS - printf("finished: %u\n", res); -#endif - - return res; -} - -static -void kernel_durbin(int n, - int r[ 40 + 0], - int y[ 40 + 0]) -{ - int z[40]; - int alpha; - int beta; - int sum; - - int ONE = 1; - int i,k; - y[0] = -r[0]; - beta = 1; - alpha = -r[0]; - - for (k = 1; k < n; plus(k)) { - beta = (ONE-alpha*alpha)*beta; - sum = 0; - for (i=0; i<k; plus(i)) { - sum += r[k-i-ONE]*y[i]; - } - alpha = - sdivider(r[k] + sum, beta); - - for (i=0; i<k; plus(i)) { - z[i] = y[i] + alpha*y[k-i-ONE]; - } - for (i=0; i<k; plus(i)) { - y[i] = z[i]; - } - y[k] = alpha; - } -} - - -int main() -{ - int n = 40; - int r[40 + 0]; - int y[40 + 0]; - - init_array (n, r); - kernel_durbin (n, r, y); - return print_array(n, y); + return a[9]; } diff --git a/test/test_all.sh b/test/test_all.sh index 6b67d27..f072eba 100755 --- a/test/test_all.sh +++ b/test/test_all.sh @@ -21,6 +21,7 @@ test_command() { test_command iverilog test_command gcc +test_command vericert echo "--------------------------------------------------" @@ -30,13 +31,13 @@ for cfile in $test_dir/*.c; do gcc -o $outbase.gcc $cfile >/dev/null 2>&1 $outbase.gcc expected=$? - ./bin/vericert -fschedule -drtl -o $outbase.v $cfile >/dev/null 2>&1 + vericert -drtl -o $outbase.v $cfile >/dev/null 2>&1 if [[ ! -f $outbase.v ]]; then echo "ERROR" continue fi iverilog -o $outbase.iverilog $outbase.v - actual=$($outbase.iverilog | sed -E -e 's/[^0-9]+([0-9]+)/\1/') + actual=$($outbase.iverilog | tail -n1 | sed -E -e 's/[^0-9]+([0-9]+)/\1/') if [[ $expected = $actual ]]; then echo "OK" else |