mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 19:52:31 +00:00
yosys-smtbmc --smtc -g
This commit is contained in:
Clifford Wolf
parent
cd18235f30
commit
ee3e7a0e45
3 changed files with 48 additions and 56 deletions
|
|
@ -58,7 +58,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
|
||||||
-m <module_name>
|
-m <module_name>
|
||||||
name of the top module
|
name of the top module
|
||||||
|
|
||||||
--constr <constr_filename>
|
--smtc <constr_filename>
|
||||||
read constraints file
|
read constraints file
|
||||||
|
|
||||||
--dump-vcd <vcd_filename>
|
--dump-vcd <vcd_filename>
|
||||||
|
|
@ -69,14 +69,14 @@ yosys-smtbmc [options] <yosys_smt2_output>
|
||||||
--dump-vlogtb <verilog_filename>
|
--dump-vlogtb <verilog_filename>
|
||||||
write trace as Verilog test bench
|
write trace as Verilog test bench
|
||||||
|
|
||||||
--dump-constr <constr_filename>
|
--dump-smtc <constr_filename>
|
||||||
write trace as constraints file
|
write trace as constraints file
|
||||||
""" + so.helpmsg())
|
""" + so.helpmsg())
|
||||||
sys.exit(1)
|
sys.exit(1)
|
||||||
|
|
||||||
|
|
||||||
try:
|
try:
|
||||||
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:igm:", so.longopts + ["constr=", "dump-vcd=", "dump-vlogtb=", "dump-constr="])
|
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:igm:", so.longopts + ["smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc="])
|
||||||
except:
|
except:
|
||||||
usage()
|
usage()
|
||||||
|
|
||||||
|
|
@ -92,13 +92,13 @@ for o, a in opts:
|
||||||
assume_skipped = int(a)
|
assume_skipped = int(a)
|
||||||
elif o == "-S":
|
elif o == "-S":
|
||||||
step_size = int(a)
|
step_size = int(a)
|
||||||
elif o == "--constr":
|
elif o == "--smtc":
|
||||||
inconstr.append(a)
|
inconstr.append(a)
|
||||||
elif o == "--dump-vcd":
|
elif o == "--dump-vcd":
|
||||||
vcdfile = a
|
vcdfile = a
|
||||||
elif o == "--dump-vlogtb":
|
elif o == "--dump-vlogtb":
|
||||||
vlogtbfile = a
|
vlogtbfile = a
|
||||||
elif o == "--dump-constr":
|
elif o == "--dump-smtc":
|
||||||
outconstr = a
|
outconstr = a
|
||||||
elif o == "-i":
|
elif o == "-i":
|
||||||
tempind = True
|
tempind = True
|
||||||
|
|
@ -116,7 +116,7 @@ if len(args) != 1:
|
||||||
|
|
||||||
|
|
||||||
if tempind and len(inconstr) != 0:
|
if tempind and len(inconstr) != 0:
|
||||||
print("Error: options -i and --constr are exclusive.");
|
print("Error: options -i and --smtc are exclusive.");
|
||||||
sys.exit(1)
|
sys.exit(1)
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -430,34 +430,6 @@ if tempind:
|
||||||
break
|
break
|
||||||
|
|
||||||
|
|
||||||
elif gentrace:
|
|
||||||
retstatus = True
|
|
||||||
for step in range(num_steps):
|
|
||||||
smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
|
|
||||||
smt.write("(assert (%s_u s%d))" % (topmod, step))
|
|
||||||
smt.write("(assert (%s_a s%d))" % (topmod, step))
|
|
||||||
smt.write("(assert (%s_h s%d))" % (topmod, step))
|
|
||||||
smt.write("(assert %s)" % get_constr_expr(constr_asserts, step))
|
|
||||||
smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
|
|
||||||
|
|
||||||
if step == 0:
|
|
||||||
smt.write("(assert (%s_i s0))" % (topmod))
|
|
||||||
smt.write("(assert (%s_is s0))" % (topmod))
|
|
||||||
|
|
||||||
else:
|
|
||||||
smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step))
|
|
||||||
smt.write("(assert (not (%s_is s%d)))" % (topmod, step))
|
|
||||||
|
|
||||||
print("%s Creating trace of length %d.." % (smt.timestamp(), num_steps))
|
|
||||||
|
|
||||||
if smt.check_sat() == "sat":
|
|
||||||
write_trace(num_steps)
|
|
||||||
|
|
||||||
else:
|
|
||||||
print("%s Creating trace failed!" % smt.timestamp())
|
|
||||||
retstatus = False
|
|
||||||
|
|
||||||
|
|
||||||
else: # not tempind, not gentrace
|
else: # not tempind, not gentrace
|
||||||
step = 0
|
step = 0
|
||||||
retstatus = True
|
retstatus = True
|
||||||
|
|
@ -495,30 +467,41 @@ else: # not tempind, not gentrace
|
||||||
smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i))
|
smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i))
|
||||||
last_check_step = step+i
|
last_check_step = step+i
|
||||||
|
|
||||||
if last_check_step == step:
|
if not gentrace:
|
||||||
print("%s Checking asserts in step %d.." % (smt.timestamp(), step))
|
if last_check_step == step:
|
||||||
else:
|
print("%s Checking asserts in step %d.." % (smt.timestamp(), step))
|
||||||
print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step))
|
else:
|
||||||
smt.write("(push 1)")
|
print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step))
|
||||||
|
smt.write("(push 1)")
|
||||||
|
|
||||||
smt.write("(assert (not (and %s)))" % " ".join(["(%s_a s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
|
smt.write("(assert (not (and %s)))" % " ".join(["(%s_a s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
|
||||||
[get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
|
[get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
|
||||||
|
|
||||||
if smt.check_sat() == "sat":
|
if smt.check_sat() == "sat":
|
||||||
print("%s BMC failed!" % smt.timestamp())
|
print("%s BMC failed!" % smt.timestamp())
|
||||||
print_failed_asserts(topmod, "s%d" % step, topmod)
|
print_failed_asserts(topmod, "s%d" % step, topmod)
|
||||||
write_trace(step+step_size)
|
write_trace(step+step_size)
|
||||||
retstatus = False
|
retstatus = False
|
||||||
break
|
break
|
||||||
|
|
||||||
else: # unsat
|
|
||||||
smt.write("(pop 1)")
|
smt.write("(pop 1)")
|
||||||
for i in range(step, last_check_step+1):
|
|
||||||
smt.write("(assert (%s_a s%d))" % (topmod, i))
|
for i in range(step, last_check_step+1):
|
||||||
smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
|
smt.write("(assert (%s_a s%d))" % (topmod, i))
|
||||||
|
smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
|
||||||
|
|
||||||
|
if gentrace:
|
||||||
|
print("%s Solving for step %d.." % (smt.timestamp(), step))
|
||||||
|
if smt.check_sat() != "sat":
|
||||||
|
print("%s No solution found!" % smt.timestamp())
|
||||||
|
retstatus = False
|
||||||
|
break
|
||||||
|
|
||||||
step += step_size
|
step += step_size
|
||||||
|
|
||||||
|
if gentrace:
|
||||||
|
write_trace(num_steps)
|
||||||
|
|
||||||
|
|
||||||
smt.write("(exit)")
|
smt.write("(exit)")
|
||||||
smt.wait()
|
smt.wait()
|
||||||
|
|
|
||||||
9
examples/smtbmc/.gitignore
vendored
Normal file
9
examples/smtbmc/.gitignore
vendored
Normal file
|
|
@ -0,0 +1,9 @@
|
||||||
|
demo1.smt2
|
||||||
|
demo1.yslog
|
||||||
|
demo2.smt2
|
||||||
|
demo2.vcd
|
||||||
|
demo2.yslog
|
||||||
|
demo2_tb
|
||||||
|
demo2_tb.smtc
|
||||||
|
demo2_tb.v
|
||||||
|
demo2_tb.vcd
|
||||||
|
|
@ -6,19 +6,19 @@ demo1: demo1.smt2
|
||||||
yosys-smtbmc -i --dump-vcd demo1.vcd demo1.smt2
|
yosys-smtbmc -i --dump-vcd demo1.vcd demo1.smt2
|
||||||
|
|
||||||
demo2: demo2.smt2
|
demo2: demo2.smt2
|
||||||
yosys-smtbmc -g --dump-vcd demo2.vcd --dump-vlogtb demo2_tb.v --dump-constr demo2.smtc demo2.smt2
|
yosys-smtbmc -g --dump-vcd demo2.vcd --dump-vlogtb demo2_tb.v --dump-smtc demo2_tb.smtc demo2.smt2
|
||||||
iverilog -g2012 -o demo2_tb demo2_tb.v demo2.v
|
iverilog -g2012 -o demo2_tb demo2_tb.v demo2.v
|
||||||
vvp demo2_tb +vcd=demo2_tb.vcd
|
vvp demo2_tb +vcd=demo2_tb.vcd
|
||||||
|
|
||||||
demo1.smt2: demo1.v
|
demo1.smt2: demo1.v
|
||||||
yosys -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires -mem -bv demo1.smt2'
|
yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires -mem -bv demo1.smt2'
|
||||||
|
|
||||||
demo2.smt2: demo2.v
|
demo2.smt2: demo2.v
|
||||||
yosys -p 'read_verilog -formal demo2.v; prep -top demo2 -nordff; write_smt2 -wires -mem -bv demo2.smt2'
|
yosys -ql demo2.yslog -p 'read_verilog -formal demo2.v; prep -top demo2 -nordff; write_smt2 -wires -mem -bv demo2.smt2'
|
||||||
|
|
||||||
clean:
|
clean:
|
||||||
rm -f demo1.smt2 demo1.vcd
|
rm -f demo1.yslog demo1.smt2 demo1.vcd
|
||||||
rm -f demo2.smt2 demo2.vcd demo2_tb.v demo2_tb demo2_tb.vcd
|
rm -f demo2.yslog demo2.smt2 demo2.vcd demo2_tb.v demo2_tb demo2_tb.vcd demo2_tb.smtc
|
||||||
|
|
||||||
.PHONY: demo1 clean
|
.PHONY: demo1 clean
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue