From 74dd36ad5555ceae0ce153e67bf26d594e9f09da Mon Sep 17 00:00:00 2001 From: Kaj Tuomi Date: Fri, 2 Sep 2016 11:02:19 +0300 Subject: [PATCH 1/7] 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: From 279298c0b85250fd0c4e3637d10f9cf24e832259 Mon Sep 17 00:00:00 2001 From: Kaj Tuomi Date: Fri, 2 Sep 2016 11:12:30 +0300 Subject: [PATCH 2/7] Fix: Unresolved reference. --- backends/smt2/smtio.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index fc7d1e13d..e5c8b231c 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -274,7 +274,7 @@ class smtio: def bv2hex(self, v): h = "" - v = bv2bin(v) + v = self.bv2bin(v) while len(v) > 0: d = 0 if len(v) > 0 and v[-1] == "1": d += 1 From 2343dda946e5ff335573c6b047d299bb90c98b1e Mon Sep 17 00:00:00 2001 From: Kaj Tuomi Date: Fri, 2 Sep 2016 12:50:23 +0300 Subject: [PATCH 3/7] Use dict lookup instead of many ifs. --- backends/smt2/smtio.py | 27 ++++++++------------------- 1 file changed, 8 insertions(+), 19 deletions(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index e5c8b231c..8db283bf7 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -292,25 +292,14 @@ class smtio: if v.startswith("#b"): return v[2:] if v.startswith("#x"): - digits = [] - for d in v[2:]: - if d == "0": digits.append("0000") - if d == "1": digits.append("0001") - if d == "2": digits.append("0010") - if d == "3": digits.append("0011") - if d == "4": digits.append("0100") - if d == "5": digits.append("0101") - if d == "6": digits.append("0110") - if d == "7": digits.append("0111") - if d == "8": digits.append("1000") - if d == "9": digits.append("1001") - if d in ("a", "A"): digits.append("1010") - if d in ("b", "B"): digits.append("1011") - if d in ("c", "C"): digits.append("1100") - if d in ("d", "D"): digits.append("1101") - if d in ("e", "E"): digits.append("1110") - if d in ("f", "F"): digits.append("1111") - return "".join(digits) + hex_dict = { + "0":"0000", "1":"0001", "2":"0010", "3":"0011", + "4":"0100", "5":"0101", "6":"0110", "7":"0111", + "8":"1000", "9":"1001", "A":"1010", "B":"1011", + "C":"1100", "D":"1101", "E":"1110", "F":"1111", + "a":"1010", "b":"1011", "c":"1100", "d":"1101", + "e":"1110", "f":"1111"} + return "".join(hex_dict.get(x) for x in v[2:]) assert False def bv2int(self, v): From c4ba1965fd4300cb7de48cde996bb068d951967d Mon Sep 17 00:00:00 2001 From: Kaj Tuomi Date: Fri, 2 Sep 2016 13:01:31 +0300 Subject: [PATCH 4/7] Indentation and PEP 8 fixes. CamelCase and white space after semicolon. --- backends/smt2/smtbmc.py | 8 ++++---- backends/smt2/smtio.py | 18 +++++++++--------- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index d7f6fff24..225ca01eb 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -19,7 +19,7 @@ import os, sys, getopt, re ##yosys-sys-path## -from smtio import smtio, smtopts, mkvcd +from smtio import SmtIo, SmtOpts, MkVcd from collections import defaultdict skip_steps = 0 @@ -35,7 +35,7 @@ dumpall = False assume_skipped = None final_only = False topmod = None -so = smtopts() +so = SmtOpts() def usage(): @@ -274,7 +274,7 @@ def get_constr_expr(db, state, final=False, getvalues=False): return "(and %s)" % " ".join(expr_list) -smt = smtio(opts=so) +smt = SmtIo(opts=so) print("%s Solver: %s" % (smt.timestamp(), so.solver)) smt.setup("QF_AUFBV") @@ -296,7 +296,7 @@ def write_vcd_trace(steps_start, steps_stop, index): print("%s Writing trace to VCD file: %s" % (smt.timestamp(), filename)) with open(filename, "w") as vcd_file: - vcd = mkvcd(vcd_file) + vcd = MkVcd(vcd_file) path_list = list() for netpath in sorted(smt.hiernets(topmod)): diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 8db283bf7..8f8dec026 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -34,7 +34,7 @@ class smtmodinfo: self.asserts = dict() self.anyconsts = dict() -class smtio: +class SmtIo: def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None): if opts is not None: self.solver = opts.solver @@ -293,12 +293,12 @@ class smtio: return v[2:] if v.startswith("#x"): hex_dict = { - "0":"0000", "1":"0001", "2":"0010", "3":"0011", - "4":"0100", "5":"0101", "6":"0110", "7":"0111", - "8":"1000", "9":"1001", "A":"1010", "B":"1011", - "C":"1100", "D":"1101", "E":"1110", "F":"1111", - "a":"1010", "b":"1011", "c":"1100", "d":"1101", - "e":"1110", "f":"1111"} + "0": "0000", "1": "0001", "2": "0010", "3": "0011", + "4": "0100", "5": "0101", "6": "0110", "7": "0111", + "8": "1000", "9": "1001", "A": "1010", "B": "1011", + "C": "1100", "D": "1101", "E": "1110", "F": "1111", + "a": "1010", "b": "1011", "c": "1100", "d": "1101", + "e": "1110", "f": "1111"} return "".join(hex_dict.get(x) for x in v[2:]) assert False @@ -395,7 +395,7 @@ class smtio: self.p.wait() -class smtopts: +class SmtOpts: def __init__(self): self.shortopts = "s:v" self.longopts = ["no-progress", "dump-smt2="] @@ -434,7 +434,7 @@ class smtopts: """ -class mkvcd: +class MkVcd: def __init__(self, f): self.f = f self.t = -1 From d88cd0ae7f8761637722d5d2c6cc1c8bac762ce3 Mon Sep 17 00:00:00 2001 From: Kaj Tuomi Date: Fri, 2 Sep 2016 13:09:09 +0300 Subject: [PATCH 5/7] More PEP 8 fixes. --- backends/smt2/smtbmc.py | 7 ++----- backends/smt2/smtio.py | 6 ++++-- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 225ca01eb..1de0b2a30 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -419,7 +419,6 @@ def write_constr_trace(steps_start, steps_stop, index): width = smt.modinfo[topmod].wsize[name] primary_inputs.append((name, width)) - if steps_start == 0: print("initial", file=f) else: @@ -450,7 +449,6 @@ def write_constr_trace(steps_start, steps_stop, index): for i, val in zip(addr_list, smt.get_list(expr_list)): print("assume (= (select [%s] #b%s) %s)" % (".".join(mempath), format(i, "0%db" % abits), val), file=f) - for k in range(steps_start, steps_stop): print("", file=f) print("state %d" % k, file=f) @@ -558,7 +556,7 @@ if tempind: break -else: # not tempind +else: # not tempind step = 0 retstatus = True while step < num_steps: @@ -644,7 +642,7 @@ else: # not tempind if not retstatus: break - else: # gentrace + else: # gentrace for i in range(step, last_check_step+1): smt.write("(assert (%s_a s%d))" % (topmod, i)) smt.write("(assert %s)" % get_constr_expr(constr_asserts, i)) @@ -671,4 +669,3 @@ smt.wait() print("%s Status: %s" % (smt.timestamp(), "PASSED" if retstatus else "FAILED (!)")) sys.exit(0 if retstatus else 1) - diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 8f8dec026..56ae8dcfe 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -22,7 +22,8 @@ import subprocess from select import select from time import time -class smtmodinfo: + +class SmtModInfo: def __init__(self): self.inputs = set() self.outputs = set() @@ -34,6 +35,7 @@ class smtmodinfo: self.asserts = dict() self.anyconsts = dict() + class SmtIo: def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None): if opts is not None: @@ -108,7 +110,7 @@ class SmtIo: if fields[1] == "yosys-smt2-module": self.curmod = fields[2] - self.modinfo[self.curmod] = smtmodinfo() + self.modinfo[self.curmod] = SmtModInfo() if fields[1] == "yosys-smt2-cell": self.modinfo[self.curmod].cells[fields[3]] = fields[2] From 948aac9e1eaed04aa8de08e62cfb078d6337e9c9 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 2 Sep 2016 13:46:56 +0200 Subject: [PATCH 6/7] Don't re-create hex_dict for each value --- backends/smt2/smtio.py | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 56ae8dcfe..dad63e567 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -23,6 +23,16 @@ from select import select from time import time +hex_dict = { + "0": "0000", "1": "0001", "2": "0010", "3": "0011", + "4": "0100", "5": "0101", "6": "0110", "7": "0111", + "8": "1000", "9": "1001", "A": "1010", "B": "1011", + "C": "1100", "D": "1101", "E": "1110", "F": "1111", + "a": "1010", "b": "1011", "c": "1100", "d": "1101", + "e": "1110", "f": "1111" +} + + class SmtModInfo: def __init__(self): self.inputs = set() @@ -294,13 +304,6 @@ class SmtIo: if v.startswith("#b"): return v[2:] if v.startswith("#x"): - hex_dict = { - "0": "0000", "1": "0001", "2": "0010", "3": "0011", - "4": "0100", "5": "0101", "6": "0110", "7": "0111", - "8": "1000", "9": "1001", "A": "1010", "B": "1011", - "C": "1100", "D": "1101", "E": "1110", "F": "1111", - "a": "1010", "b": "1011", "c": "1100", "d": "1101", - "e": "1110", "f": "1111"} return "".join(hex_dict.get(x) for x in v[2:]) assert False From 068d5bc02ffea9ba627bbf7151fdb36500eae0f2 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 2 Sep 2016 13:54:24 +0200 Subject: [PATCH 7/7] Made examples/smtbmc/demo1.v more interesting --- examples/smtbmc/demo1.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v index d9be41513..567dde148 100644 --- a/examples/smtbmc/demo1.v +++ b/examples/smtbmc/demo1.v @@ -9,7 +9,7 @@ module demo1(input clk, input addtwo, output iseven); `ifdef FORMAL assert property (cnt != 15); - initial assume (!cnt[3] && !cnt[0]); + initial assume (!cnt[2]); `endif endmodule