mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 11:42:30 +00:00
Code Activity

More PEP 8 fixes.

Browse source
This commit is contained in:
Kaj Tuomi 2016-09-02 13:09:09 +03:00
parent c4ba1965fd
commit d88cd0ae7f
2 changed files with 6 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

7
backends/smt2/smtbmc.py
View file

@ -419,7 +419,6 @@ def write_constr_trace(steps_start, steps_stop, index):
width = smt.modinfo[topmod].wsize[name] width = smt.modinfo[topmod].wsize[name]
primary_inputs.append((name, width)) primary_inputs.append((name, width))
if steps_start == 0: if steps_start == 0:
print("initial", file=f) print("initial", file=f)
else: 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)): 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) 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): for k in range(steps_start, steps_stop):
print("", file=f) print("", file=f)
print("state %d" % k, file=f) print("state %d" % k, file=f)
@ -558,7 +556,7 @@ if tempind:
break break
else: # not tempind else: # not tempind
step = 0 step = 0
retstatus = True retstatus = True
while step < num_steps: while step < num_steps:
@ -644,7 +642,7 @@ else: # not tempind
if not retstatus: if not retstatus:
break break
else: # gentrace else: # gentrace
for i in range(step, last_check_step+1): for i in range(step, last_check_step+1):
smt.write("(assert (%s_a s%d))" % (topmod, i)) smt.write("(assert (%s_a s%d))" % (topmod, i))
smt.write("(assert %s)" % get_constr_expr(constr_asserts, 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 (!)")) print("%s Status: %s" % (smt.timestamp(), "PASSED" if retstatus else "FAILED (!)"))
sys.exit(0 if retstatus else 1) sys.exit(0 if retstatus else 1)

6
backends/smt2/smtio.py
View file

@ -22,7 +22,8 @@ import subprocess
from select import select from select import select
from time import time from time import time
class smtmodinfo:
class SmtModInfo:
def __init__(self): def __init__(self):
self.inputs = set() self.inputs = set()
self.outputs = set() self.outputs = set()
@ -34,6 +35,7 @@ class smtmodinfo:
self.asserts = dict() self.asserts = dict()
self.anyconsts = dict() self.anyconsts = dict()
class SmtIo: class SmtIo:
def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None): def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
if opts is not None: if opts is not None:
@ -108,7 +110,7 @@ class SmtIo:
if fields[1] == "yosys-smt2-module": if fields[1] == "yosys-smt2-module":
self.curmod = fields[2] self.curmod = fields[2]
self.modinfo[self.curmod] = smtmodinfo() self.modinfo[self.curmod] = SmtModInfo()
if fields[1] == "yosys-smt2-cell": if fields[1] == "yosys-smt2-cell":
self.modinfo[self.curmod].cells[fields[3]] = fields[2] self.modinfo[self.curmod].cells[fields[3]] = fields[2]