summaryrefslogtreecommitdiff
path: root/backends/smt2
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2015-10-15 15:54:59 +0200
committerClifford Wolf <clifford@clifford.at>2015-10-15 15:54:59 +0200
commit255bb914bada727806df4bdc22ab8472f03a6317 (patch)
treec17c6a477be758e4bd5823b6a1b311ed749d7127 /backends/smt2
parent5308c1e02a4867b184efd8cbb419c058032d06b4 (diff)
Progress in yosys-smtbmc
Diffstat (limited to 'backends/smt2')
-rw-r--r--backends/smt2/smtbmc.py14
1 files changed, 10 insertions, 4 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 60cd9775..db0bce4b 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -121,6 +121,7 @@ def write_vcd_model(steps):
if tempind:
+ retstatus = False
for step in range(num_steps, -1, -1):
smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
smt.write("(assert (%s_u s%d))" % (topmod, step))
@@ -140,16 +141,18 @@ if tempind:
if smt.check_sat() == "sat":
if step == 0:
- print("%s temporal induction failed!" % smt.timestamp())
+ print("%s Temporal induction failed!" % smt.timestamp())
if vcdfile is not None:
write_vcd_model(num_steps+1)
else:
- print("%s PASSED." % smt.timestamp())
+ print("%s Temporal induction successful." % smt.timestamp())
+ retstatus = True
break
else: # not tempind
+ retstatus = True
for step in range(num_steps+1):
smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
smt.write("(assert (%s_u s%d))" % (topmod, step))
@@ -176,7 +179,8 @@ else: # not tempind
if smt.check_sat() == "sat":
print("%s BMC failed!" % smt.timestamp())
if vcdfile is not None:
- write_vcd_model(steps+1)
+ write_vcd_model(step+1)
+ retstatus = False
break
else: # unsat
@@ -184,7 +188,9 @@ else: # not tempind
smt.write("(assert (%s_a s%d))" % (topmod, step))
-print("%s Done." % smt.timestamp())
smt.write("(exit)")
smt.wait()
+print("%s Status: %s" % (smt.timestamp(), "PASSED" if retstatus else "FAILED (!)"))
+sys.exit(0 if retstatus else 1)
+