Added smtc "final" statement

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))

examples/smtbmc/.gitignore

@@ -10,3 +10,6 @@ demo2_tb.vcd
 demo3.smt2
 demo3.vcd
 demo3.yslog
+demo4.smt2
+demo4.vcd
+demo4.yslog

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
 

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])

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