mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 04:28:18 +00:00
Code Activity

Progress in yosys-smtbmc

Browse source
This commit is contained in:
Clifford Wolf 2015-10-15 15:54:59 +02:00
parent 5308c1e02a
commit 255bb914ba
1 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
backends/smt2/smtbmc.py
View file

@ -121,6 +121,7 @@ def write_vcd_model(steps):
if tempind: if tempind:
retstatus = False
for step in range(num_steps, -1, -1): for step in range(num_steps, -1, -1):
smt.write("(declare-fun s%d () %s_s)" % (step, topmod)) smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
smt.write("(assert (%s_u s%d))" % (topmod, step)) smt.write("(assert (%s_u s%d))" % (topmod, step))
@ -140,16 +141,18 @@ if tempind:
if smt.check_sat() == "sat": if smt.check_sat() == "sat":
if step == 0: if step == 0:
print("%s temporal induction failed!" % smt.timestamp()) print("%s Temporal induction failed!" % smt.timestamp())
if vcdfile is not None: if vcdfile is not None:
write_vcd_model(num_steps+1) write_vcd_model(num_steps+1)
else: else:
print("%s PASSED." % smt.timestamp()) print("%s Temporal induction successful." % smt.timestamp())
retstatus = True
break break
else: # not tempind else: # not tempind
retstatus = True
for step in range(num_steps+1): for step in range(num_steps+1):
smt.write("(declare-fun s%d () %s_s)" % (step, topmod)) smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
smt.write("(assert (%s_u s%d))" % (topmod, step)) smt.write("(assert (%s_u s%d))" % (topmod, step))
@ -176,7 +179,8 @@ else: # not tempind
if smt.check_sat() == "sat": if smt.check_sat() == "sat":
print("%s BMC failed!" % smt.timestamp()) print("%s BMC failed!" % smt.timestamp())
if vcdfile is not None: if vcdfile is not None:
write_vcd_model(steps+1) write_vcd_model(step+1)
retstatus = False
break break
else: # unsat else: # unsat
@ -184,7 +188,9 @@ else: # not tempind
smt.write("(assert (%s_a s%d))" % (topmod, step)) smt.write("(assert (%s_a s%d))" % (topmod, step))
print("%s Done." % smt.timestamp())
smt.write("(exit)") smt.write("(exit)")
smt.wait() smt.wait()
print("%s Status: %s" % (smt.timestamp(), "PASSED" if retstatus else "FAILED (!)"))
sys.exit(0 if retstatus else 1)