New upstream version 0.7+20180830git0b7a184

4 files changed, 1818 insertions, 314 deletions

diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index eacda273..dce82f01 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -6,7 +6,7 @@ ifneq ($(CONFIG),emcc)
 TARGETS += yosys-smtbmc
 
 yosys-smtbmc: backends/smt2/smtbmc.py
-	$(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(__file__) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new
+	$(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new
 	$(Q) chmod +x $@.new
 	$(Q) mv $@.new $@
 
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index ddac6900..e2777ae0 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -32,14 +32,18 @@ struct Smt2Worker
 	CellTypes ct;
 	SigMap sigmap;
 	RTLIL::Module *module;
-	bool bvmode, memmode, wiresmode, verbose;
-	int idcounter;
+	bool bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode;
+	dict<IdString, int> &mod_stbv_width;
+	int idcounter = 0, statebv_width = 0;
 
-	std::vector<std::string> decls, trans, hier;
+	std::vector<std::string> decls, trans, hier, dtmembers;
 	std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
 	std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
 	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;
 	std::map<int, int> bvsizes;
@@ -63,17 +67,64 @@ struct Smt2Worker
 		return get_id(obj->name);
 	}
 
-	Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose) :
-			ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode),
-			wiresmode(wiresmode), verbose(verbose), idcounter(0)
+	void makebits(std::string name, int width = 0, std::string comment = std::string())
+	{
+		std::string decl_str;
+
+		if (statebv)
+		{
+			if (width == 0) {
+				decl_str = stringf("(define-fun |%s| ((state |%s_s|)) Bool (= ((_ extract %d %d) state) #b1))", name.c_str(), get_id(module), statebv_width, statebv_width);
+				statebv_width += 1;
+			} else {
+				decl_str = stringf("(define-fun |%s| ((state |%s_s|)) (_ BitVec %d) ((_ extract %d %d) state))", name.c_str(), get_id(module), width, statebv_width+width-1, statebv_width);
+				statebv_width += width;
+			}
+		}
+		else if (statedt)
+		{
+			if (width == 0) {
+				decl_str = stringf("  (|%s| Bool)", name.c_str());
+			} else {
+				decl_str = stringf("  (|%s| (_ BitVec %d))", name.c_str(), width);
+			}
+		}
+		else
+		{
+			if (width == 0) {
+				decl_str = stringf("(declare-fun |%s| (|%s_s|) Bool)", name.c_str(), get_id(module));
+			} else {
+				decl_str = stringf("(declare-fun |%s| (|%s_s|) (_ BitVec %d))", name.c_str(), get_id(module), width);
+			}
+		}
+
+		if (!comment.empty())
+			decl_str += " ; " + comment;
+
+		if (statedt)
+			dtmembers.push_back(decl_str + "\n");
+		else
+			decls.push_back(decl_str + "\n");
+	}
+
+	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), forallmode(forallmode), mod_stbv_width(mod_stbv_width)
 	{
-		decls.push_back(stringf("(declare-sort |%s_s| 0)\n", get_id(module)));
-		decls.push_back(stringf("(declare-fun |%s_is| (|%s_s|) Bool)\n", get_id(module), get_id(module)));
+		pool<SigBit> noclock;
+
+		makebits(stringf("%s_is", get_id(module)));
 
 		for (auto cell : module->cells())
-		for (auto &conn : cell->connections()) {
+		for (auto &conn : cell->connections())
+		{
+			if (GetSize(conn.second) == 0)
+				continue;
+
 			bool is_input = ct.cell_input(cell->type, conn.first);
 			bool is_output = ct.cell_output(cell->type, conn.first);
+
 			if (is_output && !is_input)
 				for (auto bit : sigmap(conn.second)) {
 					if (bit_driver.count(bit))
@@ -83,6 +134,66 @@ struct Smt2Worker
 			else if (is_output || !is_input)
 				log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n",
 						log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type));
+
+			if (cell->type.in("$mem") && conn.first.in("\\RD_CLK", "\\WR_CLK"))
+			{
+				SigSpec clk = sigmap(conn.second);
+				for (int i = 0; i < GetSize(clk); i++)
+				{
+					if (clk[i].wire == nullptr)
+						continue;
+
+					if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_ENABLE" : "\\WR_CLK_ENABLE")[i] != State::S1)
+						continue;
+
+					if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_POLARITY" : "\\WR_CLK_POLARITY")[i] == State::S1)
+						clock_posedge.insert(clk[i]);
+					else
+						clock_negedge.insert(clk[i]);
+				}
+			}
+			else
+			if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_") && conn.first.in("\\CLK", "\\C"))
+			{
+				bool posedge = (cell->type == "$_DFF_N_") || (cell->type == "$dff" && cell->getParam("\\CLK_POLARITY").as_bool());
+				for (auto bit : sigmap(conn.second)) {
+					if (posedge)
+						clock_posedge.insert(bit);
+					else
+						clock_negedge.insert(bit);
+				}
+			}
+			else
+			if (mod_clk_cache.count(cell->type) && mod_clk_cache.at(cell->type).count(conn.first))
+			{
+				for (auto bit : sigmap(conn.second)) {
+					if (mod_clk_cache.at(cell->type).at(conn.first).first)
+						clock_posedge.insert(bit);
+					if (mod_clk_cache.at(cell->type).at(conn.first).second)
+						clock_negedge.insert(bit);
+				}
+			}
+			else
+			{
+				for (auto bit : sigmap(conn.second))
+					noclock.insert(bit);
+			}
+		}
+
+		for (auto bit : noclock) {
+			clock_posedge.erase(bit);
+			clock_negedge.erase(bit);
+		}
+
+		for (auto wire : module->wires())
+		{
+			if (!wire->port_input || GetSize(wire) != 1)
+				continue;
+			SigBit bit = sigmap(wire);
+			if (clock_posedge.count(bit))
+				mod_clk_cache[module->name][wire->name].first = true;
+			if (clock_negedge.count(bit))
+				mod_clk_cache[module->name][wire->name].second = true;
 		}
 	}
 
@@ -162,8 +273,7 @@ struct Smt2Worker
 		if (fcache.count(bit) == 0) {
 			if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",
 					log_signal(bit));
-			decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
-					get_id(module), idcounter, get_id(module), log_signal(bit)));
+			makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(bit));
 			register_bool(bit, idcounter++);
 		}
 
@@ -237,8 +347,7 @@ struct Smt2Worker
 					log_signal(sig.extract(i, j)));
 			for (auto bit : sig.extract(i, j))
 				log_assert(bit_driver.count(bit) == 0);
-			decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
-					get_id(module), idcounter, get_id(module), j, log_signal(sig.extract(i, j))));
+			makebits(stringf("%s#%d", get_id(module), idcounter), j, log_signal(sig.extract(i, j)));
 			subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), idcounter, state_name));
 			register_bv(sig.extract(i, j), idcounter++);
 		}
@@ -288,7 +397,8 @@ struct Smt2Worker
 
 		if (type == 's' || type == 'd' || type == 'b') {
 			width = max(width, GetSize(cell->getPort("\\A")));
-			width = max(width, GetSize(cell->getPort("\\B")));
+			if (cell->hasPort("\\B"))
+				width = max(width, GetSize(cell->getPort("\\B")));
 		}
 
 		if (cell->hasPort("\\A")) {
@@ -382,8 +492,7 @@ struct Smt2Worker
 		if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
 		{
 			registers.insert(cell);
-			decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
-					get_id(module), idcounter, get_id(module), log_signal(cell->getPort("\\Q"))));
+			makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort("\\Q")));
 			register_bool(cell->getPort("\\Q"), idcounter++);
 			recursive_cells.erase(cell);
 			return;
@@ -397,6 +506,8 @@ struct Smt2Worker
 		if (cell->type == "$_NOR_") return export_gate(cell, "(not (or A B))");
 		if (cell->type == "$_XOR_") return export_gate(cell, "(xor A B)");
 		if (cell->type == "$_XNOR_") return export_gate(cell, "(not (xor A B))");
+		if (cell->type == "$_ANDNOT_") return export_gate(cell, "(and A (not B))");
+		if (cell->type == "$_ORNOT_") return export_gate(cell, "(or A (not B))");
 		if (cell->type == "$_MUX_") return export_gate(cell, "(ite S B A)");
 		if (cell->type == "$_AOI3_") return export_gate(cell, "(not (or (and A B) C))");
 		if (cell->type == "$_OAI3_") return export_gate(cell, "(not (and (or A B) C))");
@@ -410,20 +521,22 @@ struct Smt2Worker
 			if (cell->type.in("$ff", "$dff"))
 			{
 				registers.insert(cell);
-				decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
-						get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))));
+				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q")));
 				register_bv(cell->getPort("\\Q"), idcounter++);
 				recursive_cells.erase(cell);
 				return;
 			}
 
-			if (cell->type.in("$anyconst", "$anyseq"))
+			if (cell->type.in("$anyconst", "$anyseq", "$allconst", "$allseq"))
 			{
 				registers.insert(cell);
-				decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
-						cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
-				decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
-						get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y"))));
+				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 %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;
@@ -467,6 +580,13 @@ struct Smt2Worker
 			if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
 			if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
 
+			if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool") &&
+					2*GetSize(cell->getPort("\\A").chunks()) < GetSize(cell->getPort("\\A"))) {
+				bool is_and = cell->type == "$reduce_and";
+				string bits(GetSize(cell->getPort("\\A")), is_and ? '1' : '0');
+				return export_bvop(cell, stringf("(%s A #b%s)", is_and ? "=" : "distinct", bits.c_str()), 'b');
+			}
+
 			if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
 			if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
 			if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
@@ -513,30 +633,97 @@ struct Smt2Worker
 			int abits = cell->getParam("\\ABITS").as_int();
 			int width = cell->getParam("\\WIDTH").as_int();
 			int rd_ports = cell->getParam("\\RD_PORTS").as_int();
+			int wr_ports = cell->getParam("\\WR_PORTS").as_int();
 
-			decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
-					get_id(module), arrayid, get_id(module), abits, width, get_id(cell)));
+			bool async_read = false;
+			if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
+				if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_zero())
+					log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
+				async_read = true;
+			}
 
-			decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d\n", get_id(cell), abits, width, rd_ports));
-			decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n",
-					get_id(module), get_id(cell), get_id(module), abits, width, get_id(module), arrayid));
+			decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(cell), abits, width, rd_ports, wr_ports, async_read ? "async" : "sync"));
 
-			for (int i = 0; i < rd_ports; i++)
+			string memstate;
+			if (async_read) {
+				memstate = stringf("%s#%d#final", get_id(module), arrayid);
+			} else {
+				memstate = stringf("%s#%d#0", get_id(module), arrayid);
+			}
+
+			if (statebv)
 			{
-				SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
-				SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
-				std::string addr = get_bv(addr_sig);
+				int mem_size = cell->getParam("\\SIZE").as_int();
+				int mem_offset = cell->getParam("\\OFFSET").as_int();
+
+				makebits(memstate, width*mem_size, get_id(cell));
+				decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n",
+						get_id(module), get_id(cell), get_id(module), width*mem_size, memstate.c_str()));
+
+				for (int i = 0; i < rd_ports; i++)
+				{
+					SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
+					SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
+					std::string addr = get_bv(addr_sig);
+
+					if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
+						log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
+								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
+
+					decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+							get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
 
-				if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
-					log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
-							"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
+					std::string read_expr = "#b";
+					for (int k = 0; k < width; k++)
+						read_expr += "0";
 
-				decls.push_back(stringf("(define-fun |%s_m:%d %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
-						get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+					for (int k = 0; k < mem_size; k++)
+						read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s| state))\n  %s)",
+								get_id(module), i, get_id(cell), Const(k+mem_offset, abits).as_string().c_str(),
+								width*(k+1)-1, width*k, memstate.c_str(), read_expr.c_str());
 
-				decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s#%d#0| state) %s)) ; %s\n",
-						get_id(module), idcounter, get_id(module), width, get_id(module), arrayid, addr.c_str(), log_signal(data_sig)));
-				register_bv(data_sig, idcounter++);
+					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n  %s) ; %s\n",
+							get_id(module), idcounter, get_id(module), width, read_expr.c_str(), log_signal(data_sig)));
+
+					decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
+							get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));
+
+					register_bv(data_sig, idcounter++);
+				}
+			}
+			else
+			{
+				if (statedt)
+					dtmembers.push_back(stringf("  (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+							memstate.c_str(), abits, width, get_id(cell)));
+				else
+					decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+							memstate.c_str(), get_id(module), abits, width, get_id(cell)));
+
+				decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s| state))\n",
+						get_id(module), get_id(cell), get_id(module), abits, width, memstate.c_str()));
+
+				for (int i = 0; i < rd_ports; i++)
+				{
+					SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
+					SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
+					std::string addr = get_bv(addr_sig);
+
+					if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
+						log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
+								"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
+
+					decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+							get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+
+					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s| state) (|%s_m:R%dA %s| state))) ; %s\n",
+							get_id(module), idcounter, get_id(module), width, memstate.c_str(), get_id(module), i, get_id(cell), log_signal(data_sig)));
+
+					decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
+							get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));
+
+					register_bv(data_sig, idcounter++);
+				}
 			}
 
 			registers.insert(cell);
@@ -553,32 +740,38 @@ struct Smt2Worker
 
 			for (auto &conn : cell->connections())
 			{
+				if (GetSize(conn.second) == 0)
+					continue;
+
 				Wire *w = m->wire(conn.first);
 				SigSpec sig = sigmap(conn.second);
 
 				if (w->port_output && !w->port_input) {
 					if (GetSize(w) > 1) {
 						if (bvmode) {
-							decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
-									get_id(module), idcounter, get_id(module), GetSize(w), log_signal(sig)));
+							makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(w), log_signal(sig));
 							register_bv(sig, idcounter++);
 						} else {
 							for (int i = 0; i < GetSize(w); i++) {
-								decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
-										get_id(module), idcounter, get_id(module), log_signal(sig[i])));
+								makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig[i]));
 								register_bool(sig[i], idcounter++);
 							}
 						}
 					} else {
-						decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
-								get_id(module), idcounter, get_id(module), log_signal(sig)));
+						makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig));
 						register_bool(sig, idcounter++);
 					}
 				}
 			}
 
-			decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n",
-					get_id(module), get_id(cell->name), get_id(module), get_id(cell->type)));
+			if (statebv)
+				makebits(stringf("%s_h %s", get_id(module), get_id(cell->name)), mod_stbv_width.at(cell->type));
+			else if (statedt)
+				dtmembers.push_back(stringf("  (|%s_h %s| |%s_s|)\n",
+						get_id(module), get_id(cell->name), get_id(cell->type)));
+			else
+				decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n",
+						get_id(module), get_id(cell->name), get_id(module), get_id(cell->type)));
 
 			hiercells.insert(cell);
 			hiercells_queue.insert(cell);
@@ -617,17 +810,30 @@ struct Smt2Worker
 					decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
 				if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\'))
 					decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
+				if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
+					decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
+							clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
 				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)));
+						}
 				}
 			}
 		}
@@ -639,31 +845,104 @@ struct Smt2Worker
 			if (wire->attributes.count("\\init")) {
 				RTLIL::SigSpec sig = sigmap(wire);
 				Const val = wire->attributes.at("\\init");
-				val.bits.resize(GetSize(sig));
+				val.bits.resize(GetSize(sig), State::Sx);
 				if (bvmode && GetSize(sig) > 1) {
-					init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire)));
+					Const mask(State::S1, GetSize(sig));
+					bool use_mask = false;
+					for (int i = 0; i < GetSize(sig); i++)
+						if (val[i] != State::S0 && val[i] != State::S1) {
+							val[i] = State::S0;
+							mask[i] = State::S0;
+							use_mask = true;
+						}
+					if (use_mask)
+						init_list.push_back(stringf("(= (bvand %s #b%s) #b%s) ; %s", get_bv(sig).c_str(), mask.as_string().c_str(), val.as_string().c_str(), get_id(wire)));
+					else
+						init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire)));
 				} else {
 					for (int i = 0; i < GetSize(sig); i++)
-						init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val.bits[i] == State::S1 ? "true" : "false", get_id(wire)));
+						if (val[i] == State::S0 || val[i] == State::S1)
+							init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val[i] == State::S1 ? "true" : "false", get_id(wire)));
 				}
 			}
 
 		if (verbose) log("=> export logic driving asserts\n");
 
-		vector<string> assert_list, assume_list;
+		int assert_id = 0, assume_id = 0, cover_id = 0;
+		vector<string> assert_list, assume_list, cover_list;
+
 		for (auto cell : module->cells())
-			if (cell->type.in("$assert", "$assume")) {
+		{
+			if (cell->type.in("$assert", "$assume", "$cover"))
+			{
+				int &id = cell->type == "$assert" ? assert_id :
+						cell->type == "$assume" ? assume_id :
+						cell->type == "$cover" ? cover_id : *(int*)nullptr;
+
+				char postfix = cell->type == "$assert" ? 'a' :
+						cell->type == "$assume" ? 'u' :
+						cell->type == "$cover" ? 'c' : 0;
+
 				string name_a = get_bool(cell->getPort("\\A"));
 				string name_en = get_bool(cell->getPort("\\EN"));
-				decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
+				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
 						cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
-				decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
-						get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
-				if (cell->type == "$assert")
-					assert_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
+
+				if (cell->type == "$cover")
+					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
+							get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
 				else
-					assume_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
+					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
+							get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
+
+				if (cell->type == "$assert")
+					assert_list.push_back(stringf("(|%s_a %d| state)", get_id(module), id));
+				else if (cell->type == "$assume")
+					assume_list.push_back(stringf("(|%s_u %d| state)", get_id(module), id));
+
+				id++;
 			}
+		}
+
+		if (verbose) log("=> export logic driving hierarchical cells\n");
+
+		for (auto cell : module->cells())
+			if (module->design->module(cell->type) != nullptr)
+				export_cell(cell);
+
+		while (!hiercells_queue.empty())
+		{
+			std::set<RTLIL::Cell*> queue;
+			queue.swap(hiercells_queue);
+
+			for (auto cell : queue)
+			{
+				string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
+				Module *m = module->design->module(cell->type);
+				log_assert(m != nullptr);
+
+				hier.push_back(stringf("  (= (|%s_is| state) (|%s_is| %s))\n",
+						get_id(module), get_id(cell->type), cell_state.c_str()));
+
+				for (auto &conn : cell->connections())
+				{
+					if (GetSize(conn.second) == 0)
+						continue;
+
+					Wire *w = m->wire(conn.first);
+					SigSpec sig = sigmap(conn.second);
+
+					if (bvmode || GetSize(w) == 1) {
+						hier.push_back(stringf("  (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)).c_str(),
+								get_id(cell->type), get_id(w), cell_state.c_str(), get_id(cell->type), get_id(w)));
+					} else {
+						for (int i = 0; i < GetSize(w); i++)
+							hier.push_back(stringf("  (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]).c_str(),
+									get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i));
+					}
+				}
+			}
+		}
 
 		for (int iter = 1; !registers.empty(); iter++)
 		{
@@ -679,6 +958,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"))
@@ -686,13 +966,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")
@@ -703,24 +986,111 @@ struct Smt2Worker
 					int width = cell->getParam("\\WIDTH").as_int();
 					int wr_ports = cell->getParam("\\WR_PORTS").as_int();
 
-					for (int i = 0; i < wr_ports; i++)
+					bool async_read = false;
+					string initial_memstate, final_memstate;
+
+					if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
+						log_assert(cell->getParam("\\WR_CLK_ENABLE").is_fully_zero());
+						async_read = true;
+						initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
+						final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
+					}
+
+					if (statebv)
+					{
+						int mem_size = cell->getParam("\\SIZE").as_int();
+						int mem_offset = cell->getParam("\\OFFSET").as_int();
+
+						if (async_read) {
+							makebits(final_memstate, width*mem_size, get_id(cell));
+						}
+
+						for (int i = 0; i < wr_ports; i++)
+						{
+							SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
+							SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width);
+							SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width);
+
+							std::string addr = get_bv(addr_sig);
+							std::string data = get_bv(data_sig);
+							std::string mask = get_bv(mask_sig);
+
+							decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+									get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+							addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));
+
+							decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+									get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
+							data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));
+
+							decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+									get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
+							mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));
+
+							std::string data_expr;
+
+							for (int k = mem_size-1; k >= 0; k--) {
+								std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))",
+										data.c_str(), mask.c_str(), width*(k+1)-1, width*k, get_id(module), arrayid, i, mask.c_str());
+								data_expr += stringf("\n  (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))",
+										addr.c_str(), Const(k+mem_offset, abits).as_string().c_str(), new_data.c_str(),
+										width*(k+1)-1, width*k, get_id(module), arrayid, i);
+							}
+
+							decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n",
+									get_id(module), arrayid, i+1, get_id(module), width*mem_size, data_expr.c_str(), get_id(cell)));
+						}
+					}
+					else
 					{
-						std::string addr = get_bv(cell->getPort("\\WR_ADDR").extract(abits*i, abits));
-						std::string data = get_bv(cell->getPort("\\WR_DATA").extract(width*i, width));
-						std::string mask = get_bv(cell->getPort("\\WR_EN").extract(width*i, width));
+						if (async_read) {
+							if (statedt)
+								dtmembers.push_back(stringf("  (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+										initial_memstate.c_str(), abits, width, get_id(cell)));
+							else
+								decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+										initial_memstate.c_str(), get_id(module), abits, width, get_id(cell)));
+						}
+
+						for (int i = 0; i < wr_ports; i++)
+						{
+							SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
+							SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width);
+							SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width);
+
+							std::string addr = get_bv(addr_sig);
+							std::string data = get_bv(data_sig);
+							std::string mask = get_bv(mask_sig);
+
+							decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+									get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+							addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));
+
+							decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+									get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
+							data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));
+
+							decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+									get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
+							mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));
 
-						data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
-								data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
+							data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
+									data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
 
