diff options
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smtbmc.py | 10 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 29 |
2 files changed, 30 insertions, 9 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 4f684584..65729efa 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -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 diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index acaf8f30..799efa88 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -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)) |