Add smtbmc support for exist-forall problems

Signed-off-by: Clifford Wolf <clifford@clifford.at>

3 files changed, 334 insertions, 87 deletions

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index a401cacb7..124364120 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -32,9 +32,9 @@ struct Smt2Worker
 	CellTypes ct;
 	SigMap sigmap;
 	RTLIL::Module *module;
-	bool bvmode, memmode, wiresmode, verbose, statebv, statedt;
+	bool bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode;
 	dict<IdString, int> &mod_stbv_width;
-	int idcounter, statebv_width;
+	int idcounter = 0, statebv_width = 0;
 
 	std::vector<std::string> decls, trans, hier, dtmembers;
 	std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
@@ -42,6 +42,7 @@ struct Smt2Worker
 	pool<Cell*> recursive_cells, registers;
 
 	pool<SigBit> clock_posedge, clock_negedge;
+	vector<string> ex_state_eq, ex_input_eq;
 
 	std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
 	std::map<Cell*, int> memarrays;
@@ -106,10 +107,10 @@ struct Smt2Worker
 			decls.push_back(decl_str + "\n");
 	}
 
-	Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt,
+	Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, bool forallmode,
 			dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache) :
 			ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
-			verbose(verbose), statebv(statebv), statedt(statedt), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0)
+			verbose(verbose), statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width)
 	{
 		pool<SigBit> noclock;
 
@@ -507,14 +508,16 @@ struct Smt2Worker
 				return;
 			}
 
-			if (cell->type.in("$anyconst", "$anyseq"))
+			if (cell->type.in("$anyconst", "$anyseq", "$allconst", "$allseq"))
 			{
 				registers.insert(cell);
 				string infostr = cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell);
 				if (cell->attributes.count("\\reg"))
 					infostr += " " + cell->attributes.at("\\reg").decode_string();
-				decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, infostr.c_str()));
+				decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort("\\Y")), infostr.c_str()));
 				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
+				if (cell->type == "$anyseq")
+					ex_input_eq.push_back(stringf("  (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
 				register_bv(cell->getPort("\\Y"), idcounter++);
 				recursive_cells.erase(cell);
 				return;
@@ -787,14 +790,24 @@ struct Smt2Worker
 				if (bvmode && GetSize(sig) > 1) {
 					decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
 							get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str()));
+					if (wire->port_input)
+						ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
+								get_id(module), get_id(wire), get_id(module), get_id(wire)));
 				} else {
 					for (int i = 0; i < GetSize(sig); i++)
-						if (GetSize(sig) > 1)
+						if (GetSize(sig) > 1) {
 							decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
 									get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str()));
-						else
+							if (wire->port_input)
+								ex_input_eq.push_back(stringf("  (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))",
+										get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
+						} else {
 							decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
 									get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str()));
+							if (wire->port_input)
+								ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
+										get_id(module), get_id(wire), get_id(module), get_id(wire)));
+						}
 				}
 			}
 		}
@@ -919,6 +932,7 @@ struct Smt2Worker
 					std::string expr_d = get_bool(cell->getPort("\\D"));
 					std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
 					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
+					ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort("\\Q")).c_str(), get_bool(cell->getPort("\\Q"), "other_state").c_str()));
 				}
 
 				if (cell->type.in("$ff", "$dff"))
@@ -926,13 +940,16 @@ struct Smt2Worker
 					std::string expr_d = get_bv(cell->getPort("\\D"));
 					std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
 					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
+					ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Q")).c_str(), get_bv(cell->getPort("\\Q"), "other_state").c_str()));
 				}
 
-				if (cell->type == "$anyconst")
+				if (cell->type.in("$anyconst", "$allconst"))
 				{
 					std::string expr_d = get_bv(cell->getPort("\\Y"));
 					std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state");
 					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y"))));
+					if (cell->type == "$anyconst")
+						ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Y")).c_str(), get_bv(cell->getPort("\\Y"), "other_state").c_str()));
 				}
 
 				if (cell->type == "$mem")
