diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-02-12 14:31:44 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-12 14:31:44 +0000 |
commit | 23c4e482cad3aff97391f32b51993b053d6aa4db (patch) | |
tree | 77c75a39c41ca1bcfca1850c894485bf79f2f8f6 /test | |
parent | 8d5047ca436ba42e9253d24d6b5b2c0c62dd7437 (diff) | |
download | vericert-23c4e482cad3aff97391f32b51993b053d6aa4db.tar.gz vericert-23c4e482cad3aff97391f32b51993b053d6aa4db.zip |
Add temporary fixes to get everything to compile
Diffstat (limited to 'test')
-rw-r--r-- | test/array.c | 135 | ||||
-rwxr-xr-x | test/test_all.sh | 2 |
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 |