summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/fsm/generate.py83
-rwxr-xr-xtests/fsm/run-test.sh30
2 files changed, 113 insertions, 0 deletions
diff --git a/tests/fsm/generate.py b/tests/fsm/generate.py
new file mode 100644
index 00000000..0d000f04
--- /dev/null
+++ b/tests/fsm/generate.py
@@ -0,0 +1,83 @@
+#!/usr/bin/python
+
+from __future__ import division
+from __future__ import print_function
+
+import sys
+import random
+from contextlib import contextmanager
+
+@contextmanager
+def redirect_stdout(new_target):
+ old_target, sys.stdout = sys.stdout, new_target
+ try:
+ yield new_target
+ finally:
+ sys.stdout = old_target
+
+def random_expr(variables):
+ c = random.choice(['bin', 'uni', 'var', 'const'])
+ if c == 'bin':
+ op = random.choice(['+', '-', '*', '<', '<=', '==', '!=', '>=', '>', '<<', '>>', '<<<', '>>>', '|', '&', '^', '~^', '||', '&&'])
+ return "(%s %s %s)" % (random_expr(variables), op, random_expr(variables))
+ if c == 'uni':
+ op = random.choice(['+', '-', '~', '|', '&', '^', '~^', '!', '$signed', '$unsigned'])
+ return "%s(%s)" % (op, random_expr(variables))
+ if c == 'var':
+ return random.choice(variables)
+ if c == 'const':
+ bits = random.randint(1, 32)
+ return "%d'd%s" % (bits, random.randint(0, 2**bits-1))
+ raise AssertionError
+
+for idx in range(100):
+ 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;')
+ variables=['a', 'b', 'c', 'x', 'y', 'z']
+ print(' input%s [%d:0] a;' % (random.choice(['', ' signed']), random.randint(0, 31)))
+ print(' input%s [%d:0] b;' % (random.choice(['', ' signed']), random.randint(0, 31)))
+ print(' input%s [%d:0] c;' % (random.choice(['', ' signed']), random.randint(0, 31)))
+ print(' output reg%s [%d:0] x;' % (random.choice(['', ' signed']), random.randint(0, 31)))
+ print(' output reg%s [%d:0] y;' % (random.choice(['', ' signed']), random.randint(0, 31)))
+ print(' output reg%s [%d:0] z;' % (random.choice(['', ' signed']), random.randint(0, 31)))
+ print(' reg [15:0] state;')
+ states=[]
+ for i in range(random.randint(2, 10)):
+ n = random.randint(0, 2**16-1)
+ if n not in states:
+ states.append(n)
+ print(' always @(posedge clk) begin')
+ print(' if (rst) begin')
+ print(' x <= %d;' % random.randint(0, 2**31-1))
+ print(' y <= %d;' % random.randint(0, 2**31-1))
+ print(' z <= %d;' % random.randint(0, 2**31-1))
+ print(' state <= %d;' % random.choice(states))
+ print(' end else begin')
+ print(' case (state)')
+ for state in states:
+ print(' %d: begin' % state)
+ for var in ('x', 'y', 'z'):
+ print(' %s <= %s;' % (var, random_expr(variables)))
+ next_states = states[:]
+ for i in range(random.randint(0, len(states))):
+ next_state = random.choice(next_states)
+ next_states.remove(next_state)
+ print(' if ((%s) %s (%s)) state <= %s;' % (random_expr(variables),
+ random.choice(['<', '<=', '>=', '>']), random_expr(variables), next_state))
+ print(' end')
+ print(' endcase')
+ print(' end')
+ print(' end')
+ print('endmodule')
+ with file('temp/uut_%05d.ys' % idx, 'w') as f, redirect_stdout(f):
+ print('read_verilog temp/uut_%05d.v' % idx)
+ print('proc;;')
+ print('copy uut_%05d gold' % idx)
+ print('rename uut_%05d gate' % idx)
+ print('cd gate')
+ 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')
+
diff --git a/tests/fsm/run-test.sh b/tests/fsm/run-test.sh
new file mode 100755
index 00000000..697ed935
--- /dev/null
+++ b/tests/fsm/run-test.sh
@@ -0,0 +1,30 @@
+#!/bin/bash
+
+# run this test many times:
+# time bash -c 'for ((i=0; i<100; i++)); do echo "-- $i --"; bash run-test.sh || exit 1; done'
+
+set -e
+
+rm -rf temp
+mkdir -p temp
+echo "generating tests.."
+python generate.py
+
+{
+ all_targets="all_targets:"
+ echo "all: all_targets"
+ for i in $( ls temp/*.ys | sed 's,[^0-9],,g; s,^0*\(.\),\1,g;' ); do
+ idx=$( printf "%05d" $i )
+ 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"
+ all_targets="$all_targets temp/uut_${idx}.log"
+ done
+ echo "$all_targets"
+} > temp/makefile
+
+echo "running tests.."
+${MAKE:-make} -f temp/makefile
+echo
+
+exit 0