summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-08-08 14:30:45 +0200
committerClifford Wolf <clifford@clifford.at>2014-08-08 15:08:11 +0200
commit51aa5544fbda97c6b49bfba55696083ba47d4cef (patch)
tree8aa603acbca96bb6514cd2c240865d332e3f1947
parent58ac605470aed3b2a537b4f99ac17a199f8b5233 (diff)
Improved FSM tests
-rw-r--r--Makefile1
-rw-r--r--tests/fsm/.gitignore1
-rw-r--r--tests/fsm/generate.py4
-rwxr-xr-xtests/fsm/run-test.sh1
4 files changed, 5 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index cd43e53b..0e3a88a7 100644
--- a/Makefile
+++ b/Makefile
@@ -218,6 +218,7 @@ test: $(TARGETS) $(EXTRA_TARGETS)
+cd tests/asicworld && bash run-test.sh
+cd tests/realmath && bash run-test.sh
+cd tests/share && bash run-test.sh
+ +cd tests/fsm && bash run-test.sh
+cd tests/techmap && bash run-test.sh
+cd tests/memories && bash run-test.sh
+cd tests/various && bash run-test.sh
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"