-						decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
-								"(store (|%s#%d#%d| state) %s %s)) ; %s\n",
-								get_id(module), arrayid, i+1, get_id(module), abits, width,
-								get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(cell)));
+							decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
+									"(store (|%s#%d#%d| state) %s %s)) ; %s\n",
+									get_id(module), arrayid, i+1, get_id(module), abits, width,
+									get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(cell)));
+						}
 					}
 
 					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)));
 
 					Const init_data = cell->getParam("\\INIT");
 					int memsize = cell->getParam("\\SIZE").as_int();
@@ -737,46 +1107,20 @@ struct Smt2Worker
 							if (bit == State::S0 || bit == State::S1)
 								gen_init_constr = true;
 
-						if (gen_init_constr) {
-							init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
-									get_id(module), arrayid, Const(i, abits).as_string().c_str(),
-									initword.as_string().c_str(), get_id(cell), i));
+						if (gen_init_constr)
+						{
+							if (statebv)
+								/* FIXME */;
+							else
+								init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+										get_id(module), arrayid, Const(i, abits).as_string().c_str(),
+										initword.as_string().c_str(), get_id(cell), i));
 						}
 					}
 				}
 			}
 		}
 
-		if (verbose) log("=> export logic driving hierarchical cells\n");
-
-		while (!hiercells_queue.empty())
-		{
-			std::set<RTLIL::Cell*> queue;
-			queue.swap(hiercells_queue);
-
-			for (auto cell : queue)
-			{
-				string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
-				Module *m = module->design->module(cell->type);
-				log_assert(m != nullptr);
-
-				for (auto &conn : cell->connections())
-				{
-					Wire *w = m->wire(conn.first);
-					SigSpec sig = sigmap(conn.second);
-
-					if (bvmode || GetSize(w) == 1) {
-						hier.push_back(stringf("  (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)).c_str(),
-								get_id(cell->type), get_id(w), cell_state.c_str(), get_id(cell->type), get_id(w)));
-					} else {
-						for (int i = 0; i < GetSize(w); i++)
-							hier.push_back(stringf("  (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]).c_str(),
-									get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i));
-					}
-				}
-			}
-		}
-
 		if (verbose) log("=> finalizing SMT2 representation of %s.\n", log_id(module));
 
 		for (auto c : hiercells) {
@@ -786,6 +1130,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";
@@ -832,6 +1207,18 @@ struct Smt2Worker
 	{
 		f << stringf("; yosys-smt2-module %s\n", get_id(module));
 
+		if (statebv) {
+			f << stringf("(define-sort |%s_s| () (_ BitVec %d))\n", get_id(module), statebv_width);
+			mod_stbv_width[module->name] = statebv_width;
+		} else
+		if (statedt) {
+			f << stringf("(declare-datatype |%s_s| ((|%s_mk|\n", get_id(module), get_id(module));
+			for (auto it : dtmembers)
+				f << it;
+			f << stringf(")))\n");
+		} else
+			f << stringf("(declare-sort |%s_s| 0)\n", get_id(module));
+
 		for (auto it : decls)
 			f << it;
 
@@ -864,44 +1251,92 @@ struct Smt2Worker
 
 struct Smt2Backend : public Backend {
 	Smt2Backend() : Backend("smt2", "write design to SMT-LIBv2 file") { }
-	virtual void help()
+	void help() YS_OVERRIDE
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
 		log("    write_smt2 [options] [filename]\n");
 		log("\n");
 		log("Write a SMT-LIBv2 [1] description of the current design. For a module with name\n");
-		log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and the\n");
-		log("functions operating on that state.\n");
+		log("'<mod>' this will declare the sort '<mod>_s' (state of the module) and will\n");
+		log("define and declare functions operating on that state.\n");
+		log("\n");
+		log("The following SMT2 functions are generated for a module with name '<mod>'.\n");
+		log("Some declarations/definitions are printed with a special comment. A prover\n");
+		log("using the SMT2 files can use those comments to collect all relevant metadata\n");
+		log("about the design.\n");
+		log("\n");
+		log("    ; yosys-smt2-module <mod>\n");
+		log("    (declare-sort |<mod>_s| 0)\n");
+		log("        The sort representing a state of module <mod>.\n");
+		log("\n");
+		log("    (define-fun |<mod>_h| ((state |<mod>_s|)) Bool (...))\n");
+		log("        This function must be asserted for each state to establish the\n");
+		log("        design hierarchy.\n");
+		log("\n");
+		log("    ; yosys-smt2-input <wirename> <width>\n");
+		log("    ; yosys-smt2-output <wirename> <width>\n");
+		log("    ; yosys-smt2-register <wirename> <width>\n");
+		log("    ; yosys-smt2-wire <wirename> <width>\n");
+		log("    (define-fun |<mod>_n <wirename>| (|<mod>_s|) (_ BitVec <width>))\n");
+		log("    (define-fun |<mod>_n <wirename>| (|<mod>_s|) Bool)\n");
+		log("        For each port, register, and wire with the 'keep' attribute set an\n");
+		log("        accessor function is generated. Single-bit wires are returned as Bool,\n");
+		log("        multi-bit wires as BitVec.\n");
+		log("\n");
+		log("    ; yosys-smt2-cell <submod> <instancename>\n");
+		log("    (declare-fun |<mod>_h <instancename>| (|<mod>_s|) |<submod>_s|)\n");
+		log("        There is a function like that for each hierarchical instance. It\n");
+		log("        returns the sort that represents the state of the sub-module that\n");
+		log("        implements the instance.\n");
+		log("\n");
+		log("    (declare-fun |<mod>_is| (|<mod>_s|) Bool)\n");
+		log("        This function must be asserted 'true' for initial states, and 'false'\n");
+		log("        otherwise.\n");
+		log("\n");
+		log("    (define-fun |<mod>_i| ((state |<mod>_s|)) Bool (...))\n");
+		log("        This function must be asserted 'true' for initial states. For\n");
+		log("        non-initial states it must be left unconstrained.\n");
 		log("\n");
-		log("The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions\n");
-		log("are provided that can be used to access the values of the signals in the module.\n");
-		log("By default only ports, registers, and wires with the 'keep' attribute set are\n");
-		log("made available via such functions. With the -nobv option, multi-bit wires are\n");
-		log("exported as separate functions of type Bool for the individual bits. Without\n");
-		log("-nobv multi-bit wires are exported as single functions of type BitVec.\n");
+		log("    (define-fun |<mod>_t| ((state |<mod>_s|) (next_state |<mod>_s|)) Bool (...))\n");
+		log("        This function evaluates to 'true' if the states 'state' and\n");
+		log("        'next_state' form a valid state transition.\n");
 		log("\n");
-		log("The '<mod>_t' function evaluates to 'true' when the given pair of states\n");
-		log("describes a valid state transition.\n");
+		log("    (define-fun |<mod>_a| ((state |<mod>_s|)) Bool (...))\n");
+		log("        This function evaluates to 'true' if all assertions hold in the state.\n");
 		log("\n");
-		log("The '<mod>_a' function evaluates to 'true' when the given state satisfies\n");
-		log("the asserts in the module.\n");
+		log("    (define-fun |<mod>_u| ((state |<mod>_s|)) Bool (...))\n");
+		log("        This function evaluates to 'true' if all assumptions hold in the state.\n");
 		log("\n");
-		log("The '<mod>_u' function evaluates to 'true' when the given state satisfies\n");
-		log("the assumptions in the module.\n");
+		log("    ; yosys-smt2-assert <id> <filename:linenum>\n");
+		log("    (define-fun |<mod>_a <id>| ((state |<mod>_s|)) Bool (...))\n");
+		log("        Each $assert cell is converted into one of this functions. The function\n");
+		log("        evaluates to 'true' if the assert statement holds in the state.\n");
 		log("\n");
-		log("The '<mod>_i' function evaluates to 'true' when the given state conforms\n");
-		log("to the initial state. Furthermore the '<mod>_is' function should be asserted\n");
-		log("to be true for initial states in addition to '<mod>_i', and should be\n");
-		log("asserted to be false for non-initial states.\n");
+		log("    ; yosys-smt2-assume <id> <filename:linenum>\n");
+		log("    (define-fun |<mod>_u <id>| ((state |<mod>_s|)) Bool (...))\n");
+		log("        Each $assume cell is converted into one of this functions. The function\n");
+		log("        evaluates to 'true' if the assume statement holds in the state.\n");
 		log("\n");
-		log("For hierarchical designs, the '<mod>_h' function must be asserted for each\n");
-		log("state to establish the design hierarchy. The '<mod>_h <cellname>' function\n");
-		log("evaluates to the state corresponding to the given cell within <mod>.\n");
+		log("    ; yosys-smt2-cover <id> <filename:linenum>\n");
+		log("    (define-fun |<mod>_c <id>| ((state |<mod>_s|)) Bool (...))\n");
+		log("        Each $cover cell is converted into one of this functions. The function\n");
+		log("        evaluates to 'true' if the cover statement is activated in the state.\n");
+		log("\n");
+		log("Options:\n");
 		log("\n");
 		log("    -verbose\n");
 		log("        this will print the recursive walk used to export the modules.\n");
 		log("\n");
+		log("    -stbv\n");
+		log("        Use a BitVec sort to represent a state instead of an uninterpreted\n");
+		log("        sort. As a side-effect this will prevent use of arrays to model\n");
+		log("        memories.\n");
+		log("\n");
+		log("    -stdt\n");
+		log("        Use SMT-LIB 2.6 style datatypes to represent a state instead of an\n");
+		log("        uninterpreted sort.\n");
+		log("\n");
 		log("    -nobv\n");
 		log("        disable support for BitVec (FixedSizeBitVectors theory). without this\n");
 		log("        option multi-bit wires are represented using the BitVec sort and\n");
@@ -972,10 +1407,11 @@ struct Smt2Backend : public Backend {
 		log("from non-zero to zero in the test design.\n");
 		log("\n");
 	}
-	virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
 		std::ifstream template_f;
-		bool bvmode = true, memmode = true, wiresmode = false, verbose = false;
+		bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;
+		bool forallmode = false;
 
 		log_header(design, "Executing SMT2 backend.\n");
 
@@ -992,6 +1428,16 @@ struct Smt2Backend : public Backend {
 				log_warning("Options -bv and -mem are now the default. Support for -bv and -mem will be removed in the future.\n");
 				continue;
 			}
+			if (args[argidx] == "-stbv") {
+				statebv = true;
+				statedt = false;
+				continue;
+			}
+			if (args[argidx] == "-stdt") {
+				statebv = false;
+				statedt = true;
+				continue;
+			}
 			if (args[argidx] == "-nobv") {
 				bvmode = false;
 				memmode = false;
@@ -1033,6 +1479,12 @@ struct Smt2Backend : public Backend {
 		if (!memmode)
 			*f << stringf("; yosys-smt2-nomem\n");
 
+		if (statebv)
+			*f << stringf("; yosys-smt2-stbv\n");
+
+		if (statedt)
+			*f << stringf("; yosys-smt2-stdt\n");
+
 		std::vector<RTLIL::Module*> sorted_modules;
 
 		// extract module dependencies
@@ -1062,17 +1514,31 @@ struct Smt2Backend : public Backend {
 				module_deps.erase(sorted_modules.at(sorted_modules_idx++));
 		}
 
+		dict<IdString, int> mod_stbv_width;
+		dict<IdString, dict<IdString, pair<bool, bool>>> mod_clk_cache;
 		Module *topmod = design->top_module();
 		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);
+			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 04c25f91..6af2a5ac 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -22,21 +22,32 @@ import os, sys, getopt, re
 from smtio import SmtIo, SmtOpts, MkVcd
 from collections import defaultdict
 
+got_topt = False
 skip_steps = 0
 step_size = 1
 num_steps = 20
+append_steps = 0
 vcdfile = None
 cexfile = None
+aimfile = None
+aiwfile = None
+aigheader = True
 vlogtbfile = None
+vlogtbtop = None
 inconstr = list()
 outconstr = None
 gentrace = False
+covermode = False
 tempind = False
 dumpall = False
 assume_skipped = None
 final_only = False
 topmod = None
 noinfo = False
+presat = False
+smtcinit = False
+smtctop = None
+noinit = False
 so = SmtOpts()
 
 
@@ -56,6 +67,9 @@ yosys-smtbmc [options] <yosys_smt2_output>
     -i
         instead of BMC run temporal induction
 
+    -c
+        instead of regular BMC run cover analysis
+
     -m <module_name>
         name of the top module
 
@@ -65,10 +79,30 @@ yosys-smtbmc [options] <yosys_smt2_output>
     --cex <cex_filename>
         read cex file as written by ABC's "write_cex -n"
 
+    --aig <prefix>
+        read AIGER map file (as written by Yosys' "write_aiger -map")
+        and AIGER witness file. The file names are <prefix>.aim for
+        the map file and <prefix>.aiw for the witness file.
+
+    --aig <aim_filename>:<aiw_filename>
+        like above, but for map files and witness files that do not
+        share a filename prefix (or use differen file extensions).
+
+    --aig-noheader
+        the AIGER witness file does not include the status and
+        properties lines.
+
     --noinfo
         only run the core proof, do not collect and print any
         additional information (e.g. which assert failed)
 
+    --presat
+        check if the design with assumptions but without assertions
+        is SAT before checking if assertions are UNSAT. This will
+        detect if there are contradicting assumtions. In some cases
+        this will also help to "warmup" the solver, potentially
+        yielding a speedup.
+
     --final-only
         only check final constraints, assume base case
 
@@ -85,25 +119,48 @@ yosys-smtbmc [options] <yosys_smt2_output>
     --dump-vlogtb <verilog_filename>
         write trace as Verilog test bench
 
+    --vlogtb-top <hierarchical_name>
+        use the given entity as top module for the generated
+        Verilog test bench. The <hierarchical_name> is relative
+        to the design top module without the top module name.
+
     --dump-smtc <constr_filename>
         write trace as constraints file
 
+    --smtc-init
+        write just the last state as initial constraint to smtc file
+
+    --smtc-top <old>[:<new>]
+        replace <old> with <new> in constraints dumped to smtc
+        file and only dump object below <old> in design hierarchy.
+
+    --noinit
+        do not assume initial conditions in state 0
+
     --dump-all
         when using -g or -i, create a dump file for each
         step. The character '%' is replaces in all dump
         filenames with the step number.
+
+    --append <num_steps>
+        add <num_steps> time steps at the end of the trace
+        when creating a counter example (this additional time
+        steps will still be constrained by assumtions)
 """ + so.helpmsg())
     sys.exit(1)
 
 
 try:
-    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts +
-            ["final-only", "assume-skipped=", "smtc=", "cex=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"])
+    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
+            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat",
+             "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
+             "smtc-init", "smtc-top=", "noinit"])
 except:
     usage()
 
 for o, a in opts:
     if o == "-t":
+        got_topt = True
         a = a.split(":")
         if len(a) == 1:
             num_steps = int(a[0])
@@ -115,7 +172,7 @@ for o, a in opts:
             step_size = int(a[1])
             num_steps = int(a[2])
         else:
-            assert 0
+            assert False
     elif o == "--assume-skipped":
         assume_skipped = int(a)
     elif o == "--final-only":
@@ -124,20 +181,46 @@ for o, a in opts:
         inconstr.append(a)
     elif o == "--cex":
         cexfile = a
+    elif o == "--aig":
+        if ":" in a:
+            aimfile, aiwfile = a.split(":")
+        else:
+            aimfile = a + ".aim"
+            aiwfile = a + ".aiw"
+    elif o == "--aig-noheader":
+        aigheader = False
     elif o == "--dump-vcd":
         vcdfile = a
     elif o == "--dump-vlogtb":
         vlogtbfile = a
+    elif o == "--vlogtb-top":
+        vlogtbtop = a
     elif o == "--dump-smtc":
         outconstr = a
+    elif o == "--smtc-init":
+        smtcinit = True
+    elif o == "--smtc-top":
+        smtctop = a.split(":")
+        if len(smtctop) == 1:
+            smtctop.append("")
+        assert len(smtctop) == 2
+        smtctop = tuple(smtctop)
     elif o == "--dump-all":
         dumpall = True
+    elif o == "--presat":
+        presat = True
     elif o == "--noinfo":
         noinfo = True
+    elif o == "--noinit":
+        noinit = True
+    elif o == "--append":
+        append_steps = int(a)
     elif o == "-i":
         tempind = True
     elif o == "-g":
         gentrace = True
+    elif o == "-c":
+        covermode = True
     elif o == "-m":
         topmod = a
     elif so.handle(o, a):
@@ -148,6 +231,8 @@ for o, a in opts:
 if len(args) != 1:
     usage()
 
+if sum([tempind, gentrace, covermode]) > 1:
+    usage()
 
 constr_final_start = None
 constr_asserts = defaultdict(list)
@@ -182,12 +267,11 @@ for fn in inconstr:
                     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)
+                    arg = abs(int(tokens[1]))
+                    current_states = set(["final-%d" % i for i in range(arg, num_steps+1)])
+                    constr_final_start = arg if constr_final_start is None else min(constr_final_start, arg)
                 else:
-                    assert 0
+                    assert False
                 continue
 
             if tokens[0] == "state":
@@ -206,18 +290,17 @@ for fn in inconstr:
                             for i in range(lower, upper+1):
                                 current_states.add(i)
                         else:
-                            assert 0
+                            assert False
                 continue
 
             if tokens[0] == "always":
                 if len(tokens) == 1:
                     current_states = set(range(0, num_steps+1))
                 elif len(tokens) == 2:
-                    i = int(tokens[1])
-                    assert i < 0
-                    current_states = set(range(-i, num_steps+1))
+                    arg = abs(int(tokens[1]))
+                    current_states = set(range(arg, num_steps+1))
                 else:
-                    assert 0
+                    assert False
                 continue
 
             if tokens[0] == "assert":
@@ -244,7 +327,7 @@ for fn in inconstr:
                 so.logic = " ".join(tokens[1:])
                 continue
 
-            assert 0
+            assert False
 
 
 def get_constr_expr(db, state, final=False, getvalues=False):
@@ -255,7 +338,7 @@ def get_constr_expr(db, state, final=False, getvalues=False):
         if state not in db:
             return ([], [], []) if getvalues else "true"
 
-    netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]*)\](?=[ )]|$)')
+    netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]*|\S*)\](?=[ )]|$)')
 
     def replace_netref(match):
         state_sel = match.group(2)
@@ -318,6 +401,11 @@ assert topmod is not None
 assert topmod in smt.modinfo
 
 if cexfile is not None:
+    if not got_topt:
+        assume_skipped = 0
+        skip_steps = 0
+        num_steps = 0
+
     with open(cexfile, "r") as f:
         cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
         for entry in f.read().split():
@@ -349,6 +437,144 @@ if cexfile is not None:
             # print("cex@%d: %s" % (step, smtexpr))
             constr_assumes[step].append((cexfile, smtexpr))
 
+            if not got_topt:
+                skip_steps = max(skip_steps, step)
+                num_steps = max(num_steps, step+1)
+
+if aimfile is not None:
+    input_map = dict()
+    init_map = dict()
+    latch_map = dict()
+
+    if not got_topt:
+        assume_skipped = 0
+        skip_steps = 0
+        num_steps = 0
+
+    with open(aimfile, "r") as f:
+        for entry in f.read().splitlines():
+            entry = entry.split()
+
+            if entry[0] == "input":
+                input_map[int(entry[1])] = (entry[3], int(entry[2]))
+                continue
+
+            if entry[0] == "init":
+                init_map[int(entry[1])] = (entry[3], int(entry[2]))
+                continue
+
+            if entry[0] in ["latch", "invlatch"]:
+                latch_map[int(entry[1])] = (entry[3], int(entry[2]), entry[0] == "invlatch")
+                continue
+
+            if entry[0] in ["output", "wire"]:
+                continue
+
+            assert False
+
+    with open(aiwfile, "r") as f:
+        got_state = False
+        got_ffinit = False
+        step = 0
+
+        if not aigheader:
+            got_state = True
+
+        for entry in f.read().splitlines():
+            if len(entry) == 0 or entry[0] in "bcjfu.":
+                continue
+
+            if not got_state:
+                got_state = True
+                assert entry == "1"
+                continue
+
+            if not got_ffinit:
+                got_ffinit = True
+                if len(init_map) == 0:
+                    for i in range(len(entry)):
+                        if entry[i] == "x":
+                            continue
+
+                        if i in latch_map:
+                            value = int(entry[i])
+                            name = latch_map[i][0]
+                            bitidx = latch_map[i][1]
+                            invert = latch_map[i][2]
+
+                            if invert:
+                                value = 1 - value
+
+                            path = smt.get_path(topmod, name)
+                            width = smt.net_width(topmod, path)
+
+                            if width == 1:
+                                assert bitidx == 0
+                                smtexpr = "(= [%s] %s)" % (name, "true" if value else "false")
+                            else:
+                                smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value)
+
+                            constr_assumes[0].append((cexfile, smtexpr))
+                continue
+
+            for i in range(len(entry)):
+                if entry[i] == "x":
+                    continue
+
+                if (step == 0) and (i in init_map):
+                    value = int(entry[i])
+                    name = init_map[i][0]
+                    bitidx = init_map[i][1]
+
+                    path = smt.get_path(topmod, name)
+
+                    if not smt.net_exists(topmod, path):
+                        match = re.match(r"(.*)\[(\d+)\]$", path[-1])
+                        if match:
+                            path[-1] = match.group(1)
+                            addr = int(match.group(2))
+
+                        if not match or not smt.mem_exists(topmod, path):
+                            print_msg("Ignoring init value for unknown net: %s" % (name))
+                            continue
+
+                        meminfo = smt.mem_info(topmod, path)
+                        smtexpr = "(select [%s] #b%s)" % (".".join(path), bin(addr)[2:].zfill(meminfo[0]))
+                        width = meminfo[1]
+
+                    else:
+                        smtexpr = "[%s]" % name
+                        width = smt.net_width(topmod, path)
+
+                    if width == 1:
+                        assert bitidx == 0
+                        smtexpr = "(= %s %s)" % (smtexpr, "true" if value else "false")
+                    else:
+                        smtexpr = "(= ((_ extract %d %d) %s) #b%d)" % (bitidx, bitidx, smtexpr, value)
+
+                    constr_assumes[0].append((cexfile, smtexpr))
+
+                if i in input_map:
+                    value = int(entry[i])
+                    name = input_map[i][0]
+                    bitidx = input_map[i][1]
+
+                    path = smt.get_path(topmod, name)
+                    width = smt.net_width(topmod, path)
+
+                    if width == 1:
+                        assert bitidx == 0
+                        smtexpr = "(= [%s] %s)" % (name, "true" if value else "false")
+                    else:
+                        smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value)
+
+                    constr_assumes[step].append((cexfile, smtexpr))
+
+            if not got_topt:
+                skip_steps = max(skip_steps, step)
+                num_steps = max(num_steps, step+1)
+            step += 1
+
 def write_vcd_trace(steps_start, steps_stop, index):
     filename = vcdfile.replace("%", index)
     print_msg("Writing trace to VCD file: %s" % (filename))
@@ -363,14 +589,123 @@ def write_vcd_trace(steps_start, steps_stop, index):
                 if n.startswith("$"):
                     hidden_net = True
             if not hidden_net:
-                vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath))
+                edge = smt.net_clock(topmod, netpath)
+                if edge is None:
+                    vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath))
+                else:
+                    vcd.add_clock([topmod] + netpath, edge)
                 path_list.append(netpath)
 
+        mem_trace_data = dict()
+        for mempath in sorted(smt.hiermems(topmod)):
+            abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath)
+
+            expr_id = list()
+            expr_list = list()
+            for i in range(steps_start, steps_stop):
+                for j in range(rports):
+                    expr_id.append(('R', i-steps_start, j, 'A'))
+                    expr_id.append(('R', i-steps_start, j, 'D'))
+                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
+                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
+                for j in range(wports):
+                    expr_id.append(('W', i-steps_start, j, 'A'))
+                    expr_id.append(('W', i-steps_start, j, 'D'))
+                    expr_id.append(('W', i-steps_start, j, 'M'))
+                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j))
+                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j))
+                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j))
+
+            rdata = list()
+            wdata = list()
+            addrs = set()
+
+            for eid, edat in zip(expr_id, smt.get_list(expr_list)):
+                t, i, j, f = eid
+
+                if t == 'R':
+                    c = rdata
+                elif t == 'W':
+                    c = wdata
+                else:
+                    assert False
+
+                while len(c) <= i:
+                    c.append(list())
+                c = c[i]
+
+                while len(c) <= j:
+                    c.append(dict())
+                c = c[j]
+
+                c[f] = smt.bv2bin(edat)
+
+                if f == 'A':
+                    addrs.add(c[f])
+
+            for addr in addrs:
+                tdata = list()
+                data = ["x"] * width
+                gotread = False
+
+                if len(wdata) == 0 and len(rdata) != 0:
+                    wdata = [[]] * len(rdata)
+
+                assert len(rdata) == len(wdata)
+
+                for i in range(len(wdata)):
+                    if not gotread:
+                        for j_data in rdata[i]:
+                            if j_data["A"] == addr:
+                                data = list(j_data["D"])
+                                gotread = True
+                                break
+
+                        if gotread:
+                            buf = data[:]
+                            for i in reversed(range(len(tdata))):
+                                for k in range(width):
+                                    if tdata[i][k] == "x":
+                                        tdata[i][k] = buf[k]
+                                    else:
+                                        buf[k] = tdata[i][k]
+
+                    if not asyncwr:
+                        tdata.append(data[:])
+
+                    for j_data in wdata[i]:
+                        if j_data["A"] != addr:
+                            continue
+
+                        D = j_data["D"]
+                        M = j_data["M"]
+
+                        for k in range(width):
+                            if M[k] == "1":
+                                data[k] = D[k]
+
+                    if asyncwr:
+                        tdata.append(data[:])
+
+                assert len(tdata) == len(rdata)
+
+                netpath = mempath[:]
+                netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int(addr, 2))
+                vcd.add_net([topmod] + netpath, width)
+
+                for i in range(steps_start, steps_stop):
+                    if i not in mem_trace_data:
+                        mem_trace_data[i] = list()
+                    mem_trace_data[i].append((netpath, "".join(tdata[i-steps_start])))
+
         for i in range(steps_start, steps_stop):
             vcd.set_time(i)
             value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i)
             for path, value in zip(path_list, value_list):
                 vcd.set_net([topmod] + path, value)
+            if i in mem_trace_data:
+                for path, value in mem_trace_data[i]:
+                    vcd.set_net([topmod] + path, value)
 
         vcd.set_time(steps_stop)
 
@@ -379,18 +714,38 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
     filename = vlogtbfile.replace("%", index)
     print_msg("Writing trace to Verilog testbench: %s" % (filename))
 
+    vlogtb_topmod = topmod
+    vlogtb_state = "s@@step_idx@@"
+
+    if vlogtbtop is not None:
+        for item in vlogtbtop.split("."):
+            if item in smt.modinfo[vlogtb_topmod].cells:
+                vlogtb_state = "(|%s_h %s| %s)" % (vlogtb_topmod, item, vlogtb_state)
+                vlogtb_topmod = smt.modinfo[vlogtb_topmod].cells[item]
+            else:
+                print_msg("Vlog top module '%s' not found: no cell '%s' in module '%s'" % (vlogtbtop, item, vlogtb_topmod))
+                break
+
     with open(filename, "w") as f:
+        print("`ifndef VERILATOR", file=f)
         print("module testbench;", file=f)
         print("  reg [4095:0] vcdfile;", file=f)
-        print("  reg clock = 0, genclock = 1;", file=f)
+        print("  reg clock;", file=f)
+        print("`else", file=f)
+        print("module testbench(input clock, output reg genclock);", file=f)
+        print("  initial genclock = 1;", file=f)
+        print("`endif", file=f)
+
+        print("  reg genclock = 1;", file=f)
+        print("  reg [31:0] cycle = 0;", file=f)
 
         primary_inputs = list()
         clock_inputs = set()
 
-        for name in smt.modinfo[topmod].inputs:
+        for name in smt.modinfo[vlogtb_topmod].inputs:
             if name in ["clk", "clock", "CLK", "CLOCK"]:
                 clock_inputs.add(name)
-            width = smt.modinfo[topmod].wsize[name]
+            width = smt.modinfo[vlogtb_topmod].wsize[name]
             primary_inputs.append((name, width))
 
         for name, width in primary_inputs:
@@ -399,27 +754,32 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
             else:
                 print("  reg [%d:0] PI_%s;" % (width-1, name), file=f)
 
-        print("  %s UUT (" % topmod, file=f)
+        print("  %s UUT (" % vlogtb_topmod, file=f)
         print(",\n".join("    .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f)
         print("  );", file=f)
 
+        print("`ifndef VERILATOR", file=f)
         print("  initial begin", file=f)
         print("    if ($value$plusargs(\"vcd=%s\", vcdfile)) begin", file=f)
         print("      $dumpfile(vcdfile);", file=f)
         print("      $dumpvars(0, testbench);", file=f)
         print("    end", file=f)
+        print("    #5 clock = 0;", file=f)
         print("    while (genclock) begin", file=f)
-        print("      #5; clock = 0;", file=f)
-        print("      #5; clock = 1;", file=f)
+        print("      #5 clock = 0;", file=f)
+        print("      #5 clock = 1;", file=f)
         print("    end", file=f)
         print("  end", file=f)
+        print("`endif", file=f)
 
         print("  initial begin", file=f)
 
-        regs = sorted(smt.hiernets(topmod, regs_only=True))
-        regvals = smt.get_net_bin_list(topmod, regs, "s%d" % steps_start)
+        regs = sorted(smt.hiernets(vlogtb_topmod, regs_only=True))
+        regvals = smt.get_net_bin_list(vlogtb_topmod, regs, vlogtb_state.replace("@@step_idx@@", str(steps_start)))
 
+        print("`ifndef VERILATOR", file=f)
         print("    #1;", file=f)
+        print("`endif", file=f)
         for reg, val in zip(regs, regvals):
             hidden_net = False
             for n in reg:
@@ -427,40 +787,74 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
                     hidden_net = True
             print("    %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(reg), len(val), val), file=f)
 
-        mems = sorted(smt.hiermems(topmod))
+        anyconsts = sorted(smt.hieranyconsts(vlogtb_topmod))
+        for info in anyconsts:
+            if info[3] is not None:
+                modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(steps_start)), info[0])
+                value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
+                print("    UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
+
+        mems = sorted(smt.hiermems(vlogtb_topmod))
         for mempath in mems:
-            abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
-            mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
+            abits, width, rports, wports, asyncwr = smt.mem_info(vlogtb_topmod, mempath)
 
             addr_expr_list = list()
+            data_expr_list = list()
             for i in range(steps_start, steps_stop):
-                for j in range(ports):
-                    addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, j))
+                for j in range(rports):
+                    addr_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
+                    data_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))
 
-            addr_list = set()
-            for val in smt.get_list(addr_expr_list):
-                addr_list.add(smt.bv2int(val))
+            addr_list = smt.get_list(addr_expr_list)
+            data_list = smt.get_list(data_expr_list)
 
-            expr_list = list()
-            for i in addr_list:
-                expr_list.append("(select %s #b%s)" % (mem, format(i, "0%db" % abits)))
+            addr_data = dict()
+            for addr, data in zip(addr_list, data_list):
+                addr = smt.bv2bin(addr)
+                data = smt.bv2bin(data)
+                if addr not in addr_data:
+                    addr_data[addr] = data
 
-            for i, val in zip(addr_list, smt.get_list(expr_list)):
-                val = smt.bv2bin(val)
-                print("    UUT.%s[%d] = %d'b%s;" % (".".join(mempath), i, len(val), val), file=f)
+            for addr, data in addr_data.items():
+                print("    UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath), len(addr), addr, len(data), data), file=f)
+
+        print("", file=f)
+        anyseqs = sorted(smt.hieranyseqs(vlogtb_topmod))
 
         for i in range(steps_start, steps_stop):
             pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs]
-            pi_values = smt.get_net_bin_list(topmod, pi_names, "s%d" % i)
+            pi_values = smt.get_net_bin_list(vlogtb_topmod, pi_names, vlogtb_state.replace("@@step_idx@@", str(i)))
 
-            print("    #1;", file=f)
             print("    // state %d" % i, file=f)
+
             if i > 0:
-                print("    @(posedge clock);", file=f)
+                print("    if (cycle == %d) begin" % (i-1), file=f)
+
             for name, val in zip(pi_names, pi_values):
-                print("    PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f)
+                if i > 0:
+                    print("      PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f)
+                else:
+                    print("    PI_%s = %d'b%s;" % (".".join(name), len(val), val), file=f)
+
+            for info in anyseqs:
+                if info[3] is not None:
+                    modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), info[0])
+                    value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
+                    if i > 0:
+                        print("      UUT.%s <= %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
+                    else:
+                        print("    UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
+
+            if i > 0:
+                print("    end", file=f)
+                print("", file=f)
+
+            if i == 0:
+                print("  end", file=f)
+                print("  always @(posedge clock) begin", file=f)
 
-        print("    genclock = 0;", file=f)
+        print("    genclock <= cycle < %d;" % (steps_stop-1), file=f)
+        print("    cycle <= cycle + 1;", file=f)
         print("  end", file=f)
 
         print("endmodule", file=f)
@@ -470,52 +864,71 @@ def write_constr_trace(steps_start, steps_stop, index):
     filename = outconstr.replace("%", index)
     print_msg("Writing trace to constraints file: %s" % (filename))
 
+    constr_topmod = topmod
+    constr_state = "s@@step_idx@@"
+    constr_prefix = ""
+
+    if smtctop is not None:
+        for item in smtctop[0].split("."):
+            assert item in smt.modinfo[constr_topmod].cells
+            constr_state = "(|%s_h %s| %s)" % (constr_topmod, item, constr_state)
+            constr_topmod = smt.modinfo[constr_topmod].cells[item]
+        if smtctop[1] != "":
+            constr_prefix = smtctop[1] + "."
+
+    if smtcinit:
+        steps_start = steps_stop - 1
+
     with open(filename, "w") as f:
         primary_inputs = list()
 
-        for name in smt.modinfo[topmod].inputs:
-            width = smt.modinfo[topmod].wsize[name]
+        for name in smt.modinfo[constr_topmod].inputs:
+            width = smt.modinfo[constr_topmod].wsize[name]
             primary_inputs.append((name, width))
 
-        if steps_start == 0:
+        if steps_start == 0 or smtcinit:
             print("initial", file=f)
         else:
             print("state %d" % steps_start, file=f)
 
-        regnames = sorted(smt.hiernets(topmod, regs_only=True))
-        regvals = smt.get_net_list(topmod, regnames, "s%d" % steps_start)
+        regnames = sorted(smt.hiernets(constr_topmod, regs_only=True))
+        regvals = smt.get_net_list(constr_topmod, regnames, constr_state.replace("@@step_idx@@", str(steps_start)))
 
         for name, val in zip(regnames, regvals):
-            print("assume (= [%s] %s)" % (".".join(name), val), file=f)
+            print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
 
-        mems = sorted(smt.hiermems(topmod))
+        mems = sorted(smt.hiermems(constr_topmod))
         for mempath in mems:
-            abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
-            mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
+            abits, width, rports, wports, asyncwr = smt.mem_info(constr_topmod, mempath)
 
             addr_expr_list = list()
+            data_expr_list = list()
             for i in range(steps_start, steps_stop):
-                for j in range(ports):
-                    addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, j))
+                for j in range(rports):
+                    addr_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
+                    data_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))
 
-            addr_list = set((smt.bv2int(val) for val in smt.get_list(addr_expr_list)))
+            addr_list = smt.get_list(addr_expr_list)
+            data_list = smt.get_list(data_expr_list)
 
-            expr_list = list()
-            for i in addr_list:
-                expr_list.append("(select %s #b%s)" % (mem, format(i, "0%db" % abits)))
+            addr_data = dict()
+            for addr, data in zip(addr_list, data_list):
+                if addr not in addr_data:
+                    addr_data[addr] = data
 
-            for i, val in zip(addr_list, smt.get_list(expr_list)):
-                print("assume (= (select [%s] #b%s) %s)" % (".".join(mempath), format(i, "0%db" % abits), val), file=f)
+            for addr, data in addr_data.items():
+                print("assume (= (select [%s%s] %s) %s)" % (constr_prefix, ".".join(mempath), addr, data), file=f)
 
         for k in range(steps_start, steps_stop):
-            print("", file=f)
-            print("state %d" % k, file=f)
+            if not smtcinit:
+                print("", file=f)
+                print("state %d" % k, file=f)
 
             pi_names = [[name] for name, _ in sorted(primary_inputs)]
-            pi_values = smt.get_net_list(topmod, pi_names, "s%d" % k)
+            pi_values = smt.get_net_list(constr_topmod, pi_names, constr_state.replace("@@step_idx@@", str(k)))
 
             for name, val in zip(pi_names, pi_values):
-                print("assume (= [%s] %s)" % (".".join(name), val), file=f)
+                print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
 
 
 def write_trace(steps_start, steps_stop, index):
@@ -529,30 +942,40 @@ def write_trace(steps_start, steps_stop, index):
         write_constr_trace(steps_start, steps_stop, index)
 
 
-def print_failed_asserts_worker(mod, state, path):
+def print_failed_asserts_worker(mod, state, path, extrainfo):
     assert mod in smt.modinfo
+    found_failed_assert = False
 
     if smt.get("(|%s_a| %s)" % (mod, state)) in ["true", "#b1"]:
         return
 
     for cellname, celltype in smt.modinfo[mod].cells.items():
-        print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
+        if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo):
+            found_failed_assert = True
 
     for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
         if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]:
-            print_msg("Assert failed in %s: %s" % (path, assertinfo))
+            print_msg("Assert failed in %s: %s%s" % (path, assertinfo, extrainfo))
+            found_failed_assert = True
+
+    return found_failed_assert
 
 
-def print_failed_asserts(state, final=False):
+def print_failed_asserts(state, final=False, extrainfo=""):
     if noinfo: return
     loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True)
+    found_failed_assert = False
 
     for loc, expr, value in zip(loc_list, expr_list, value_list):
         if smt.bv2int(value) == 0:
-            print_msg("Assert %s failed: %s" % (loc, expr))
+            print_msg("Assert %s failed: %s%s" % (loc, expr, extrainfo))
+            found_failed_assert = True
 
     if not final:
-        print_failed_asserts_worker(topmod, "s%d" % state, topmod)
+        if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo):
+            found_failed_assert = True
+
+    return found_failed_assert
 
 
 def print_anyconsts_worker(mod, state, path):
@@ -562,7 +985,10 @@ def print_anyconsts_worker(mod, state, path):
         print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
 
     for fun, info in smt.modinfo[mod].anyconsts.items():
-        print_msg("Value for anyconst in %s (%s): %d" % (path, info, smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+        if info[1] is None:
+            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)))))
 
 
 def print_anyconsts(state):
@@ -570,23 +996,183 @@ def print_anyconsts(state):
     print_anyconsts_worker(topmod, "s%d" % state, topmod)
 
 
+def get_cover_list(mod, base):
+    assert mod in smt.modinfo
+
+    cover_expr = list()
+    cover_desc = list()
+
+    for expr, desc in smt.modinfo[mod].covers.items():
+        cover_expr.append("(ite (|%s| %s) #b1 #b0)" % (expr, base))
+        cover_desc.append(desc)
+
+    for cell, submod in smt.modinfo[mod].cells.items():
+        e, d = get_cover_list(submod, "(|%s_h %s| %s)" % (mod, cell, base))
+        cover_expr += e
+        cover_desc += d
+
+    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(expr):
+    if expr == "true":
+        return
+
+    smt.write("(assert %s)" % expr)
+
+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("(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("(|%s_a| s%d)" % (topmod, step))
+            smt_assert(get_constr_expr(constr_asserts, step))
 
         if step > num_steps-skip_steps:
             print_msg("Skipping induction in step %d.." % (step))
@@ -600,9 +1186,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, '%')
@@ -613,33 +1199,135 @@ 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
 
+elif covermode:
+    cover_expr, cover_desc = get_cover_list(topmod, "state")
+    cover_mask = "1" * len(cover_desc)
+
+    if len(cover_expr) > 1:
+        cover_expr = "(concat %s)" % " ".join(cover_expr)
+    elif len(cover_expr) == 1:
+        cover_expr = cover_expr[0]
+    else:
+        cover_expr = "#b0"
+
+    coveridx = 0
+    smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
 
-else:  # not tempind
+    step = 0
+    retstatus = False
+    found_failed_assert = False
+
+    assert step_size == 1
+
+    while step < num_steps:
+        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_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
+            else:
+                smt_assert_antecedent("(|%s_i| s0)" % (topmod))
+                smt_assert_antecedent("(|%s_is| s0)" % (topmod))
+
+        else:
+            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_push()
+            smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx, step, "0" * len(cover_desc)))
+
+            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_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"
+
+            reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
+            assert len(reached_covers) == len(cover_desc)
+
+            new_cover_mask = []
+
+            for i in range(len(reached_covers)):
+                if reached_covers[i] == "0":
+                    new_cover_mask.append(cover_mask[i])
+                    continue
+
+                print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step))
+                new_cover_mask.append("0")
+
+            cover_mask = "".join(new_cover_mask)
+
+            for i in range(step+1+append_steps):
+                if print_failed_asserts(i, extrainfo=" (step %d)" % i):
+                    found_failed_assert = True
+
+            write_trace(0, step+1+append_steps, "%d" % coveridx)
+
+            if found_failed_assert:
+                break
+
+            coveridx += 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:
+            break
+
+        if "1" not in cover_mask:
+            retstatus = True
+            break
+
+        step += 1
+
+    if "1" in cover_mask:
+        for i in range(len(cover_mask)):
+            if cover_mask[i] == "1":
+                print_msg("Unreached cover statement at %s." % cover_desc[i])
+
+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:
-            smt.write("(assert (|%s_i| s0))" % (topmod))
-            smt.write("(assert (|%s_is| s0))" % (topmod))
+            if noinit:
+                smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
+            else:
+                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("(|%s_a| s%d)" % (topmod, step))
+                smt_assert(get_constr_expr(constr_asserts, step))
             else:
                 print_msg("Skipping step %d.." % (step))
             step += 1
@@ -648,39 +1336,61 @@ else:  # not tempind
         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 (|%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:
+            if presat:
+                if last_check_step == step:
+                    print_msg("Checking assumptions in step %d.." % (step))
+                else:
+                    print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
+
+                if smt_check_sat() == "unsat":
+                    print("%s Warmup failed!" % smt.timestamp())
+                    retstatus = False
+                    break
+
             if not final_only:
                 if last_check_step == step:
-                    print_msg("Checking asserts in step %d.." % (step))
+                    print_msg("Checking assertions in step %d.." % (step))
                 else:
-                    print_msg("Checking asserts in steps %d to %d.." % (step, last_check_step))
-                smt.write("(push 1)")
+                    print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step))
+                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("(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_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)
-                    write_trace(0, last_check_step+1, '%')
+                    write_trace(0, last_check_step+1+append_steps, '%')
                     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("(|%s_a| s%d)" % (topmod, i))
+                    smt_assert(get_constr_expr(constr_asserts, i))
 
             if constr_final_start is not None:
                 for i in range(step, last_check_step+1):
@@ -688,12 +1398,12 @@ else:  # not tempind
                         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("(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)
@@ -701,17 +1411,17 @@ else:  # not tempind
                         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("(|%s_a| s%d)" % (topmod, i))
+                smt_assert(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
@@ -722,7 +1432,7 @@ else:  # not tempind
 
         step += step_size
 
-    if gentrace:
+    if gentrace and retstatus:
         print_anyconsts(0)
         write_trace(0, num_steps, '%')
 
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 865eed1f..3fc823e3 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -1,4 +1,3 @@
-#!/usr/bin/env python3
 #
 # yosys -- Yosys Open SYnthesis Suite
 #
@@ -17,10 +16,55 @@
 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 #
 
-import sys, subprocess, re
+import sys, re, os, signal
+import subprocess
+if os.name == "posix":
+    import resource
 from copy import deepcopy
 from select import select
 from time import time
+from queue import Queue, Empty
+from threading import Thread
+
+
+# This is needed so that the recursive SMT2 S-expression parser
+# does not run out of stack frames when parsing large expressions
+if os.name == "posix":
+    smtio_reclimit = 64 * 1024
+    smtio_stacksize = 128 * 1024 * 1024
+    if sys.getrecursionlimit() < smtio_reclimit:
+        sys.setrecursionlimit(smtio_reclimit)
+    if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize:
+        resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1))
+
+
+# currently running solvers (so we can kill them)
+running_solvers = dict()
+forced_shutdown = False
+solvers_index = 0
+
+def force_shutdown(signum, frame):
+    global forced_shutdown
+    if not forced_shutdown:
+        forced_shutdown = True
+        if signum is not None:
+            print("<%s>" % signal.Signals(signum).name)
+        for p in running_solvers.values():
+            # os.killpg(os.getpgid(p.pid), signal.SIGTERM)
+            os.kill(p.pid, signal.SIGTERM)
+    sys.exit(1)
+
+if os.name == "posix":
+    signal.signal(signal.SIGHUP, force_shutdown)
+signal.signal(signal.SIGINT, force_shutdown)
+signal.signal(signal.SIGTERM, force_shutdown)
+
+def except_hook(exctype, value, traceback):
+    if not forced_shutdown:
+        sys.__excepthook__(exctype, value, traceback)
+    force_shutdown(None, None)
+
+sys.excepthook = except_hook
 
 
 hex_dict = {
@@ -41,25 +85,38 @@ class SmtModInfo:
         self.memories = dict()
         self.wires = set()
         self.wsize = dict()
+        self.clocks = dict()
         self.cells = dict()
         self.asserts = dict()
+        self.covers = dict()
         self.anyconsts = dict()
+        self.anyseqs = dict()
+        self.allconsts = dict()
+        self.allseqs = dict()
+        self.asize = dict()
 
 
 class SmtIo:
     def __init__(self, opts=None):
+        global solvers_index
+
         self.logic = None
         self.logic_qf = True
         self.logic_ax = True
         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
+        self.p_index = solvers_index
+        solvers_index += 1
 
         if opts is not None:
             self.logic = opts.logic
             self.solver = opts.solver
+            self.solver_opts = opts.solver_opts
             self.debug_print = opts.debug_print
             self.debug_file = opts.debug_file
             self.dummy_file = opts.dummy_file
@@ -70,34 +127,57 @@ class SmtIo:
             self.nocomments = opts.nocomments
 
         else:
-            self.solver = "z3"
+            self.solver = "yices"
+            self.solver_opts = list()
             self.debug_print = False
             self.debug_file = None
             self.dummy_file = None
-            self.timeinfo = True
+            self.timeinfo = os.name != "nt"
             self.unroll = False
             self.noincr = False
             self.info_stmts = list()
             self.nocomments = False
 
+        self.start_time = time()
+
+        self.modinfo = dict()
+        self.curmod = None
+        self.topmod = None
+        self.setup_done = False
+
+    def __del__(self):
+        if self.p is not None and not forced_shutdown:
+            os.killpg(os.getpgid(self.p.pid), signal.SIGTERM)
+            if running_solvers is not None:
+                del running_solvers[self.p_index]
+
+    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.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
 
         if self.solver == "z3":
-            self.popen_vargs = ['z3', '-smt2', '-in']
+            self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
 
         if self.solver == "cvc4":
-            self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
+            self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
 
         if self.solver == "mathsat":
-            self.popen_vargs = ['mathsat']
+            self.popen_vargs = ['mathsat'] + self.solver_opts
 
         if self.solver == "boolector":
-            self.popen_vargs = ['boolector', '--smt2', '-i']
+            self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
             self.unroll = True
 
         if self.solver == "abc":
-            self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
+            if len(self.solver_opts) > 0:
+                self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]
+            else:
+                self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
             self.logic_ax = False
             self.unroll = True
             self.noincr = True
@@ -109,9 +189,10 @@ class SmtIo:
             if self.dummy_file is not None:
                 self.dummy_fd = open(self.dummy_file, "w")
             if not self.noincr:
-                self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+                self.p_open()
 
         if self.unroll:
+            assert not self.forall
             self.logic_uf = False
             self.unroll_idcnt = 0
             self.unroll_buffer = ""
@@ -121,36 +202,27 @@ class SmtIo:
             self.unroll_cache = dict()
             self.unroll_stack = list()
 
-        self.start_time = time()
-
-        self.modinfo = dict()
-        self.curmod = None
-        self.topmod = None
-        self.setup_done = False
-
-    def setup(self):
-        assert not self.setup_done
-
         if self.logic is None:
             self.logic = ""
             if self.logic_qf: self.logic += "QF_"
             if self.logic_ax: self.logic += "A"
             if self.logic_uf: self.logic += "UF"
             if self.logic_bv: self.logic += "BV"
+            if self.logic_dt: self.logic = "ALL"
 
         self.setup_done = True
 
+        for stmt in self.info_stmts:
+            self.write(stmt)
+
         if self.produce_models:
             self.write("(set-option :produce-models true)")
 
         self.write("(set-logic %s)" % self.logic)
 
-        for stmt in self.info_stmts:
-            self.write(stmt)
-
     def timestamp(self):
         secs = int(time() - self.start_time)
-        return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
+        return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60)
 
     def replace_in_stmt(self, stmt, pat, repl):
         if stmt == pat:
@@ -201,18 +273,75 @@ class SmtIo:
 
         return stmt
 
+    def p_thread_main(self):
+        while True:
+            data = self.p.stdout.readline().decode("ascii")
+            if data == "": break
+            self.p_queue.put(data)
+        self.p_queue.put("")
+        self.p_running = False
+
+    def p_open(self):
+        assert self.p is None
+        self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+        running_solvers[self.p_index] = self.p
+        self.p_running = True
+        self.p_next = None
+        self.p_queue = Queue()
+        self.p_thread = Thread(target=self.p_thread_main)
+        self.p_thread.start()
+
+    def p_write(self, data, flush):
+        assert self.p is not None
+        self.p.stdin.write(bytes(data, "ascii"))
+        if flush: self.p.stdin.flush()
+
+    def p_read(self):
+        assert self.p is not None
+        if self.p_next is not None:
+            data = self.p_next
+            self.p_next = None
+            return data
+        if not self.p_running:
+            return ""
+        return self.p_queue.get()
+
+    def p_poll(self, timeout=0.1):
+        assert self.p is not None
+        assert self.p_running
+        if self.p_next is not None:
+            return False
+        try:
+            self.p_next = self.p_queue.get(True, timeout)
+            return False
+        except Empty:
+            return True
+
+    def p_close(self):
+        assert self.p is not None
+        self.p.stdin.close()
+        self.p_thread.join()
+        assert not self.p_running
+        del running_solvers[self.p_index]
+        self.p = None
+        self.p_next = None
+        self.p_queue = None
+        self.p_thread = None
+
     def write(self, stmt, unroll=True):
         if stmt.startswith(";"):
             self.info(stmt)
+            if not self.setup_done:
+                self.info_stmts.append(stmt)
+                return
         elif not self.setup_done:
             self.setup()
 
         stmt = stmt.strip()
 
         if self.nocomments or self.unroll:
-            if stmt.startswith(";"):
-                return
-            stmt = re.sub(r" ;.*", "", stmt)
+            stmt = re.sub(r" *;.*", "", stmt)
+            if stmt == "": return
 
         if unroll and self.unroll:
             stmt = self.unroll_buffer + stmt
@@ -271,20 +400,17 @@ class SmtIo:
         if self.solver != "dummy":
             if self.noincr:
                 if self.p is not None and not stmt.startswith("(get-"):
-                    self.p.stdin.close()
-                    self.p = None
+                    self.p_close()
                 if stmt == "(push 1)":
                     self.smt2cache.append(list())
                 elif stmt == "(pop 1)":
                     self.smt2cache.pop()
                 else:
                     if self.p is not None:
-                        self.p.stdin.write(bytes(stmt + "\n", "ascii"))
-                        self.p.stdin.flush()
+                        self.p_write(stmt + "\n", True)
                     self.smt2cache[-1].append(stmt)
             else:
-                self.p.stdin.write(bytes(stmt + "\n", "ascii"))
-                self.p.stdin.flush()
+                self.p_write(stmt + "\n", True)
 
     def info(self, stmt):
         if not stmt.startswith("; yosys-smt2-"):
@@ -300,6 +426,15 @@ class SmtIo:
             if self.logic is None:
                 self.logic_bv = False
 
+        if fields[1] == "yosys-smt2-stdt":
+            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()
@@ -323,17 +458,40 @@ class SmtIo:
             self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
 
         if fields[1] == "yosys-smt2-memory":
-            self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4]), int(fields[5]))
+            self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4]), int(fields[5]), int(fields[6]), fields[7] == "async")
 
         if fields[1] == "yosys-smt2-wire":
             self.modinfo[self.curmod].wires.add(fields[2])
             self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
 
+        if fields[1] == "yosys-smt2-clock":
+            for edge in fields[3:]:
+                if fields[2] not in self.modinfo[self.curmod].clocks:
+                    self.modinfo[self.curmod].clocks[fields[2]] = edge
+                elif self.modinfo[self.curmod].clocks[fields[2]] != edge:
+                    self.modinfo[self.curmod].clocks[fields[2]] = "event"
+
         if fields[1] == "yosys-smt2-assert":
-            self.modinfo[self.curmod].asserts[fields[2]] = fields[3]
+            self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
+
+        if fields[1] == "yosys-smt2-cover":
+            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]
+            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[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):
@@ -347,6 +505,54 @@ class SmtIo:
         hiernets_worker(nets, top, [])
         return nets
 
+    def hieranyconsts(self, top):
+        def worker(results, mod, cursor):
+            for name, value in sorted(self.modinfo[mod].anyconsts.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 hieranyseqs(self, top):
+        def worker(results, mod, cursor):
+            for name, value in sorted(self.modinfo[mod].anyseqs.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 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])
+
+        results = list()
+        worker(results, top, [])
+        return results
+
     def hiermems(self, top):
         def hiermems_worker(mems, mod, cursor):
             for memname in sorted(self.modinfo[mod].memories.keys()):
@@ -366,7 +572,7 @@ class SmtIo:
             if self.solver == "dummy":
                 line = self.dummy_fd.readline().strip()
             else:
-                line = self.p.stdout.readline().decode("ascii").strip()
+                line = self.p_read().strip()
                 if self.dummy_file is not None:
                     self.dummy_fd.write(line + "\n")
 
@@ -379,12 +585,14 @@ class SmtIo:
             if count_brackets == 0:
                 break
             if self.solver != "dummy" and self.p.poll():
-                print("SMT Solver terminated unexpectedly: %s" % "".join(stmt))
+                print("%s Solver terminated unexpectedly: %s" % (self.timestamp(), "".join(stmt)), flush=True)
                 sys.exit(1)
 
         stmt = "".join(stmt)
         if stmt.startswith("(error"):
-            print("SMT Solver Error: %s" % stmt, file=sys.stderr)
+            print("%s Solver Error: %s" % (self.timestamp(), stmt), flush=True)
+            if self.solver != "dummy":
+                self.p_close()
             sys.exit(1)
 
         return stmt
@@ -399,15 +607,13 @@ class SmtIo:
         if self.solver != "dummy":
             if self.noincr:
                 if self.p is not None:
-                    self.p.stdin.close()
-                    self.p = None
-                self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+                    self.p_close()
+                self.p_open()
                 for cache_ctx in self.smt2cache:
                     for cache_stmt in cache_ctx:
-                        self.p.stdin.write(bytes(cache_stmt + "\n", "ascii"))
+                        self.p_write(cache_stmt + "\n", False)
 
-            self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
-            self.p.stdin.flush()
+            self.p_write("(check-sat)\n", True)
 
             if self.timeinfo:
                 i = 0
@@ -415,7 +621,7 @@ class SmtIo:
 
                 count = 0
                 num_bs = 0
-                while select([self.p.stdout], [], [], 0.1) == ([], [], []):
+                while self.p_poll():
                     count += 1
 
                     if count < 25:
@@ -444,11 +650,43 @@ class SmtIo:
                     print("\b \b" * num_bs, end="", file=sys.stderr)
                     sys.stderr.flush()
 
+            else:
+                count = 0
+                while self.p_poll(60):
+                    count += 1
+                    msg = None
+
+                    if count == 1:
+                        msg = "1 minute"
+
+                    elif count in [5, 10, 15, 30]:
+                        msg = "%d minutes" % count
+
+                    elif count == 60:
+                        msg = "1 hour"
+
+                    elif count % 60 == 0:
+                        msg = "%d hours" % (count // 60)
+
+                    if msg is not None:
+                        print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True)
+
         result = self.read()
+
         if self.debug_file:
             print("(set-info :status %s)" % result, file=self.debug_file)
             print("(check-sat)", file=self.debug_file)
             self.debug_file.flush()
+
+        if result not in ["sat", "unsat"]:
+            if result == "":
+                print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True)
+            else:
+                print("%s Unexpected response from solver: %s" % (self.timestamp(), result), flush=True)
+            if self.solver != "dummy":
+                self.p_close()
+            sys.exit(1)
+
         return result
 
     def parse(self, stmt):
@@ -503,6 +741,9 @@ class SmtIo:
         return h
 
     def bv2bin(self, v):
+        if type(v) is list and len(v) == 3 and v[0] == "_" and v[1].startswith("bv"):
+            x, n = int(v[1][2:]), int(v[2])
+            return "".join("1" if (x & (1 << i)) else "0" for i in range(n-1, -1, -1))
         if v == "true": return "1"
         if v == "false": return "0"
         if v.startswith("#b"):
@@ -539,6 +780,9 @@ class SmtIo:
         return [".".join(path)]
 
     def net_expr(self, mod, base, path):
+        if len(path) == 0:
+            return base
+
         if len(path) == 1:
             assert mod in self.modinfo
             if path[0] == "":
@@ -568,23 +812,54 @@ class SmtIo:
         assert net_path[-1] in self.modinfo[mod].wsize
         return self.modinfo[mod].wsize[net_path[-1]]
 
-    def mem_expr(self, mod, base, path, portidx=None, infomode=False):
+    def net_clock(self, mod, net_path):
+        for i in range(len(net_path)-1):
+            assert mod in self.modinfo
+            assert net_path[i] in self.modinfo[mod].cells
+            mod = self.modinfo[mod].cells[net_path[i]]
+
+        assert mod in self.modinfo
+        if net_path[-1] not in self.modinfo[mod].clocks:
+            return None
+        return self.modinfo[mod].clocks[net_path[-1]]
+
+    def net_exists(self, mod, net_path):
+        for i in range(len(net_path)-1):
+            if mod not in self.modinfo: return False
+            if net_path[i] not in self.modinfo[mod].cells: return False
+            mod = self.modinfo[mod].cells[net_path[i]]
+
+        if mod not in self.modinfo: return False
+        if net_path[-1] not in self.modinfo[mod].wsize: return False
+        return True
+
+    def mem_exists(self, mod, mem_path):
+        for i in range(len(mem_path)-1):
+            if mod not in self.modinfo: return False
+            if mem_path[i] not in self.modinfo[mod].cells: return False
+            mod = self.modinfo[mod].cells[mem_path[i]]
+
+        if mod not in self.modinfo: return False
+        if mem_path[-1] not in self.modinfo[mod].memories: return False
+        return True
+
+    def mem_expr(self, mod, base, path, port=None, infomode=False):
         if len(path) == 1:
             assert mod in self.modinfo
             assert path[0] in self.modinfo[mod].memories
             if infomode:
                 return self.modinfo[mod].memories[path[0]]
-            return "(|%s_m%s %s| %s)" % (mod, "" if portidx is None else ":%d" % portidx, path[0], base)
+            return "(|%s_m%s %s| %s)" % (mod, "" if port is None else ":%s" % port, path[0], base)
 
         assert mod in self.modinfo
         assert path[0] in self.modinfo[mod].cells
 
         nextmod = self.modinfo[mod].cells[path[0]]
         nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
-        return self.mem_expr(nextmod, nextbase, path[1:], portidx=portidx, infomode=infomode)
+        return self.mem_expr(nextmod, nextbase, path[1:], port=port, infomode=infomode)
 
-    def mem_info(self, mod, base, path):
-        return self.mem_expr(mod, base, path, infomode=True)
+    def mem_info(self, mod, path):
+        return self.mem_expr(mod, "", path, infomode=True)
 
     def get_net(self, mod_name, net_path, state_name):
         return self.get(self.net_expr(mod_name, state_name, net_path))
@@ -607,19 +882,21 @@ class SmtIo:
     def wait(self):
         if self.p is not None:
             self.p.wait()
+            self.p_close()
 
 
 class SmtOpts:
     def __init__(self):
-        self.shortopts = "s:v"
+        self.shortopts = "s:S:v"
         self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
-        self.solver = "z3"
+        self.solver = "yices"
+        self.solver_opts = list()
         self.debug_print = False
         self.debug_file = None
         self.dummy_file = None
         self.unroll = False
         self.noincr = False
-        self.timeinfo = True
+        self.timeinfo = os.name != "nt"
         self.logic = None
         self.info_stmts = list()
         self.nocomments = False
@@ -627,6 +904,8 @@ class SmtOpts:
     def handle(self, o, a):
         if o == "-s":
             self.solver = a
+        elif o == "-S":
+            self.solver_opts.append(a)
         elif o == "-v":
             self.debug_print = True
         elif o == "--unroll":
@@ -634,7 +913,7 @@ class SmtOpts:
         elif o == "--noincr":
             self.noincr = True
         elif o == "--noprogress":
-            self.timeinfo = True
+            self.timeinfo = False
         elif o == "--dump-smt2":
             self.debug_file = open(a, "w")
         elif o == "--logic":
@@ -652,8 +931,11 @@ class SmtOpts:
     def helpmsg(self):
         return """
     -s <solver>
-        set SMT solver: z3, cvc4, yices, mathsat, boolector, dummy
-        default: z3
+        set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
+        default: yices
+
+    -S <opt>
+        pass <opt> as command line argument to the solver
 
     --logic <smt2_logic>
         use the specified SMT2 logic (e.g. QF_AUFBV)
@@ -674,6 +956,7 @@ class SmtOpts:
 
     --noprogress
         disable timer display during solving
+        (this option is set implicitly on Windows)
 
     --dump-smt2 <filename>
         write smt2 statements to file
@@ -691,6 +974,7 @@ class MkVcd:
         self.f = f
         self.t = -1
         self.nets = dict()
+        self.clocks = dict()
 
     def add_net(self, path, width):
         path = tuple(path)
@@ -698,11 +982,25 @@ class MkVcd:
         key = "n%d" % len(self.nets)
         self.nets[path] = (key, width)
 
+    def add_clock(self, path, edge):
+        path = tuple(path)
+        assert self.t == -1
+        key = "n%d" % len(self.nets)
+        self.nets[path] = (key, 1)
+        self.clocks[path] = (key, edge)
+
     def set_net(self, path, bits):
         path = tuple(path)
         assert self.t >= 0
         assert path in self.nets
-        print("b%s %s" % (bits, self.nets[path][0]), file=self.f)
+        if path not in self.clocks:
+            print("b%s %s" % (bits, self.nets[path][0]), file=self.f)
+
+    def escape_name(self, name):
+        name = re.sub(r"\[([0-9a-zA-Z_]*[a-zA-Z_][0-9a-zA-Z_]*)\]", r"<\1>", name)
+        if re.match("[\[\]]", name) and name[0] != "\\":
+            name = "\\" + name
+        return name
 
     def set_time(self, t):
         assert t >= self.t
@@ -710,22 +1008,52 @@ class MkVcd:
             if self.t == -1:
                 print("$var integer 32 t smt_step $end", file=self.f)
                 print("$var event 1 ! smt_clock $end", file=self.f)
+
                 scope = []
                 for path in sorted(self.nets):
-                    while len(scope)+1 > len(path) or (len(scope) > 0 and scope[-1] != path[len(scope)-1]):
+                    key, width = self.nets[path]
+
+                    uipath = list(path)
+                    if "." in uipath[-1]:
+                        uipath = uipath[0:-1] + uipath[-1].split(".")
+                    for i in range(len(uipath)):
+                        uipath[i] = re.sub(r"\[([^\]]*)\]", r"<\1>", uipath[i])
+
+                    while uipath[:len(scope)] != scope:
                         print("$upscope $end", file=self.f)
                         scope = scope[:-1]
-                    while len(scope)+1 < len(path):
-                        print("$scope module %s $end" % path[len(scope)], file=self.f)
-                        scope.append(path[len(scope)-1])
-                    key, width = self.nets[path]
-                    print("$var wire %d %s %s $end" % (width, key, path[-1]), file=self.f)
+
+                    while uipath[:-1] != scope:
+                        print("$scope module %s $end" % uipath[len(scope)], file=self.f)
+                        scope.append(uipath[len(scope)])
+
+                    if path in self.clocks and self.clocks[path][1] == "event":
+                        print("$var event 1 %s %s $end" % (key, uipath[-1]), file=self.f)
+                    else:
+                        print("$var wire %d %s %s $end" % (width, key, uipath[-1]), file=self.f)
+
                 for i in range(len(scope)):
                     print("$upscope $end", file=self.f)
+
                 print("$enddefinitions $end", file=self.f)
+
             self.t = t
             assert self.t >= 0
+
+            if self.t > 0:
+                print("#%d" % (10 * self.t - 5), file=self.f)
+                for path in sorted(self.clocks.keys()):
+                    if self.clocks[path][1] == "posedge":
+                        print("b0 %s" % self.nets[path][0], file=self.f)
+                    elif self.clocks[path][1] == "negedge":
+                        print("b1 %s" % self.nets[path][0], file=self.f)
+
             print("#%d" % (10 * self.t), file=self.f)
             print("1!", file=self.f)
             print("b%s t" % format(self.t, "032b"), file=self.f)
 
+            for path in sorted(self.clocks.keys()):
+                if self.clocks[path][1] == "negedge":
+                    print("b0 %s" % self.nets[path][0], file=self.f)
+                else:
+                    print("b1 %s" % self.nets[path][0], file=self.f)