@@ -1044,6 +1061,7 @@ struct Smt2Worker
 					std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports);
 					std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
 					trans.push_back(stringf("  (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell)));
+					ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid));
 
 					if (async_read)
 						hier.push_back(stringf("  (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell)));
@@ -1086,6 +1104,37 @@ struct Smt2Worker
 			hier.push_back(stringf("  (|%s_h| (|%s_h %s| state))\n", get_id(c->type), get_id(module), get_id(c->name)));
 			trans.push_back(stringf("  (|%s_t| (|%s_h %s| state) (|%s_h %s| next_state))\n",
 					get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name)));
+			ex_state_eq.push_back(stringf("(|%s_ex_state_eq| (|%s_h %s| state) (|%s_h %s| other_state))\n",
+					get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name)));
+		}
+
+		if (forallmode)
+		{
+			string expr = ex_state_eq.empty() ? "true" : "(and";
+			if (!ex_state_eq.empty()) {
+				if (GetSize(ex_state_eq) == 1) {
+					expr = "\n  " + ex_state_eq.front() + "\n";
+				} else {
+					for (auto &str : ex_state_eq)
+						expr += stringf("\n  %s", str.c_str());
+					expr += "\n)";
+				}
+			}
+			decls.push_back(stringf("(define-fun |%s_ex_state_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n",
+				get_id(module), get_id(module), get_id(module), expr.c_str()));
+
+			expr = ex_input_eq.empty() ? "true" : "(and";
+			if (!ex_input_eq.empty()) {
+				if (GetSize(ex_input_eq) == 1) {
+					expr = "\n  " + ex_input_eq.front() + "\n";
+				} else {
+					for (auto &str : ex_input_eq)
+						expr += stringf("\n  %s", str.c_str());
+					expr += "\n)";
+				}
+			}
+			decls.push_back(stringf("(define-fun |%s_ex_input_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n",
+				get_id(module), get_id(module), get_id(module), expr.c_str()));
 		}
 
 		string assert_expr = assert_list.empty() ? "true" : "(and";
