6 from contextlib
import contextmanager
8 # set to 'True' to compare verific with yosys
12 def redirect_stdout(new_target
):
13 old_target
, sys
.stdout
= sys
.stdout
, new_target
17 sys
.stdout
= old_target
19 def random_expr(variables
):
20 c
= random
.choice(['bin', 'uni', 'var', 'const'])
22 op
= random
.choice(['+', '-', '*', '<', '<=', '==', '!=', '>=', '>', '<<', '>>', '<<<', '>>>', '|', '&', '^', '~^', '||', '&&'])
23 return "(%s %s %s)" % (random_expr(variables
), op
, random_expr(variables
))
25 op
= random
.choice(['+', '-', '~', '|', '&', '^', '~^', '!', '$signed', '$unsigned'])
26 return "%s(%s)" % (op
, random_expr(variables
))
28 return random
.choice(variables
)
30 bits
= random
.randint(1, 32)
31 return "%d'd%s" % (bits
, random
.randint(0, 2**bits
-1))
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()
39 if args
.seed
is not None:
40 print("PRNG seed: %d" % args
.seed
)
41 random
.seed(args
.seed
)
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])
48 print('module uut_%05d(clk, rst1, rst2, rst, a, b, c, x, y, z);' % (idx
))
49 print(' input clk, rst1, rst2;')
51 print(' assign rst = rst1 || rst2;')
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))
66 for i
in range(random
.randint(2, 10)):
67 n
= random
.randint(0, 2**state_bits
-1)
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)')
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
))
91 print(' if (rst2) begin')
95 print(' state <= %d;' % random
.choice(states
))
100 with
open('temp/uut_%05d.ys' % idx
, 'w') as f
:
101 with
redirect_stdout(f
):
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
)
109 print('read_verilog temp/uut_%05d.v' % idx
)
111 print('copy uut_%05d gold' % idx
)
112 print('rename uut_%05d gate' % idx
)
114 print('opt; wreduce; share%s; opt; fsm;;' % random
.choice(['', ' -aggressive']))
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'))