riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Some syntax fixes. Generator and comma separated list modifications.

This commit is contained in:
Kaj Tuomi 2016-09-02 11:02:19 +03:00
parent 2ee9bf10d0
commit 74dd36ad55
1 changed files with 8 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
backends/smt2/smtbmc.py
View File

@ -137,7 +137,7 @@ if len(args) != 1:
if tempind and len(inconstr) != 0:
print("Error: options -i and --smtc are exclusive.");
print("Error: options -i and --smtc are exclusive.")
sys.exit(1)
@ -179,7 +179,6 @@ for fn in inconstr:
else:
assert 0
continue
continue
if tokens[0] == "state":
current_states = set()
@ -343,10 +342,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
print(" reg [%d:0] PI_%s;" % (width-1, name), file=f)
print(" %s UUT (" % topmod, file=f)
for i in range(len(primary_inputs)):
name, width = primary_inputs[i]
last_pi = i+1 == len(primary_inputs)
print(" .%s(PI_%s)%s" % (name, name, "" if last_pi else ","), file=f)
print(",\n".join(" .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f)
print(" );", file=f)
print(" initial begin", file=f)
@ -365,7 +361,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
regs = sorted(smt.hiernets(topmod, regs_only=True))
regvals = smt.get_net_bin_list(topmod, regs, "s%d" % steps_start)
print(" #1;", file=f);
print(" #1;", file=f)
for reg, val in zip(regs, regvals):
hidden_net = False
for n in reg:
@ -399,14 +395,14 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs]
pi_values = smt.get_net_bin_list(topmod, pi_names, "s%d" % i)
print(" #1;", file=f);
print(" // state %d" % i, file=f);
print(" #1;", file=f)
print(" // state %d" % i, file=f)
if i > 0:
print(" @(posedge clock);", file=f);
print(" @(posedge clock);", file=f)
for name, val in zip(pi_names, pi_values):
print(" PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f)
print(" genclock = 0;", file=f);
print(" genclock = 0;", file=f)
print(" end", file=f)
print("endmodule", file=f)
@ -445,9 +441,7 @@ def write_constr_trace(steps_start, steps_stop, index):
for j in range(ports):
addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, j))
addr_list = set()
for val in smt.get_list(addr_expr_list):
addr_list.add(smt.bv2int(val))
addr_list = set((smt.bv2int(val) for val in smt.get_list(addr_expr_list)))
expr_list = list()
for i in addr_list: