final checks reworked and including compilation time in scriptdev-experiments

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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h> 
+#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 <stdio.h> 
+#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 <stdio.h> 
+#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 <stdio.h> 
+#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 <stdio.h> 
+#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 <stdio.h> 
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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 <stdio.h>
+#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;
 }