summaryrefslogtreecommitdiff
path: root/tests/fsm
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2015-03-20 09:10:02 +0100
committerClifford Wolf <clifford@clifford.at>2015-03-20 09:10:02 +0100
commit604c097f9818a5b29fa06223b88930630fafca5e (patch)
treec2e0242bc6ec0cd913ab1ff298c6e570af1397c5 /tests/fsm
parentaed4d763cf40c6341f5a53eb856a940ace4b15e7 (diff)
fix for python 2.6.6
Diffstat (limited to 'tests/fsm')
-rw-r--r--tests/fsm/generate.py146
1 files changed, 74 insertions, 72 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'))