diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/fsm/generate.py | 146 | ||||
| -rw-r--r-- | tests/realmath/generate.py | 99 | ||||
| -rw-r--r-- | tests/share/generate.py | 92 |
3 files changed, 172 insertions, 165 deletions
diff --git a/tests/fsm/generate.py b/tests/fsm/generate.py index b5b4626d..fc67543f 100644 --- a/tests/fsm/generate.py +++ b/tests/fsm/generate.py @@ -34,76 +34,78 @@ def random_expr(variables): raise AssertionError for idx in range(50): - with file('temp/uut_%05d.v' % idx, 'w') as f, redirect_stdout(f): - rst2 = random.choice([False, True]) - if rst2: - print('module uut_%05d(clk, rst1, rst2, rst, a, b, c, x, y, z);' % (idx)) - print(' input clk, rst1, rst2;') - print(' output rst;') - print(' assign rst = rst1 || rst2;') - else: - 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))) - state_bits = random.randint(5, 16); - print(' %sreg [%d:0] state;' % (random.choice(['', '(* fsm_encoding = "one-hot" *)', - '(* fsm_encoding = "binary" *)']), state_bits-1)) - states=[] - for i in range(random.randint(2, 10)): - n = random.randint(0, 2**state_bits-1) - if n not in states: - states.append(n) - print(' always @(posedge clk) begin') - print(' if (%s) begin' % ('rst1' if rst2 else 'rst')) - 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') - if rst2: - print(' if (rst2) begin') - print(' x <= a;') - print(' y <= b;') - print(' z <= c;') - print(' state <= %d;' % random.choice(states)) - print(' end') - print(' end') - print(' end') - print('endmodule') - with file('temp/uut_%05d.ys' % idx, 'w') as f, redirect_stdout(f): - if test_verific: - print('read_verilog temp/uut_%05d.v' % idx) - print('proc;; rename uut_%05d gold' % idx) - print('verific -vlog2k temp/uut_%05d.v' % idx) - print('verific -import uut_%05d' % idx) - print('rename uut_%05d gate' % idx) - else: - 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%s; opt; fsm;;' % random.choice(['', ' -aggressive'])) - print('cd ..') - print('miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold gate miter') - 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')) + with file('temp/uut_%05d.v' % idx, 'w') as f: + with redirect_stdout(f): + rst2 = random.choice([False, True]) + if rst2: + print('module uut_%05d(clk, rst1, rst2, rst, a, b, c, x, y, z);' % (idx)) + print(' input clk, rst1, rst2;') + print(' output rst;') + print(' assign rst = rst1 || rst2;') + else: + 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))) + state_bits = random.randint(5, 16); + print(' %sreg [%d:0] state;' % (random.choice(['', '(* fsm_encoding = "one-hot" *)', + '(* fsm_encoding = "binary" *)']), state_bits-1)) + states=[] + for i in range(random.randint(2, 10)): + n = random.randint(0, 2**state_bits-1) + if n not in states: + states.append(n) + print(' always @(posedge clk) begin') + print(' if (%s) begin' % ('rst1' if rst2 else 'rst')) + 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') + if rst2: + print(' if (rst2) begin') + print(' x <= a;') + print(' y <= b;') + print(' z <= c;') + print(' state <= %d;' % random.choice(states)) + print(' end') + print(' end') + print(' end') + print('endmodule') + with file('temp/uut_%05d.ys' % idx, 'w') as f: + with redirect_stdout(f): + if test_verific: + print('read_verilog temp/uut_%05d.v' % idx) + print('proc;; rename uut_%05d gold' % idx) + print('verific -vlog2k temp/uut_%05d.v' % idx) + print('verific -import uut_%05d' % idx) + print('rename uut_%05d gate' % idx) + else: + 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%s; opt; fsm;;' % random.choice(['', ' -aggressive'])) + print('cd ..') + print('miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold gate miter') + 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')) diff --git a/tests/realmath/generate.py b/tests/realmath/generate.py index 972021dc..24d13561 100644 --- a/tests/realmath/generate.py +++ b/tests/realmath/generate.py @@ -40,52 +40,55 @@ def random_expression(depth = 3, maxparam = 0): raise for idx in range(100): - with file('temp/uut_%05d.v' % idx, 'w') as f, redirect_stdout(f): - print('module uut_%05d(output [63:0] %s);\n' % (idx, ', '.join(['y%02d' % i for i in range(100)]))) - for i in range(30): - if idx < 10: - print('localparam p%02d = %s;' % (i, random_expression())) - else: - print('localparam%s p%02d = %s;' % (random.choice(['', ' real', ' integer']), i, random_expression())) - for i in range(30, 60): - if idx < 10: - print('localparam p%02d = %s;' % (i, random_expression(maxparam = 30))) - else: - print('localparam%s p%02d = %s;' % (random.choice(['', ' real', ' integer']), i, random_expression(maxparam = 30))) - for i in range(100): - print('assign y%02d = 65536 * (%s);' % (i, random_expression(maxparam = 60))) - print('endmodule') - with file('temp/uut_%05d.ys' % idx, 'w') as f, redirect_stdout(f): - print('read_verilog uut_%05d.v' % idx) - print('rename uut_%05d uut_%05d_syn' % (idx, idx)) - print('write_verilog uut_%05d_syn.v' % idx) - with file('temp/uut_%05d_tb.v' % idx, 'w') as f, redirect_stdout(f): - print('module uut_%05d_tb;\n' % idx) - print('wire [63:0] %s;' % (', '.join(['r%02d' % i for i in range(100)]))) - print('wire [63:0] %s;' % (', '.join(['s%02d' % i for i in range(100)]))) - print('uut_%05d ref(%s);' % (idx, ', '.join(['r%02d' % i for i in range(100)]))) - print('uut_%05d_syn syn(%s);' % (idx, ', '.join(['s%02d' % i for i in range(100)]))) - print('task compare_ref_syn;') - print(' input [7:0] i;') - print(' input [63:0] r, s;') - print(' reg [64*8-1:0] buffer;') - print(' integer j;') - print(' begin') - print(' if (-1 <= $signed(r-s) && $signed(r-s) <= +1) begin') - print(' // $display("%d: %b %b", i, r, s);') - print(' end else if (r === s) begin ') - print(' // $display("%d: %b %b", i, r, s);') - print(' end else begin ') - print(' for (j = 0; j < 64; j = j+1)') - print(' buffer[j*8 +: 8] = r[j] !== s[j] ? "^" : " ";') - print(' $display("\\n%3d: %b %b", i, r, s);') - print(' $display(" %s %s", buffer, buffer);') - print(' end') - print(' end') - print('endtask') - print('initial begin #1;') - for i in range(100): - print(' compare_ref_syn(%2d, r%02d, s%02d);' % (i, i, i)) - print('end') - print('endmodule') + with file('temp/uut_%05d.v' % idx, 'w') as f: + with redirect_stdout(f): + print('module uut_%05d(output [63:0] %s);\n' % (idx, ', '.join(['y%02d' % i for i in range(100)]))) + for i in range(30): + if idx < 10: + print('localparam p%02d = %s;' % (i, random_expression())) + else: + print('localparam%s p%02d = %s;' % (random.choice(['', ' real', ' integer']), i, random_expression())) + for i in range(30, 60): + if idx < 10: + print('localparam p%02d = %s;' % (i, random_expression(maxparam = 30))) + else: + print('localparam%s p%02d = %s;' % (random.choice(['', ' real', ' integer']), i, random_expression(maxparam = 30))) + for i in range(100): + print('assign y%02d = 65536 * (%s);' % (i, random_expression(maxparam = 60))) + print('endmodule') + with file('temp/uut_%05d.ys' % idx, 'w') as f: + with redirect_stdout(f): + print('read_verilog uut_%05d.v' % idx) + print('rename uut_%05d uut_%05d_syn' % (idx, idx)) + print('write_verilog uut_%05d_syn.v' % idx) + with file('temp/uut_%05d_tb.v' % idx, 'w') as f: + with redirect_stdout(f): + print('module uut_%05d_tb;\n' % idx) + print('wire [63:0] %s;' % (', '.join(['r%02d' % i for i in range(100)]))) + print('wire [63:0] %s;' % (', '.join(['s%02d' % i for i in range(100)]))) + print('uut_%05d ref(%s);' % (idx, ', '.join(['r%02d' % i for i in range(100)]))) + print('uut_%05d_syn syn(%s);' % (idx, ', '.join(['s%02d' % i for i in range(100)]))) + print('task compare_ref_syn;') + print(' input [7:0] i;') + print(' input [63:0] r, s;') + print(' reg [64*8-1:0] buffer;') + print(' integer j;') + print(' begin') + print(' if (-1 <= $signed(r-s) && $signed(r-s) <= +1) begin') + print(' // $display("%d: %b %b", i, r, s);') + print(' end else if (r === s) begin ') + print(' // $display("%d: %b %b", i, r, s);') + print(' end else begin ') + print(' for (j = 0; j < 64; j = j+1)') + print(' buffer[j*8 +: 8] = r[j] !== s[j] ? "^" : " ";') + print(' $display("\\n%3d: %b %b", i, r, s);') + print(' $display(" %s %s", buffer, buffer);') + print(' end') + print(' end') + print('endtask') + print('initial begin #1;') + for i in range(100): + print(' compare_ref_syn(%2d, r%02d, s%02d);' % (i, i, i)) + print('end') + print('endmodule') diff --git a/tests/share/generate.py b/tests/share/generate.py index a06a642d..bb96fec6 100644 --- a/tests/share/generate.py +++ b/tests/share/generate.py @@ -25,49 +25,51 @@ def maybe_plus_x(expr): return expr for idx in range(100): - with file('temp/uut_%05d.v' % idx, 'w') as f, redirect_stdout(f): - if random.choice(['bin', 'uni']) == 'bin': - print('module uut_%05d(a, b, c, d, x, s, y);' % (idx)) - op = random.choice([ - random.choice(['+', '-', '*', '/', '%']), - random.choice(['<', '<=', '==', '!=', '===', '!==', '>=', '>' ]), - random.choice(['<<', '>>', '<<<', '>>>']), - random.choice(['|', '&', '^', '~^', '||', '&&']), - ]) - print(' input%s [%d:0] a;' % (random.choice(['', ' signed']), random.randint(0, 8))) - print(' input%s [%d:0] b;' % (random.choice(['', ' signed']), random.randint(0, 8))) - print(' input%s [%d:0] c;' % (random.choice(['', ' signed']), random.randint(0, 8))) - print(' input%s [%d:0] d;' % (random.choice(['', ' signed']), random.randint(0, 8))) - print(' input%s [%d:0] x;' % (random.choice(['', ' signed']), random.randint(0, 8))) - print(' input s;') - print(' output [%d:0] y;' % random.randint(0, 8)) - print(' assign y = (s ? %s(%s %s %s) : %s(%s %s %s))%s;' % - (random.choice(['', '$signed', '$unsigned']), maybe_plus_x('a'), op, maybe_plus_x('b'), - random.choice(['', '$signed', '$unsigned']), maybe_plus_x('c'), op, maybe_plus_x('d'), - random_plus_x() if random.randint(0, 4) == 0 else '')) - print('endmodule') - else: - print('module uut_%05d(a, b, x, s, y);' % (idx)) - op = random.choice(['~', '-', '!']) - print(' input%s [%d:0] a;' % (random.choice(['', ' signed']), random.randint(0, 8))) - print(' input%s [%d:0] b;' % (random.choice(['', ' signed']), random.randint(0, 8))) - print(' input%s [%d:0] x;' % (random.choice(['', ' signed']), random.randint(0, 8))) - print(' input s;') - print(' output [%d:0] y;' % random.randint(0, 8)) - print(' assign y = (s ? %s(%s%s) : %s(%s%s))%s;' % - (random.choice(['', '$signed', '$unsigned']), op, maybe_plus_x('a'), - random.choice(['', '$signed', '$unsigned']), op, maybe_plus_x('b'), - random_plus_x() if random.randint(0, 4) == 0 else '')) - 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('tee -a temp/all_share_log.txt log') - print('tee -a temp/all_share_log.txt log #job# uut_%05d' % idx) - print('tee -a temp/all_share_log.txt wreduce') - print('tee -a temp/all_share_log.txt share -aggressive gate') - print('miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold gate miter') - print('sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter') + with file('temp/uut_%05d.v' % idx, 'w') as f: + with redirect_stdout(f): + if random.choice(['bin', 'uni']) == 'bin': + print('module uut_%05d(a, b, c, d, x, s, y);' % (idx)) + op = random.choice([ + random.choice(['+', '-', '*', '/', '%']), + random.choice(['<', '<=', '==', '!=', '===', '!==', '>=', '>' ]), + random.choice(['<<', '>>', '<<<', '>>>']), + random.choice(['|', '&', '^', '~^', '||', '&&']), + ]) + print(' input%s [%d:0] a;' % (random.choice(['', ' signed']), random.randint(0, 8))) + print(' input%s [%d:0] b;' % (random.choice(['', ' signed']), random.randint(0, 8))) + print(' input%s [%d:0] c;' % (random.choice(['', ' signed']), random.randint(0, 8))) + print(' input%s [%d:0] d;' % (random.choice(['', ' signed']), random.randint(0, 8))) + print(' input%s [%d:0] x;' % (random.choice(['', ' signed']), random.randint(0, 8))) + print(' input s;') + print(' output [%d:0] y;' % random.randint(0, 8)) + print(' assign y = (s ? %s(%s %s %s) : %s(%s %s %s))%s;' % + (random.choice(['', '$signed', '$unsigned']), maybe_plus_x('a'), op, maybe_plus_x('b'), + random.choice(['', '$signed', '$unsigned']), maybe_plus_x('c'), op, maybe_plus_x('d'), + random_plus_x() if random.randint(0, 4) == 0 else '')) + print('endmodule') + else: + print('module uut_%05d(a, b, x, s, y);' % (idx)) + op = random.choice(['~', '-', '!']) + print(' input%s [%d:0] a;' % (random.choice(['', ' signed']), random.randint(0, 8))) + print(' input%s [%d:0] b;' % (random.choice(['', ' signed']), random.randint(0, 8))) + print(' input%s [%d:0] x;' % (random.choice(['', ' signed']), random.randint(0, 8))) + print(' input s;') + print(' output [%d:0] y;' % random.randint(0, 8)) + print(' assign y = (s ? %s(%s%s) : %s(%s%s))%s;' % + (random.choice(['', '$signed', '$unsigned']), op, maybe_plus_x('a'), + random.choice(['', '$signed', '$unsigned']), op, maybe_plus_x('b'), + random_plus_x() if random.randint(0, 4) == 0 else '')) + print('endmodule') + with file('temp/uut_%05d.ys' % idx, 'w') as f: + with 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('tee -a temp/all_share_log.txt log') + print('tee -a temp/all_share_log.txt log #job# uut_%05d' % idx) + print('tee -a temp/all_share_log.txt wreduce') + print('tee -a temp/all_share_log.txt share -aggressive gate') + print('miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold gate miter') + print('sat -set-def-inputs -verify -prove trigger 0 -show-inputs -show-outputs miter') |