Merge branch 'dev-experiments'

27 files changed, 203 insertions, 96 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/durbin.c b/benchmarks/polybench-syn/linear-algebra/solvers/durbin.c
index 5c853a7..b51adca 100644
--- a/benchmarks/polybench-syn/linear-algebra/solvers/durbin.c
+++ b/benchmarks/polybench-syn/linear-algebra/solvers/durbin.c
@@ -52,45 +52,6 @@ int sdivider(int N, int D) {
     }
 }
 
-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
@@ -118,11 +79,11 @@ int print_array(int n,
     int res = 0;
 
     for (i = 0; i < n; plus(i)) {
-        res  += y[i];
+        res  ^= y[i];
     }
 
 #ifndef SYNTHESIS
-    printf("finished = %u\n", res);
+    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 d925db8..759d6ff 100644
--- a/benchmarks/polybench-syn/linear-algebra/solvers/lu.c
+++ b/benchmarks/polybench-syn/linear-algebra/solvers/lu.c
@@ -17,7 +17,11 @@
 
 #include "../../include/misc.h"
 
-#define plus(n) ((n = n + 1))
+#ifndef SYNTHESIS
+#include <stdio.h>
+#endif 
+
+#define plus(i) i = i + ONE
 
 static
 void init_array (int n,
@@ -25,11 +29,14 @@ void init_array (int n,
 {
   int i, j;
 
-  for (i = 0; i < n; i++)  {
-    for (j = 0; j <= i; j++)
-      A[i][j] = (-j % n) / n + 1;
-    for (j = i+1; j < n; j++) {
-      A[i][j] = 0;
+  for (i = 0; i < n; plus(i))
+    {
+      for (j = 0; j <= i; plus(j))
+ A[i][j] = sdivider(smodulo(-j, n), n) + ONE;
+      for (j = i+1; j < n; plus(j)) {
+ A[i][j] = 0;
+      }
+      A[i][i] = 1;
     }
     A[i][i] = 1;
   }
@@ -53,27 +60,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])
@@ -107,6 +93,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;
 }
@@ -123,8 +112,6 @@ int main()
 
   init_array (n, A);
 
-
-
   kernel_lu (n, A);
 
   return check_array(n, A);
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/linear-algebra/solvers/trisolv.c b/benchmarks/polybench-syn/linear-algebra/solvers/trisolv.c
index 8e76231..2f636df 100644
--- a/benchmarks/polybench-syn/linear-algebra/solvers/trisolv.c
+++ b/benchmarks/polybench-syn/linear-algebra/solvers/trisolv.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,
@@ -23,7 +28,7 @@ void init_array(int n,
 
   for (i = 0; i < n; plus(i))
     {
-      x[i] = - 999;
+      x[i] = -999;
       b[i] = i ;
       for (j = 0; j <= i; plus(j))
         L[i][j] = (int) divider((i+n-j+ONE)*(ONE+ONE), n);
@@ -42,8 +47,12 @@ int check_array(int n,
   int res = 0;
   int ONE = 1;
   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 3be6098..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 -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 f9f4a84..d92183e 100644
--- a/benchmarks/polybench-syn/stencils/fdtd-2d.c
+++ b/benchmarks/polybench-syn/stencils/fdtd-2d.c
@@ -13,6 +13,13 @@
 #include <stdio.h>
 #endif
 
+#ifndef SYNTHESIS
+#include <stdio.h>
+#endif 
+
+
+#include "../include/misc.h"
+
 #define plus(i) i = i + ONE
 static
 void init_array (int tmax,
@@ -25,18 +32,16 @@ void init_array (int tmax,
 {
   int i, j;
   int ONE = 1;
-  int TWO = 1;
-  int THREE = 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] = ((int) i*(j+ONE)) / nx;
- ey[i][j] = ((int) i*(j+TWO)) / ny;
- hz[i][j] = ((int) i*(j+THREE)) / nx;
-      }
+    {
+      ex[i][j] = sdivider(i*(j+1) , nx);
+      ey[i][j] = sdivider(i*(j+2) , ny);
+      hz[i][j] = sdivider(i*(j+3) , nx);
+    }
       
 }
 
@@ -70,7 +75,7 @@ int print_array(int nx,
 #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 6529e8b..4bc92ee 100644
--- a/benchmarks/polybench-syn/stencils/heat-3d.c
+++ b/benchmarks/polybench-syn/stencils/heat-3d.c
@@ -9,6 +9,12 @@
  */
 /* 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,
@@ -17,12 +23,11 @@ void init_array (int n,
 {
   int i, j, k;
   int ONE = 1;
-  int TEN = 10;
 
   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))* TEN / (n);
+        A[i][j][k] = B[i][j][k] = (int) (i + j + (n-k))* sdivider(10, n);
 }
 
 
@@ -42,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;
 }
 
@@ -57,16 +65,14 @@ void kernel_heat_3d(int tsteps,
   int t, i, j, k;
   int ONE = 1;
   int TWO = 2;
-  int FOUR = 4;
 
-#pragma scop
  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]) >> FOUR 
-                                 + (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
+                    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]
                                     ;
                 }
@@ -75,16 +81,15 @@ void kernel_heat_3d(int tsteps,
         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
+                   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];
                                     //;
                }
            }
        }
     }
-#pragma endscop
 }
 
 
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;
 }