From ee3e7a0e45e764c2655391b0e444e4379c97fe3c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 24 Aug 2016 22:09:50 +0200 Subject: [PATCH] yosys-smtbmc --smtc -g --- backends/smt2/smtbmc.py | 85 +++++++++++++++----------------------- examples/smtbmc/.gitignore | 9 ++++ examples/smtbmc/Makefile | 10 ++--- 3 files changed, 48 insertions(+), 56 deletions(-) create mode 100644 examples/smtbmc/.gitignore diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 498621612..1c017df18 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -58,7 +58,7 @@ yosys-smtbmc [options] -m name of the top module - --constr + --smtc read constraints file --dump-vcd @@ -69,14 +69,14 @@ yosys-smtbmc [options] --dump-vlogtb write trace as Verilog test bench - --dump-constr + --dump-smtc write trace as constraints file """ + so.helpmsg()) sys.exit(1) 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: usage() @@ -92,13 +92,13 @@ for o, a in opts: assume_skipped = int(a) elif o == "-S": step_size = int(a) - elif o == "--constr": + elif o == "--smtc": inconstr.append(a) elif o == "--dump-vcd": vcdfile = a elif o == "--dump-vlogtb": vlogtbfile = a - elif o == "--dump-constr": + elif o == "--dump-smtc": outconstr = a elif o == "-i": tempind = True @@ -116,7 +116,7 @@ if len(args) != 1: 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) @@ -430,34 +430,6 @@ if tempind: 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 step = 0 retstatus = True @@ -495,30 +467,41 @@ else: # not tempind, not gentrace smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i)) last_check_step = step+i - if last_check_step == step: - print("%s Checking asserts in step %d.." % (smt.timestamp(), step)) - else: - print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step)) - smt.write("(push 1)") + if not gentrace: + if last_check_step == step: + print("%s Checking asserts in step %d.." % (smt.timestamp(), step)) + else: + 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)] + - [get_constr_expr(constr_asserts, 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)])) - if smt.check_sat() == "sat": - print("%s BMC failed!" % smt.timestamp()) - print_failed_asserts(topmod, "s%d" % step, topmod) - write_trace(step+step_size) - retstatus = False - break + if smt.check_sat() == "sat": + print("%s BMC failed!" % smt.timestamp()) + print_failed_asserts(topmod, "s%d" % step, topmod) + write_trace(step+step_size) + retstatus = False + break - else: # unsat smt.write("(pop 1)") - for i in range(step, last_check_step+1): - smt.write("(assert (%s_a s%d))" % (topmod, i)) - smt.write("(assert %s)" % get_constr_expr(constr_asserts, i)) + + for i in range(step, last_check_step+1): + 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 + if gentrace: + write_trace(num_steps) + smt.write("(exit)") smt.wait() diff --git a/examples/smtbmc/.gitignore b/examples/smtbmc/.gitignore new file mode 100644 index 000000000..1c9afd5ba --- /dev/null +++ b/examples/smtbmc/.gitignore @@ -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 diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile index 711be712b..a266567e4 100644 --- a/examples/smtbmc/Makefile +++ b/examples/smtbmc/Makefile @@ -6,19 +6,19 @@ demo1: demo1.smt2 yosys-smtbmc -i --dump-vcd demo1.vcd demo1.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 vvp demo2_tb +vcd=demo2_tb.vcd 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 - 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: - rm -f demo1.smt2 demo1.vcd - rm -f demo2.smt2 demo2.vcd demo2_tb.v demo2_tb demo2_tb.vcd + rm -f demo1.yslog demo1.smt2 demo1.vcd + rm -f demo2.yslog demo2.smt2 demo2.vcd demo2_tb.v demo2_tb demo2_tb.vcd demo2_tb.smtc .PHONY: demo1 clean