tests/fsm/generate.py

   1 #!/usr/bin/env python3
   2
   3 import argparse
   4 import sys
   5 import random
   6 from contextlib import contextmanager
   7
   8 # set to 'True' to compare verific with yosys
   9 test_verific = False
  10
  11 @contextmanager
  12 def redirect_stdout(new_target):
  13     old_target, sys.stdout = sys.stdout, new_target
  14     try:
  15         yield new_target
  16     finally:
  17         sys.stdout = old_target
  18
  19 def random_expr(variables):
  20     c = random.choice(['bin', 'uni', 'var', 'const'])
  21     if c == 'bin':
  22         op = random.choice(['+', '-', '*', '<', '<=', '==', '!=', '>=', '>', '<<', '>>', '<<<', '>>>', '|', '&', '^', '~^', '||', '&&'])
  23         return "(%s %s %s)" % (random_expr(variables), op, random_expr(variables))
  24     if c == 'uni':
  25         op = random.choice(['+', '-', '~', '|', '&', '^', '~^', '!', '$signed', '$unsigned'])
  26         return "%s(%s)" % (op, random_expr(variables))
  27     if c == 'var':
  28         return random.choice(variables)
  29     if c == 'const':
  30         bits = random.randint(1, 32)
  31         return "%d'd%s" % (bits, random.randint(0, 2**bits-1))
  32     raise AssertionError
  33
  34 parser = argparse.ArgumentParser(formatter_class = argparse.ArgumentDefaultsHelpFormatter)
  35 parser.add_argument('-S', '--seed',  type = int, help = 'seed for PRNG')
  36 parser.add_argument('-c', '--count', type = int, default = 50, help = 'number of test cases to generate')
  37 args = parser.parse_args()
  38
  39 if args.seed is not None:
  40     print("PRNG seed: %d" % args.seed)
  41     random.seed(args.seed)
  42
  43 for idx in range(args.count):
  44     with open('temp/uut_%05d.v' % idx, 'w') as f:
  45         with redirect_stdout(f):
  46             rst2 = random.choice([False, True])
  47             if rst2:
  48                 print('module uut_%05d(clk, rst1, rst2, rst, a, b, c, x, y, z);' % (idx))
  49                 print('  input clk, rst1, rst2;')
  50                 print('  output rst;')
  51                 print('  assign rst = rst1 || rst2;')
  52             else:
  53                 print('module uut_%05d(clk, rst, a, b, c, x, y, z);' % (idx))
  54                 print('  input clk, rst;')
  55             variables=['a', 'b', 'c', 'x', 'y', 'z']
  56             print('  input%s [%d:0] a;' % (random.choice(['', ' signed']), random.randint(0, 31)))
  57             print('  input%s [%d:0] b;' % (random.choice(['', ' signed']), random.randint(0, 31)))
  58             print('  input%s [%d:0] c;' % (random.choice(['', ' signed']), random.randint(0, 31)))
  59             print('  output reg%s [%d:0] x;' % (random.choice(['', ' signed']), random.randint(0, 31)))
  60             print('  output reg%s [%d:0] y;' % (random.choice(['', ' signed']), random.randint(0, 31)))
  61             print('  output reg%s [%d:0] z;' % (random.choice(['', ' signed']), random.randint(0, 31)))
  62             state_bits = random.randint(5, 16);
  63             print('  %sreg [%d:0] state;' % (random.choice(['', '(* fsm_encoding = "one-hot" *)',
  64                     '(* fsm_encoding = "binary" *)']), state_bits-1))
  65             states=[]
  66             for i in range(random.randint(2, 10)):
  67                 n = random.randint(0, 2**state_bits-1)
  68                 if n not in states:
  69                     states.append(n)
  70             print('  always @(posedge clk) begin')
  71             print('    if (%s) begin' % ('rst1' if rst2 else 'rst'))
  72             print('      x <= %d;' % random.randint(0, 2**31-1))
  73             print('      y <= %d;' % random.randint(0, 2**31-1))
  74             print('      z <= %d;' % random.randint(0, 2**31-1))
  75             print('      state <= %d;' % random.choice(states))
  76             print('    end else begin')
  77             print('      case (state)')
  78             for state in states:
  79                 print('        %d: begin' % state)
  80                 for var in ('x', 'y', 'z'):
  81                     print('            %s <= %s;' % (var, random_expr(variables)))
  82                 next_states = states[:]
  83                 for i in range(random.randint(0, len(states))):
  84                     next_state = random.choice(next_states)
  85                     next_states.remove(next_state)
  86                     print('            if ((%s) %s (%s)) state <= %s;' % (random_expr(variables),
  87                             random.choice(['<', '<=', '>=', '>']), random_expr(variables), next_state))
  88                 print('          end')
  89             print('      endcase')
  90             if rst2:
  91                 print('      if (rst2) begin')
  92                 print('        x <= a;')
  93                 print('        y <= b;')
  94                 print('        z <= c;')
  95                 print('        state <= %d;' % random.choice(states))
  96                 print('      end')
  97             print('    end')
  98             print('  end')
  99             print('endmodule')
 100     with open('temp/uut_%05d.ys' % idx, 'w') as f:
 101         with redirect_stdout(f):
 102             if test_verific:
 103                 print('read_verilog temp/uut_%05d.v' % idx)
 104                 print('proc;; rename uut_%05d gold' % idx)
 105                 print('verific -vlog2k temp/uut_%05d.v' % idx)
 106                 print('verific -import uut_%05d' % idx)
 107                 print('rename uut_%05d gate' % idx)
 108             else:
 109                 print('read_verilog temp/uut_%05d.v' % idx)
 110                 print('proc;;')
 111                 print('copy uut_%05d gold' % idx)
 112                 print('rename uut_%05d gate' % idx)
 113                 print('cd gate')
 114                 print('opt; wreduce; share%s; opt; fsm;;' % random.choice(['', ' -aggressive']))
 115                 print('cd ..')
 116             print('miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold gate miter')
 117             print('sat -verify-no-timeout -timeout 20 -seq 5 -set-at 1 %s_rst 1 -prove trigger 0 -prove-skip 1 -show-inputs -show-outputs miter' % ('gold' if rst2 else 'in'))
 118