summaryrefslogtreecommitdiff
path: root/tests/fsm/generate.py
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-08-08 13:12:18 +0200
committerClifford Wolf <clifford@clifford.at>2014-08-08 13:12:18 +0200
commitc07774b0b674805014b3ea16b28a01d40ba83d11 (patch)
treee39f39d11ea2ab2d961020fd122d06a5267fd8c8 /tests/fsm/generate.py
parent622ebab6710815324fa7250554b56f673862b479 (diff)
Added FSM test bench
Diffstat (limited to 'tests/fsm/generate.py')
-rw-r--r--tests/fsm/generate.py83
1 files changed, 83 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')
+