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')
+