riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

More "yosys-smtbmc -c" fixes

This commit is contained in:
Clifford Wolf 2015-10-14 23:23:25 +02:00
parent 9fd0f87059
commit 5dd3e93e8f
2 changed files with 30 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
backends/smt2/smtbmc.py
View File

@ -100,7 +100,7 @@ with open(args[0], "r") as f:
smt.write(line)
def write_vcd_model():
def write_vcd_model(steps):
print("%s Writing model to VCD file." % smt.timestamp())
vcd = mkvcd(open(vcdfile, "w"))
@ -108,12 +108,12 @@ def write_vcd_model():
width = len(smt.get_net_bin(topmod, netname, "s0"))
vcd.add_net(netname, width)
for i in range(step+1):
for i in range(steps):
vcd.set_time(i)
for netname in debug_nets:
vcd.set_net(netname, smt.get_net_bin(topmod, netname, "s%d" % i))
vcd.set_time(step+1)
vcd.set_time(steps)
if tempind:
@ -138,7 +138,7 @@ if tempind:
if step == 0:
print("%s temporal induction failed!" % smt.timestamp())
if vcdfile is not None:
write_vcd_model()
write_vcd_model(num_steps+1)
else:
print("%s PASSED." % smt.timestamp())
@ -172,7 +172,7 @@ else: # not tempind
if smt.check_sat() == "sat":
print("%s BMC failed!" % smt.timestamp())
if vcdfile is not None:
write_vcd_model()
write_vcd_model(steps+1)
break
else: # unsat

29
backends/smt2/smtio.py
View File

@ -193,10 +193,9 @@ class smtio:
return worker(stmt)[0]
def bv2hex(self, v):
if v == "true": return "1"
if v == "false": return "0"
h = ""
while len(v) > 2:
v = bv2bin(v)
while len(v) > 0:
d = 0
if len(v) > 0 and v[-1] == "1": d += 1
if len(v) > 1 and v[-2] == "1": d += 2
@ -210,7 +209,29 @@ class smtio:
def bv2bin(self, v):
if v == "true": return "1"
if v == "false": return "0"
return v[2:]
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)
assert False
def get(self, expr):
self.write("(get-value (%s))" % (expr))