@@ -1336,6 +1385,7 @@ struct Smt2Backend : public Backend {
 	{
 		std::ifstream template_f;
 		bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;
+		bool forallmode = false;
 
 		log_header(design, "Executing SMT2 backend.\n");
 
@@ -1444,13 +1494,25 @@ struct Smt2Backend : public Backend {
 		std::string topmod_id;
 
 		for (auto module : sorted_modules)
+			for (auto cell : module->cells())
+				if (cell->type.in("$allconst", "$allseq"))
+					goto found_forall;
+		if (0) {
+	found_forall:
+			forallmode = true;
+			*f << stringf("; yosys-smt2-forall\n");
+			if (!statebv && !statedt)
+				log_error("Forall-exists problems are only supported in -stbv or -stdt mode.\n");
+		}
+
+		for (auto module : sorted_modules)
 		{
 			if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn())
 				continue;
 
 			log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
 
-			Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width, mod_clk_cache);
+			Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode, mod_stbv_width, mod_clk_cache);
 			worker.run();
 			worker.write(*f);
 
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 047fb6cde..4ad940551 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -983,7 +983,7 @@ def print_anyconsts_worker(mod, state, path):
 
     for fun, info in smt.modinfo[mod].anyconsts.items():
         if info[1] is None:
-            print_msg("Value for anyconst in %s (%s): %d" % (path, info, smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+            print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
         else:
             print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
 
@@ -1010,24 +1010,160 @@ def get_cover_list(mod, base):
 
     return cover_expr, cover_desc
 
+states = list()
+asserts_antecedent_cache = [list()]
+asserts_consequent_cache = [list()]
+asserts_cache_dirty = False
+
+def smt_state(step):
+    smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
+    states.append("s%d" % step)
+
+def smt_assert_antecedent(expr):
+    if expr == "true":
+        return
+
+    smt.write("(assert %s)" % expr)
+
+    global asserts_cache_dirty
+    asserts_cache_dirty = True
+    asserts_antecedent_cache[-1].append(expr)
+
+def smt_assert_consequent(expr):
+    if expr == "true":
+        return
+
+    smt.write("(assert %s)" % expr)
+
+    global asserts_cache_dirty
+    asserts_cache_dirty = True
+    asserts_consequent_cache[-1].append(expr)
+
+def smt_forall_assert():
+    if not smt.forall:
+        return
+
+    global asserts_cache_dirty
+    asserts_cache_dirty = False
+
+    def make_assert_expr(asserts_cache):
+        expr = list()
+        for lst in asserts_cache:
+            expr += lst
+
+        assert len(expr) != 0
+
+        if len(expr) == 1:
+            expr = expr[0]
+        else:
+            expr = "(and %s)" % (" ".join(expr))
+        return expr
+
+    antecedent_expr = make_assert_expr(asserts_antecedent_cache)
+    consequent_expr = make_assert_expr(asserts_consequent_cache)
+
+    states_db = set(states)
+    used_states_db = set()
+    new_antecedent_expr = list()
+    new_consequent_expr = list()
+    assert_expr = list()
+
+    def make_new_expr(new_expr, expr):
+        cursor = 0
+        while cursor < len(expr):
+            l = 1
+            if expr[cursor] in '|"':
+                while cursor+l+1 < len(expr) and expr[cursor] != expr[cursor+l]:
+                    l += 1
+                l += 1
+            elif expr[cursor] not in '() ':
+                while cursor+l < len(expr) and expr[cursor+l] not in '|"() ':
+                    l += 1
+
+            word = expr[cursor:cursor+l]
+            if word in states_db:
+                used_states_db.add(word)
+                word += "_"
+
+            new_expr.append(word)
+            cursor += l
+
+    make_new_expr(new_antecedent_expr, antecedent_expr)
+    make_new_expr(new_consequent_expr, consequent_expr)
+
+    new_antecedent_expr = ["".join(new_antecedent_expr)]
+    new_consequent_expr = ["".join(new_consequent_expr)]
+
+    if states[0] in used_states_db:
+        new_antecedent_expr.append("(|%s_ex_state_eq| %s %s_)" % (topmod, states[0], states[0]))
+    for s in states:
+        if s in used_states_db:
+            new_antecedent_expr.append("(|%s_ex_input_eq| %s %s_)" % (topmod, s, s))
+
+    if len(new_antecedent_expr) == 0:
+        new_antecedent_expr = "true"
+    elif len(new_antecedent_expr) == 1:
+        new_antecedent_expr = new_antecedent_expr[0]
+    else:
+        new_antecedent_expr = "(and %s)" % (" ".join(new_antecedent_expr))
+
+    if len(new_consequent_expr) == 0:
+        new_consequent_expr = "true"
+    elif len(new_consequent_expr) == 1:
+        new_consequent_expr = new_consequent_expr[0]
+    else:
+        new_consequent_expr = "(and %s)" % (" ".join(new_consequent_expr))
+
+    assert_expr.append("(assert (forall (")
+    first_state = True
+    for s in states:
+        if s in used_states_db:
+            assert_expr.append("%s(%s_ |%s_s|)" % ("" if first_state else " ", s, topmod))
+            first_state = False
+    assert_expr.append(") (=> %s %s)))" % (new_antecedent_expr, new_consequent_expr))
+
+    smt.write("".join(assert_expr))
+
+def smt_push():
+    global asserts_cache_dirty
+    asserts_cache_dirty = True
+    asserts_antecedent_cache.append(list())
+    asserts_consequent_cache.append(list())
+    smt.write("(push 1)")
+
+def smt_pop():
+    global asserts_cache_dirty
+    asserts_cache_dirty = True
+    asserts_antecedent_cache.pop()
+    asserts_consequent_cache.pop()
+    smt.write("(pop 1)")
+
+def smt_check_sat():
+    if asserts_cache_dirty:
+        smt_forall_assert()
+    return smt.check_sat()
 
 if tempind:
     retstatus = False
     skip_counter = step_size
     for step in range(num_steps, -1, -1):
-        smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
-        smt.write("(assert (|%s_u| s%d))" % (topmod, step))
-        smt.write("(assert (|%s_h| s%d))" % (topmod, step))
-        smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
-        smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
+        if smt.forall:
+            print_msg("Temporal induction not supported for exists-forall problems.")
+            break
+
+        smt_state(step)
+        smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
+        smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
+        smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
+        smt_assert_consequent(get_constr_expr(constr_assumes, step))
 
         if step == num_steps:
-            smt.write("(assert (not (and (|%s_a| s%d) %s)))" % (topmod, step, get_constr_expr(constr_asserts, step)))
+            smt_assert_consequent("(not (and (|%s_a| s%d) %s))" % (topmod, step, get_constr_expr(constr_asserts, step)))
 
         else:
-            smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step, step+1))
-            smt.write("(assert (|%s_a| s%d))" % (topmod, step))
-            smt.write("(assert %s)" % get_constr_expr(constr_asserts, step))
+            smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step, step+1))
+            smt_assert_consequent("(|%s_a| s%d)" % (topmod, step))
+            smt_assert_consequent(get_constr_expr(constr_asserts, step))
 
         if step > num_steps-skip_steps:
             print_msg("Skipping induction in step %d.." % (step))
