diff options
| -rw-r--r-- | backends/smt2/smtbmc.py | 57 | ||||
| -rw-r--r-- | examples/smtbmc/.gitignore | 3 | ||||
| -rw-r--r-- | examples/smtbmc/Makefile | 11 | ||||
| -rw-r--r-- | examples/smtbmc/demo4.smtc | 11 | ||||
| -rw-r--r-- | examples/smtbmc/demo4.v | 13 |
5 files changed, 86 insertions, 9 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 9dba68b2a..90936bc3c 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -121,6 +121,7 @@ if tempind and len(inconstr) != 0: sys.exit(1) +constr_final_start = None constr_asserts = defaultdict(list) constr_assumes = defaultdict(list) @@ -142,6 +143,21 @@ for fn in inconstr: current_states.add(0) continue + if tokens[0] == "final": + constr_final = True + if len(tokens) == 1: + current_states = set(["final-%d" % i for i in range(0, num_steps+1)]) + constr_final_start = 0 + elif len(tokens) == 2: + i = int(tokens[1]) + assert i < 0 + current_states = set(["final-%d" % i for i in range(-i, num_steps+1)]) + constr_final_start = -i if constr_final_start is None else min(constr_final_start, -i) + else: + assert 0 + continue + continue + if tokens[0] == "state": current_states = set() for token in tokens[1:]: @@ -190,9 +206,13 @@ for fn in inconstr: assert 0 -def get_constr_expr(db, state): - if state not in db: - return "true" +def get_constr_expr(db, state, final=False): + if final: + if ("final-%d" % state) not in db: + return "true" + else: + if state not in db: + return "true" netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]+)\](?=[ )]|$)') @@ -211,7 +231,7 @@ def get_constr_expr(db, state): return match.group(1) + expr expr_list = list() - for expr in db[state]: + for expr in db[("final-%d" % state) if final else state]: expr = netref_regex.sub(replace_netref, expr) expr_list.append(expr) @@ -530,9 +550,32 @@ else: # not tempind 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)) + if constr_final_start is not None: + for i in range(step, last_check_step+1): + if i < constr_final_start: + continue + + print("%s Checking final constraints in step %d.." % (smt.timestamp(), i)) + smt.write("(push 1)") + + smt.write("(assert %s)" % get_constr_expr(constr_assumes, i, final=True)) + smt.write("(assert (not %s))" % get_constr_expr(constr_asserts, i, final=True)) + + if smt.check_sat() == "sat": + print("%s BMC failed!" % smt.timestamp()) + print_failed_asserts(topmod, "s%d" % i, topmod) + write_trace(i) + retstatus = False + break + + smt.write("(pop 1)") + if not retstatus: + break + + if constr_final_start is None: + 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)) diff --git a/examples/smtbmc/.gitignore b/examples/smtbmc/.gitignore index bf83e0d44..fbddafa8a 100644 --- a/examples/smtbmc/.gitignore +++ b/examples/smtbmc/.gitignore @@ -10,3 +10,6 @@ demo2_tb.vcd demo3.smt2 demo3.vcd demo3.yslog +demo4.smt2 +demo4.vcd +demo4.yslog diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile index b3feb07c7..588e8429b 100644 --- a/examples/smtbmc/Makefile +++ b/examples/smtbmc/Makefile @@ -1,5 +1,5 @@ -all: demo1 demo2 demo3 +all: demo1 demo2 demo3 demo4 demo1: demo1.smt2 yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2 @@ -13,6 +13,9 @@ demo2: demo2.smt2 demo3: demo3.smt2 yosys-smtbmc --dump-vcd demo3.vcd --smtc demo3.smtc demo3.smt2 +demo4: demo4.smt2 + yosys-smtbmc -s yices --dump-vcd demo4.vcd --smtc demo4.smtc demo4.smt2 + demo1.smt2: demo1.v yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires -mem -bv demo1.smt2' @@ -22,10 +25,14 @@ demo2.smt2: demo2.v demo3.smt2: demo3.v yosys -ql demo3.yslog -p 'read_verilog -formal demo3.v; prep -top demo3 -nordff; write_smt2 -wires -mem -bv demo3.smt2' +demo4.smt2: demo4.v + yosys -ql demo4.yslog -p 'read_verilog -formal demo4.v; prep -top demo4 -nordff; write_smt2 -wires -mem -bv demo4.smt2' + clean: rm -f demo1.yslog demo1.smt2 demo1.vcd rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd rm -f demo3.yslog demo3.smt2 demo3.vcd + rm -f demo4.yslog demo4.smt2 demo4.vcd -.PHONY: demo1 demo2 demo3 clean +.PHONY: demo1 demo2 demo3 demo4 clean diff --git a/examples/smtbmc/demo4.smtc b/examples/smtbmc/demo4.smtc new file mode 100644 index 000000000..2f91f8164 --- /dev/null +++ b/examples/smtbmc/demo4.smtc @@ -0,0 +1,11 @@ +initial +assume [rst] + +always -1 +assume (not [rst]) +assume (=> [-1:inv2] [inv2]) + +final -2 +assume [-1:inv2] +assume (not [-2:inv2]) +assert (= [r1] [r2]) diff --git a/examples/smtbmc/demo4.v b/examples/smtbmc/demo4.v new file mode 100644 index 000000000..3f1b47277 --- /dev/null +++ b/examples/smtbmc/demo4.v @@ -0,0 +1,13 @@ +// Demo for "final" smtc constraints + +module demo4(input clk, rst, inv2, input [15:0] in, output reg [15:0] r1, r2); + always @(posedge clk) begin + if (rst) begin + r1 <= in; + r2 <= -in; + end else begin + r1 <= r1 + in; + r2 <= inv2 ? -(r2 - in) : (r2 - in); + end + end +endmodule |