diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smtbmc.py | 7 | ||||
| -rw-r--r-- | 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] |