aboutsummaryrefslogtreecommitdiffstats
path: root/test
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-02-12 14:31:44 +0000
committerYann Herklotz <git@yannherklotz.com>2021-02-12 14:31:44 +0000
commit23c4e482cad3aff97391f32b51993b053d6aa4db (patch)
tree77c75a39c41ca1bcfca1850c894485bf79f2f8f6 /test
parent8d5047ca436ba42e9253d24d6b5b2c0c62dd7437 (diff)
downloadvericert-23c4e482cad3aff97391f32b51993b053d6aa4db.tar.gz
vericert-23c4e482cad3aff97391f32b51993b053d6aa4db.zip
Add temporary fixes to get everything to compile
Diffstat (limited to 'test')
-rw-r--r--test/array.c135
-rwxr-xr-xtest/test_all.sh2
2 files changed, 128 insertions, 9 deletions
diff --git a/test/array.c b/test/array.c
index 59299a5..680acdf 100644
--- a/test/array.c
+++ b/test/array.c
@@ -1,9 +1,128 @@
-int main() {
- int x[10] = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10};
- int sum = 0;
- for (int i = 0; i < 10; i++) {
- sum = sum + x[i];
- x[i] = sum;
- }
- return sum;
+/* durbin.c: this file is part of PolyBench/C */
+
+#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);
+ }
+}
+
+
+
+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);
}
diff --git a/test/test_all.sh b/test/test_all.sh
index 92d3967..6b67d27 100755
--- a/test/test_all.sh
+++ b/test/test_all.sh
@@ -30,7 +30,7 @@ for cfile in $test_dir/*.c; do
gcc -o $outbase.gcc $cfile >/dev/null 2>&1
$outbase.gcc
expected=$?
- ./bin/vericert -drtl -o $outbase.v $cfile >/dev/null 2>&1
+ ./bin/vericert -fschedule -drtl -o $outbase.v $cfile >/dev/null 2>&1
if [[ ! -f $outbase.v ]]; then
echo "ERROR"
continue