From 38b249970456a55f0a69ff28070887367e113205 Mon Sep 17 00:00:00 2001 From: Nadesh Ramanathan Date: Tue, 17 Nov 2020 09:06:04 +0000 Subject: final checks reworked and including compilation time in script --- benchmarks/polybench-syn/data-mining/covariance.c | 7 +++++ .../polybench-syn/linear-algebra/blas/gemm.c | 6 ++++ .../polybench-syn/linear-algebra/blas/gemver.c | 6 ++++ .../polybench-syn/linear-algebra/blas/gesummv.c | 3 ++ .../polybench-syn/linear-algebra/blas/symm.c | 6 ++++ .../polybench-syn/linear-algebra/blas/syr2k.c | 6 ++++ .../polybench-syn/linear-algebra/blas/syrk.c | 6 ++++ .../polybench-syn/linear-algebra/blas/trmm.c | 6 ++++ .../polybench-syn/linear-algebra/kernels/2mm.c | 7 +++++ .../polybench-syn/linear-algebra/kernels/3mm.c | 7 +++++ .../polybench-syn/linear-algebra/kernels/atas.c | 7 +++++ .../polybench-syn/linear-algebra/kernels/bicg.c | 7 +++++ .../polybench-syn/linear-algebra/kernels/doitgen.c | 7 +++++ .../polybench-syn/linear-algebra/kernels/mvt.c | 7 +++++ .../linear-algebra/solvers/cholesky.c | 8 +++++ .../polybench-syn/linear-algebra/solvers/lu.c | 34 +++++----------------- .../polybench-syn/linear-algebra/solvers/ludcmp.c | 9 +++++- benchmarks/polybench-syn/medley/floyd-warshall.c | 7 +++++ benchmarks/polybench-syn/medley/nussinov.c | 7 +++++ benchmarks/polybench-syn/run-vericert.sh | 9 +++--- benchmarks/polybench-syn/stencils/fdtd-2d.c | 9 ++++++ benchmarks/polybench-syn/stencils/heat-3d.c | 7 +++++ benchmarks/polybench-syn/stencils/jacobi-1d.c | 7 +++++ benchmarks/polybench-syn/stencils/jacobi-2d.c | 8 +++++ benchmarks/polybench-syn/stencils/seidel-2d.c | 7 +++++ 25 files changed, 168 insertions(+), 32 deletions(-) diff --git a/benchmarks/polybench-syn/data-mining/covariance.c b/benchmarks/polybench-syn/data-mining/covariance.c index b0f1ffa..a591166 100644 --- a/benchmarks/polybench-syn/data-mining/covariance.c +++ b/benchmarks/polybench-syn/data-mining/covariance.c @@ -10,6 +10,10 @@ /* covariance.c: this file is part of PolyBench/C */ #include "../include/misc.h" +#ifndef SYNTHESIS +#include +#endif + #define plus(i) i = i + ONE static @@ -42,6 +46,9 @@ int print_array(int m, for (j = 0; j < m; plus(j)) { res ^= cov[i][j]; } +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/blas/gemm.c b/benchmarks/polybench-syn/linear-algebra/blas/gemm.c index a81f094..2c0aaf7 100644 --- a/benchmarks/polybench-syn/linear-algebra/blas/gemm.c +++ b/benchmarks/polybench-syn/linear-algebra/blas/gemm.c @@ -11,6 +11,9 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif #define plus(i) i = i + ONE static void init_array(int ni, int nj, int nk, @@ -50,6 +53,9 @@ int print_array(int ni, int nj, for (j = 0; j < nj; plus(j)) { res ^= C[i][j]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/blas/gemver.c b/benchmarks/polybench-syn/linear-algebra/blas/gemver.c index fafd49f..2f68871 100644 --- a/benchmarks/polybench-syn/linear-algebra/blas/gemver.c +++ b/benchmarks/polybench-syn/linear-algebra/blas/gemver.c @@ -11,6 +11,9 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif #define plus(i) i = i + ONE static void init_array (int n, @@ -63,6 +66,9 @@ int print_array(int n, for (i = 0; i < n; plus(i)) { res ^= w[i]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/blas/gesummv.c b/benchmarks/polybench-syn/linear-algebra/blas/gesummv.c index e9fe78e..c7d30f3 100644 --- a/benchmarks/polybench-syn/linear-algebra/blas/gesummv.c +++ b/benchmarks/polybench-syn/linear-algebra/blas/gesummv.c @@ -49,6 +49,9 @@ int print_array(int n, for (i = 0; i < n; plus(i)) { res ^= y[i]; } +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/blas/symm.c b/benchmarks/polybench-syn/linear-algebra/blas/symm.c index f13577b..5e8fb1e 100644 --- a/benchmarks/polybench-syn/linear-algebra/blas/symm.c +++ b/benchmarks/polybench-syn/linear-algebra/blas/symm.c @@ -11,6 +11,9 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif #define plus(i) i = i + ONE static void init_array(int m, int n, @@ -51,6 +54,9 @@ int print_array(int m, int n, for (j = 0; j < n; plus(j)) { res ^= C[i][j]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/blas/syr2k.c b/benchmarks/polybench-syn/linear-algebra/blas/syr2k.c index 2214d4a..3366672 100644 --- a/benchmarks/polybench-syn/linear-algebra/blas/syr2k.c +++ b/benchmarks/polybench-syn/linear-algebra/blas/syr2k.c @@ -11,6 +11,9 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif #define plus(i) i = i + ONE static void init_array(int n, int m, @@ -51,6 +54,9 @@ int print_array(int n, for (j = 0; j < n; plus(j)) { res ^= C[i][j]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/blas/syrk.c b/benchmarks/polybench-syn/linear-algebra/blas/syrk.c index 3c792a0..4dd65a6 100644 --- a/benchmarks/polybench-syn/linear-algebra/blas/syrk.c +++ b/benchmarks/polybench-syn/linear-algebra/blas/syrk.c @@ -11,6 +11,9 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif #define plus(i) i = i + ONE static void init_array(int n, int m, @@ -45,6 +48,9 @@ int print_array(int n, for (j = 0; j < n; plus(j)) { res ^= C[i][j]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/blas/trmm.c b/benchmarks/polybench-syn/linear-algebra/blas/trmm.c index e369fd0..a14d131 100644 --- a/benchmarks/polybench-syn/linear-algebra/blas/trmm.c +++ b/benchmarks/polybench-syn/linear-algebra/blas/trmm.c @@ -11,6 +11,9 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif #define plus(i) i = i + ONE static void init_array(int m, int n, @@ -49,6 +52,9 @@ int print_array(int m, int n, for (j = 0; j < n; plus(j)) { res ^= B[i][j]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/kernels/2mm.c b/benchmarks/polybench-syn/linear-algebra/kernels/2mm.c index f5c5ff3..d8b79e2 100644 --- a/benchmarks/polybench-syn/linear-algebra/kernels/2mm.c +++ b/benchmarks/polybench-syn/linear-algebra/kernels/2mm.c @@ -12,6 +12,10 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif + #define plus(i) i = i + ONE static void init_array(int ni, int nj, int nk, int nl, @@ -52,6 +56,9 @@ int print_array(int ni, int nl, for (j = 0; j < nl; plus(j)) { res ^= D[i][j]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/kernels/3mm.c b/benchmarks/polybench-syn/linear-algebra/kernels/3mm.c index 2905719..60be3f8 100644 --- a/benchmarks/polybench-syn/linear-algebra/kernels/3mm.c +++ b/benchmarks/polybench-syn/linear-algebra/kernels/3mm.c @@ -12,6 +12,10 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif + #define plus(i) i = i + ONE static void init_array(int ni, int nj, int nk, int nl, int nm, @@ -52,6 +56,9 @@ int print_array(int ni, int nl, for (j = 0; j < nl; plus(j)) { res ^= G[i][j]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/kernels/atas.c b/benchmarks/polybench-syn/linear-algebra/kernels/atas.c index 7bd0151..c3173e4 100644 --- a/benchmarks/polybench-syn/linear-algebra/kernels/atas.c +++ b/benchmarks/polybench-syn/linear-algebra/kernels/atas.c @@ -11,6 +11,10 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif + #define plus(i) i = i + ONE static void init_array (int m, int n, @@ -42,6 +46,9 @@ int print_array(int n, for (i = 0; i < n; plus(i)) { res ^= y[i]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/kernels/bicg.c b/benchmarks/polybench-syn/linear-algebra/kernels/bicg.c index 5981924..3290f1b 100644 --- a/benchmarks/polybench-syn/linear-algebra/kernels/bicg.c +++ b/benchmarks/polybench-syn/linear-algebra/kernels/bicg.c @@ -12,6 +12,10 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif + #define plus(i) i = i + ONE static void init_array (int m, int n, @@ -50,6 +54,9 @@ int print_array(int m, int n, for (i = 0; i < n; plus(i)) { res ^= q[i]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/kernels/doitgen.c b/benchmarks/polybench-syn/linear-algebra/kernels/doitgen.c index 081a3ba..7a997f1 100644 --- a/benchmarks/polybench-syn/linear-algebra/kernels/doitgen.c +++ b/benchmarks/polybench-syn/linear-algebra/kernels/doitgen.c @@ -11,6 +11,10 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif + #define plus(i) i = i + ONE static void init_array(int nr, int nq, int np, @@ -43,6 +47,9 @@ int print_array(int nr, int nq, int np, for (k = 0; k < np; plus(k)) { res ^= A[i][j][k]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/kernels/mvt.c b/benchmarks/polybench-syn/linear-algebra/kernels/mvt.c index 7eb612e..f8822bb 100644 --- a/benchmarks/polybench-syn/linear-algebra/kernels/mvt.c +++ b/benchmarks/polybench-syn/linear-algebra/kernels/mvt.c @@ -11,6 +11,10 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS + #include +#endif + #define plus(i) i = i + ONE static @@ -56,6 +60,9 @@ int print_array(int n, for (i = 0; i < n; plus(i)) { res ^= x2[i]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/solvers/cholesky.c b/benchmarks/polybench-syn/linear-algebra/solvers/cholesky.c index 05e85ea..b43402b 100644 --- a/benchmarks/polybench-syn/linear-algebra/solvers/cholesky.c +++ b/benchmarks/polybench-syn/linear-algebra/solvers/cholesky.c @@ -11,6 +11,10 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS +#include +#endif + # define SQRT_FUN(x) sqrtf(x) #define plus(i) i = i + ONE @@ -63,6 +67,10 @@ int check_array(int n, for (j = 0; j <= i; plus(j)) { if(A[i][j]!=0) res = 1; } + #ifndef SYNTHESIS + printf("finished: %u\n", res); + #endif + return res; } diff --git a/benchmarks/polybench-syn/linear-algebra/solvers/lu.c b/benchmarks/polybench-syn/linear-algebra/solvers/lu.c index a7ec246..1365f54 100644 --- a/benchmarks/polybench-syn/linear-algebra/solvers/lu.c +++ b/benchmarks/polybench-syn/linear-algebra/solvers/lu.c @@ -16,6 +16,10 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS +#include +#endif + #define plus(i) i = i + ONE static @@ -53,30 +57,6 @@ void init_array (int n, } - - -/* -static -void print_array(int n, - int A[ 40 + 0][40 + 0]) - -{ - int i, j; - - fprintf(stderr, "==BEGIN DUMP_ARRAYS==\n"); - fprintf(stderr, "begin dump: %s", "A"); - for (i = 0; i < n; i++) - for (j = 0; j < n; j++) { - if ((i * n + j) % 20 == 0) fprintf (stderr, "\n"); - fprintf (stderr, "%d ", A[i][j]); - } - fprintf(stderr, "\nend dump: %s\n", "A"); - fprintf(stderr, "==END DUMP_ARRAYS==\n"); -} -*/ - - - static void kernel_lu(int n, int A[ 40][40]) @@ -110,6 +90,9 @@ int check_array(int n, 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; } @@ -126,11 +109,8 @@ int main() init_array (n, A); - - kernel_lu (n, A); - return check_array(n, A); return 0; diff --git a/benchmarks/polybench-syn/linear-algebra/solvers/ludcmp.c b/benchmarks/polybench-syn/linear-algebra/solvers/ludcmp.c index f37d983..0f4522e 100644 --- a/benchmarks/polybench-syn/linear-algebra/solvers/ludcmp.c +++ b/benchmarks/polybench-syn/linear-algebra/solvers/ludcmp.c @@ -11,6 +11,10 @@ #include "../../include/misc.h" +#ifndef SYNTHESIS +#include +#endif + #define plus(i) i = i + ONE static @@ -71,8 +75,11 @@ int check_array(int n, int res = 0; for (i = 0; i < n; plus(i)) { - res += x[i]; + res ^= x[i]; } +#ifndef SYNTHESIS + printf("finished: %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/medley/floyd-warshall.c b/benchmarks/polybench-syn/medley/floyd-warshall.c index 48a7e8d..e840082 100644 --- a/benchmarks/polybench-syn/medley/floyd-warshall.c +++ b/benchmarks/polybench-syn/medley/floyd-warshall.c @@ -11,6 +11,10 @@ #include "../include/misc.h" +#ifndef SYNTHESIS + #include +#endif + #define plus(i) i = i + ONE static void init_array (int n, @@ -44,6 +48,9 @@ int print_array(int n, for (j = 0; j < n; plus(j)) { res ^= path[i][j]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/medley/nussinov.c b/benchmarks/polybench-syn/medley/nussinov.c index a2c3b70..fdd04a2 100644 --- a/benchmarks/polybench-syn/medley/nussinov.c +++ b/benchmarks/polybench-syn/medley/nussinov.c @@ -13,6 +13,10 @@ typedef int base; #include "../include/misc.h" +#ifndef SYNTHESIS + #include +#endif + #define plus(i) i = i + ONE static void init_array (int n, @@ -50,6 +54,9 @@ int print_array(int n, res ^= table[i][j]; } } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/run-vericert.sh b/benchmarks/polybench-syn/run-vericert.sh index 7256235..469fef1 100755 --- a/benchmarks/polybench-syn/run-vericert.sh +++ b/benchmarks/polybench-syn/run-vericert.sh @@ -5,14 +5,15 @@ top=$(pwd) while read benchmark ; do echo "Running "$benchmark clang -Wall -Werror -fsanitize=undefined $benchmark.c -o $benchmark.o - ./$benchmark.o - cresult=$(echo $?) + ./$benchmark.o > $benchmark.clog + cresult=$(cat $benchmark.clog | cut -d' ' -f2) echo "C output: "$cresult - ../../bin/vericert -DSYNTHESIS -O0 -finline --debug-hls $benchmark.c -o $benchmark.v + { time ../../bin/vericert -DSYNTHESIS -O0 -finline --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 -4 $benchmark.tmp | head -1 | tr -s ' ' | cut -d' ' -f3) + ctime=$(cat $benchmark.comp | head -2 | tail -1 | xargs | cut -d' ' -f2 | cut -d'm' -f2 | sed 's/s//g') echo "Veri output: "$veriresult #Undefined checks @@ -38,5 +39,5 @@ while read benchmark ; do echo "PASS" fi name=$(echo $benchmark | awk -v FS="/" '{print $NF}') - echo $name","$cycles >> exec.csv + echo $name","$cycles","$ctime >> exec.csv done < benchmark-list-master diff --git a/benchmarks/polybench-syn/stencils/fdtd-2d.c b/benchmarks/polybench-syn/stencils/fdtd-2d.c index 853d362..c29982e 100644 --- a/benchmarks/polybench-syn/stencils/fdtd-2d.c +++ b/benchmarks/polybench-syn/stencils/fdtd-2d.c @@ -10,6 +10,11 @@ /* fdtd-2d.c: this file is part of PolyBench/C */ +#ifndef SYNTHESIS +#include +#endif + + #include "../include/misc.h" #define plus(i) i = i + ONE @@ -64,6 +69,10 @@ int print_array(int nx, res ^= hz[i][j]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif + return res; } diff --git a/benchmarks/polybench-syn/stencils/heat-3d.c b/benchmarks/polybench-syn/stencils/heat-3d.c index 8df16d4..4bc92ee 100644 --- a/benchmarks/polybench-syn/stencils/heat-3d.c +++ b/benchmarks/polybench-syn/stencils/heat-3d.c @@ -11,6 +11,10 @@ #include "../include/misc.h" +#ifndef SYNTHESIS +#include +#endif + #define plus(i) i = i + ONE static void init_array (int n, @@ -43,6 +47,9 @@ int print_array(int n, for (k = 0; k < n; plus(k)) { res ^= A[i][j][k]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/stencils/jacobi-1d.c b/benchmarks/polybench-syn/stencils/jacobi-1d.c index 95cbb35..7b1d692 100644 --- a/benchmarks/polybench-syn/stencils/jacobi-1d.c +++ b/benchmarks/polybench-syn/stencils/jacobi-1d.c @@ -11,6 +11,10 @@ #include "../include/misc.h" +#ifndef SYNTHESIS +#include +#endif + #define plus(i) i = i + ONE static void init_array (int n, @@ -45,6 +49,9 @@ int print_array(int n, { res ^= A[i]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/stencils/jacobi-2d.c b/benchmarks/polybench-syn/stencils/jacobi-2d.c index 11349f4..2d61d76 100644 --- a/benchmarks/polybench-syn/stencils/jacobi-2d.c +++ b/benchmarks/polybench-syn/stencils/jacobi-2d.c @@ -11,6 +11,11 @@ #include "../include/misc.h" +#ifndef SYNTHESIS +#include +#endif + + #define plus(i) i = i + ONE static void init_array (int n, @@ -46,6 +51,9 @@ int print_array(int n, for (j = 0; j < n; plus(j)) { res ^= A[i][j]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } diff --git a/benchmarks/polybench-syn/stencils/seidel-2d.c b/benchmarks/polybench-syn/stencils/seidel-2d.c index 23ddc74..eb48acc 100644 --- a/benchmarks/polybench-syn/stencils/seidel-2d.c +++ b/benchmarks/polybench-syn/stencils/seidel-2d.c @@ -11,6 +11,10 @@ #include "../include/misc.h" +#ifndef SYNTHESIS +#include +#endif + #define plus(i) i = i + ONE static void init_array (int n, @@ -41,6 +45,9 @@ int print_array(int n, for (j = 0; j < n; plus(j)) { res ^= A[i][j]; } +#ifndef SYNTHESIS + printf("finished %u\n", res); +#endif return res; } -- cgit