mirror of https://github.com/YosysHQ/yosys.git
84 lines
3.7 KiB
Python
84 lines
3.7 KiB
Python
#!/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(50):
|
|
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-no-timeout -timeout 20 -seq 5 -set-at 1 in_rst 1 -prove trigger 0 -prove-skip 1 -show-inputs -show-outputs miter')
|
|
|