@@ -1041,9 +1177,9 @@ if tempind:
         skip_counter = 0
         print_msg("Trying induction in step %d.." % (step))
 
-        if smt.check_sat() == "sat":
+        if smt_check_sat() == "sat":
             if step == 0:
-                print("%s Temporal induction failed!" % smt.timestamp())
+                print_msg("Temporal induction failed!")
                 print_anyconsts(num_steps)
                 print_failed_asserts(num_steps)
                 write_trace(step, num_steps+1, '%')
@@ -1054,7 +1190,7 @@ if tempind:
                 write_trace(step, num_steps+1, "%d" % step)
 
         else:
-            print("%s Temporal induction successful." % smt.timestamp())
+            print_msg("Temporal induction successful.")
             retstatus = True
             break
 
@@ -1079,42 +1215,42 @@ elif covermode:
     assert step_size == 1
 
     while step < 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_h| s%d))" % (topmod, step))
-        smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
+        smt_state(step)
+        smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
+        smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
+        smt_assert_consequent(get_constr_expr(constr_assumes, step))
 
         if step == 0:
             if noinit:
-                smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
+                smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
             else:
-                smt.write("(assert (|%s_i| s0))" % (topmod))
-                smt.write("(assert (|%s_is| s0))" % (topmod))
+                smt_assert_antecedent("(|%s_i| s0)" % (topmod))
+                smt_assert_antecedent("(|%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))
+            smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
+            smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
 
         while "1" in cover_mask:
             print_msg("Checking cover reachability in step %d.." % (step))
-            smt.write("(push 1)")
-            smt.write("(assert (distinct (covers_%d s%d) #b%s))" % (coveridx, step, "0" * len(cover_desc)))
+            smt_push()
+            smt_assert_antecedent("(distinct (covers_%d s%d) #b%s)" % (coveridx, step, "0" * len(cover_desc)))
 
-            if smt.check_sat() == "unsat":
-                smt.write("(pop 1)")
+            if smt_check_sat() == "unsat":
+                smt_pop()
                 break
 
             if append_steps > 0:
                 for i in range(step+1, step+1+append_steps):
                     print_msg("Appending additional step %d." % i)
-                    smt.write("(declare-fun s%d () |%s_s|)" % (i, topmod))
-                    smt.write("(assert (not (|%s_is| s%d)))" % (topmod, i))
-                    smt.write("(assert (|%s_u| s%d))" % (topmod, i))
-                    smt.write("(assert (|%s_h| s%d))" % (topmod, i))
-                    smt.write("(assert (|%s_t| s%d s%d))" % (topmod, i-1, i))
-                    smt.write("(assert %s)" % get_constr_expr(constr_assumes, i))
+                    smt_state(i)
+                    smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
+                    smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
+                    smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
+                    smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
+                    smt_assert_consequent(get_constr_expr(constr_assumes, i))
                 print_msg("Re-solving with appended steps..")
-                assert smt.check_sat() == "sat"
+                assert smt_check_sat() == "sat"
 
             reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
             assert len(reached_covers) == len(cover_desc)
@@ -1141,7 +1277,7 @@ elif covermode:
                 break
 
             coveridx += 1
-            smt.write("(pop 1)")
+            smt_pop()
             smt.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx, topmod, len(cover_desc), coveridx-1, cover_mask))
 
         if found_failed_assert:
@@ -1162,27 +1298,27 @@ else:  # not tempind, covermode
     step = 0
     retstatus = True
     while step < 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_h| s%d))" % (topmod, step))
-        smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
+        smt_state(step)
+        smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
+        smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
+        smt_assert_consequent(get_constr_expr(constr_assumes, step))
 
         if step == 0:
             if noinit:
-                smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
+                smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
             else:
-                smt.write("(assert (|%s_i| s0))" % (topmod))
-                smt.write("(assert (|%s_is| s0))" % (topmod))
+                smt_assert_antecedent("(|%s_i| s0)" % (topmod))
+                smt_assert_antecedent("(|%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))
+            smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
+            smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
 
         if step < skip_steps:
             if assume_skipped is not None and step >= assume_skipped:
                 print_msg("Skipping step %d (and assuming pass).." % (step))
-                smt.write("(assert (|%s_a| s%d))" % (topmod, step))
-                smt.write("(assert %s)" % get_constr_expr(constr_asserts, step))
+                smt_assert_consequent("(|%s_a| s%d)" % (topmod, step))
+                smt_assert_consequent(get_constr_expr(constr_asserts, step))
             else:
                 print_msg("Skipping step %d.." % (step))
             step += 1
@@ -1191,12 +1327,12 @@ else:  # not tempind, covermode
         last_check_step = step
         for i in range(1, step_size):
             if step+i < num_steps:
-                smt.write("(declare-fun s%d () |%s_s|)" % (step+i, topmod))
-                smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step+i))
-                smt.write("(assert (|%s_u| s%d))" % (topmod, step+i))
-                smt.write("(assert (|%s_h| s%d))" % (topmod, step+i))
-                smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step+i-1, step+i))
-                smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i))
+                smt_state(step+i)
+                smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step+i))
+                smt_assert_consequent("(|%s_u| s%d)" % (topmod, step+i))
+                smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step+i))
+                smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step+i-1, step+i))
+                smt_assert_consequent(get_constr_expr(constr_assumes, step+i))
                 last_check_step = step+i
 
         if not gentrace:
@@ -1206,7 +1342,7 @@ else:  # not tempind, covermode
                 else:
                     print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
 
-                if smt.check_sat() == "unsat":
+                if smt_check_sat() == "unsat":
                     print("%s Warmup failed!" % smt.timestamp())
                     retstatus = False
                     break
@@ -1216,23 +1352,23 @@ else:  # not tempind, covermode
                     print_msg("Checking assertions in step %d.." % (step))
                 else:
                     print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step))
-                smt.write("(push 1)")
+                smt_push()
 
-                smt.write("(assert (not (and %s)))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
+                smt_assert_consequent("(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":
+                if smt_check_sat() == "sat":
                     print("%s BMC failed!" % smt.timestamp())
                     if append_steps > 0:
                         for i in range(last_check_step+1, last_check_step+1+append_steps):
                             print_msg("Appending additional step %d." % i)
-                            smt.write("(declare-fun s%d () |%s_s|)" % (i, topmod))
-                            smt.write("(assert (not (|%s_is| s%d)))" % (topmod, i))
-                            smt.write("(assert (|%s_u| s%d))" % (topmod, i))
-                            smt.write("(assert (|%s_h| s%d))" % (topmod, i))
-                            smt.write("(assert (|%s_t| s%d s%d))" % (topmod, i-1, i))
-                            smt.write("(assert %s)" % get_constr_expr(constr_assumes, i))
-                            assert smt.check_sat() == "sat"
+                            smt_state(i)
+                            smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
+                            smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
+                            smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
+                            smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
+                            smt_assert_consequent(get_constr_expr(constr_assumes, i))
+                            assert smt_check_sat() == "sat"
                     print_anyconsts(step)
                     for i in range(step, last_check_step+1):
                         print_failed_asserts(i)
@@ -1240,12 +1376,12 @@ else:  # not tempind, covermode
                     retstatus = False
                     break
 
-                smt.write("(pop 1)")
+                smt_pop()
 
             if (constr_final_start is not None) or (last_check_step+1 != num_steps):
                 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))
+                    smt_assert_consequent("(|%s_a| s%d)" % (topmod, i))
+                    smt_assert_consequent(get_constr_expr(constr_asserts, i))
 
             if constr_final_start is not None:
                 for i in range(step, last_check_step+1):
@@ -1253,12 +1389,12 @@ else:  # not tempind, covermode
                         continue
 
                     print_msg("Checking final constraints in step %d.." % (i))
-                    smt.write("(push 1)")
+                    smt_push()
 
-                    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))
+                    smt_assert_consequent(get_constr_expr(constr_assumes, i, final=True))
+                    smt_assert_consequent("(not %s)" % get_constr_expr(constr_asserts, i, final=True))
 
-                    if smt.check_sat() == "sat":
+                    if smt_check_sat() == "sat":
                         print("%s BMC failed!" % smt.timestamp())
                         print_anyconsts(i)
                         print_failed_asserts(i, final=True)
@@ -1266,17 +1402,17 @@ else:  # not tempind, covermode
                         retstatus = False
                         break
 
-                    smt.write("(pop 1)")
+                    smt_pop()
                 if not retstatus:
                     break
 
         else:  # gentrace
             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))
+                smt_assert_consequent("(|%s_a| s%d)" % (topmod, i))
+                smt_assert_consequent(get_constr_expr(constr_asserts, i))
 
             print_msg("Solving for step %d.." % (last_check_step))
-            if smt.check_sat() != "sat":
+            if smt_check_sat() != "sat":
                 print("%s No solution found!" % smt.timestamp())
                 retstatus = False
                 break
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 7af37bca2..4e5359795 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -59,6 +59,9 @@ class SmtModInfo:
         self.covers = dict()
         self.anyconsts = dict()
         self.anyseqs = dict()
+        self.allconsts = dict()
+        self.allseqs = dict()
+        self.asize = dict()
 
 
 class SmtIo:
@@ -69,6 +72,7 @@ class SmtIo:
         self.logic_uf = True
         self.logic_bv = True
         self.logic_dt = False
+        self.forall = False
         self.produce_models = True
         self.smt2cache = [list()]
         self.p = None
@@ -108,6 +112,9 @@ class SmtIo:
     def setup(self):
         assert not self.setup_done
 
+        if self.forall:
+            self.unroll = False
+
         if self.solver == "yices":
             self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
 
@@ -143,6 +150,7 @@ class SmtIo:
                 self.p_open()
 
         if self.unroll:
+            assert not self.forall
             self.logic_uf = False
             self.unroll_idcnt = 0
             self.unroll_buffer = ""
@@ -376,6 +384,11 @@ class SmtIo:
             if self.logic is None:
                 self.logic_dt = True
 
+        if fields[1] == "yosys-smt2-forall":
+            if self.logic is None:
+                self.logic_qf = False
+            self.forall = True
+
         if fields[1] == "yosys-smt2-module":
             self.curmod = fields[2]
             self.modinfo[self.curmod] = SmtModInfo()
@@ -419,10 +432,20 @@ class SmtIo:
             self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
 
         if fields[1] == "yosys-smt2-anyconst":
-            self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[3], None if len(fields) <= 4 else fields[4])
+            self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
+            self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
 
         if fields[1] == "yosys-smt2-anyseq":
-            self.modinfo[self.curmod].anyseqs[fields[2]] = (fields[3], None if len(fields) <= 4 else fields[4])
+            self.modinfo[self.curmod].anyseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
+            self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
+
+        if fields[1] == "yosys-smt2-allconst":
+            self.modinfo[self.curmod].allconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
+            self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
+
+        if fields[1] == "yosys-smt2-allseq":
+            self.modinfo[self.curmod].allseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
+            self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
 
     def hiernets(self, top, regs_only=False):
         def hiernets_worker(nets, mod, cursor):
@@ -439,7 +462,8 @@ class SmtIo:
     def hieranyconsts(self, top):
         def worker(results, mod, cursor):
             for name, value in sorted(self.modinfo[mod].anyconsts.items()):
-                results.append((cursor, name, value[0], value[1]))
+                width = self.modinfo[mod].asize[name]
+                results.append((cursor, name, value[0], value[1], width))
             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
                 worker(results, celltype, cursor + [cellname])
 
@@ -450,7 +474,32 @@ class SmtIo:
     def hieranyseqs(self, top):
         def worker(results, mod, cursor):
             for name, value in sorted(self.modinfo[mod].anyseqs.items()):
-                results.append((cursor, name, value[0], value[1]))
+                width = self.modinfo[mod].asize[name]
+                results.append((cursor, name, value[0], value[1], width))
+            for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
+                worker(results, celltype, cursor + [cellname])
+
+        results = list()
+        worker(results, top, [])
+        return results
+
+    def hierallconsts(self, top):
+        def worker(results, mod, cursor):
+            for name, value in sorted(self.modinfo[mod].allconsts.items()):
+                width = self.modinfo[mod].asize[name]
+                results.append((cursor, name, value[0], value[1], width))
+            for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
+                worker(results, celltype, cursor + [cellname])
+
+        results = list()
+        worker(results, top, [])
+        return results
+
+    def hierallseqs(self, top):
+        def worker(results, mod, cursor):
+            for name, value in sorted(self.modinfo[mod].allseqs.items()):
+                width = self.modinfo[mod].asize[name]
+                results.append((cursor, name, value[0], value[1], width))
             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
                 worker(results, celltype, cursor + [cellname])