From c73f4e44c96310540434d0b9cc81e969c6430b90 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 11 Jul 2021 14:12:50 +0200 Subject: Fix the small test bench for Vericert --- test/array.c | 129 +++---------------------------------------------------- test/test_all.sh | 5 ++- 2 files changed, 8 insertions(+), 126 deletions(-) (limited to 'test') diff --git a/test/array.c b/test/array.c index 680acdf..a50cda4 100644 --- a/test/array.c +++ b/test/array.c @@ -1,128 +1,9 @@ -/* durbin.c: this file is part of PolyBench/C */ +int main() { + int a[10] = {0}; -#ifndef SYNTHESIS -#include -#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); + for (int i = 1; i < 10; i++) { + a[i] = a[i-1] + 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/dev/null 2>&1 $outbase.gcc expected=$? - ./bin/vericert -fschedule -drtl -o $outbase.v $cfile >/dev/null 2>&1 + vericert -fschedule -drtl -o $outbase.v $cfile >/dev/null 2>&1 if [[ ! -f $outbase.v ]]; then echo "ERROR" continue fi iverilog -o $outbase.iverilog $outbase.v - actual=$($outbase.iverilog | sed -E -e 's/[^0-9]+([0-9]+)/\1/') + actual=$($outbase.iverilog | tail -n1 | sed -E -e 's/[^0-9]+([0-9]+)/\1/') if [[ $expected = $actual ]]; then echo "OK" else -- cgit