diff options
Diffstat (limited to 'tests/fsm')
| -rw-r--r-- | tests/fsm/generate.py | 83 | ||||
| -rwxr-xr-x | tests/fsm/run-test.sh | 30 |
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 |