From 74dd36ad5555ceae0ce153e67bf26d594e9f09da Mon Sep 17 00:00:00 2001 From: Kaj Tuomi Date: Fri, 2 Sep 2016 11:02:19 +0300 Subject: [PATCH] Some syntax fixes. Generator and comma separated list modifications. --- backends/smt2/smtbmc.py | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index fa887dd15..d7f6fff24 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -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: