Some syntax fixes. Generator and comma separated list modifications.

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index fa887dd1540b09f2d9260359ed458e9dc8b57a54..d7f6fff242ad731a61b00058d3c6756a52b27f6c 100644 (file)
--- 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: