From 51aa5544fbda97c6b49bfba55696083ba47d4cef Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 8 Aug 2014 14:30:45 +0200 Subject: Improved FSM tests --- tests/fsm/.gitignore | 1 + tests/fsm/generate.py | 4 ++-- tests/fsm/run-test.sh | 1 + 3 files changed, 4 insertions(+), 2 deletions(-) create mode 100644 tests/fsm/.gitignore (limited to 'tests') diff --git a/tests/fsm/.gitignore b/tests/fsm/.gitignore new file mode 100644 index 00000000..9c595a6f --- /dev/null +++ b/tests/fsm/.gitignore @@ -0,0 +1 @@ +temp diff --git a/tests/fsm/generate.py b/tests/fsm/generate.py index 0d000f04..722bd62a 100644 --- a/tests/fsm/generate.py +++ b/tests/fsm/generate.py @@ -30,7 +30,7 @@ def random_expr(variables): return "%d'd%s" % (bits, random.randint(0, 2**bits-1)) raise AssertionError -for idx in range(100): +for idx in range(50): with file('temp/uut_%05d.v' % idx, 'w') as f, redirect_stdout(f): print('module uut_%05d(clk, rst, a, b, c, x, y, z);' % (idx)) print(' input clk, rst;') @@ -79,5 +79,5 @@ for idx in range(100): print('opt; wreduce; share; opt; fsm;;') print('cd ..') print('miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold gate miter') - print('sat -verify -seq 5 -set-at 1 in_rst 1 -prove trigger 0 -prove-skip 1 -show-inputs -show-outputs miter') + print('sat -verify-no-timeout -timeout 20 -seq 5 -set-at 1 in_rst 1 -prove trigger 0 -prove-skip 1 -show-inputs -show-outputs miter') diff --git a/tests/fsm/run-test.sh b/tests/fsm/run-test.sh index 697ed935..f5299c09 100755 --- a/tests/fsm/run-test.sh +++ b/tests/fsm/run-test.sh @@ -18,6 +18,7 @@ python generate.py echo "temp/uut_${idx}.log: temp/uut_${idx}.ys temp/uut_${idx}.v" echo " @echo -n '[$i]'" echo " @../../yosys -ql temp/uut_${idx}.log temp/uut_${idx}.ys" + echo " @grep -q 'SAT proof finished' temp/uut_${idx}.log && echo -n K || echo -n T" all_targets="$all_targets temp/uut_${idx}.log" done echo "$all_targets" -- cgit v1.2.3