diff --git a/.github/ISSUE_TEMPLATE/bug_report.yml b/.github/ISSUE_TEMPLATE/bug_report.yml
index ca9cb4811..27cfd09b7 100644
--- a/.github/ISSUE_TEMPLATE/bug_report.yml
+++ b/.github/ISSUE_TEMPLATE/bug_report.yml
@@ -25,6 +25,19 @@ body:
     validations:
       required: true
 
+  - type: dropdown
+    id: os
+    attributes:
+      label: On which OS did this happen?
+      options:
+        - Linux
+        - macOS
+        - Windows
+        - BSD
+      multiple: true
+    validations:
+      required: true
+
   - type: markdown
     attributes:
       value: >
@@ -60,4 +73,3 @@ body:
       description: "Please describe how the behavior you see differs from the expected behavior."
     validations:
       required: true
-
diff --git a/Makefile b/Makefile
index 9e1dc8207..0acf55a72 100644
--- a/Makefile
+++ b/Makefile
@@ -23,7 +23,6 @@ DISABLE_VERIFIC_EXTENSIONS := 0
 DISABLE_VERIFIC_VHDL := 0
 ENABLE_COVER := 1
 ENABLE_LIBYOSYS := 0
-ENABLE_PROTOBUF := 0
 ENABLE_ZLIB := 1
 
 # python wrappers
@@ -132,7 +131,7 @@ LDLIBS += -lrt
 endif
 endif
 
-YOSYS_VER := 0.22+4
+YOSYS_VER := 0.22+37
 
 # Note: We arrange for .gitcommit to contain the (short) commit hash in
 # tarballs generated with git-archive(1) using .gitattributes. The git repo
@@ -544,9 +543,6 @@ LDLIBS += $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -lz
 endif
 endif
 
-ifeq ($(ENABLE_PROTOBUF),1)
-LDLIBS += $(shell pkg-config --cflags --libs protobuf)
-endif
 
 ifeq ($(ENABLE_COVER),1)
 CXXFLAGS += -DYOSYS_ENABLE_COVER
diff --git a/backends/protobuf/.gitignore b/backends/protobuf/.gitignore
deleted file mode 100644
index 849b38d45..000000000
--- a/backends/protobuf/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-yosys.pb.cc
-yosys.pb.h
diff --git a/backends/protobuf/Makefile.inc b/backends/protobuf/Makefile.inc
deleted file mode 100644
index 9cac9dcaa..000000000
--- a/backends/protobuf/Makefile.inc
+++ /dev/null
@@ -1,10 +0,0 @@
-ifeq ($(ENABLE_PROTOBUF),1)
-
-backends/protobuf/yosys.pb.cc backends/protobuf/yosys.pb.h: misc/yosys.proto
-	$(Q) cd misc && protoc --cpp_out "../backends/protobuf" yosys.proto
-
-backends/protobuf/protobuf.cc: backends/protobuf/yosys.pb.h
-
-OBJS += backends/protobuf/protobuf.o backends/protobuf/yosys.pb.o
-
-endif
diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
deleted file mode 100644
index 384ce2e8e..000000000
--- a/backends/protobuf/protobuf.cc
+++ /dev/null
@@ -1,371 +0,0 @@
-/*
- *  yosys -- Yosys Open SYnthesis Suite
- *
- *  Copyright (C) 2012  Claire Xenia Wolf <claire@yosyshq.com>
- *  Copyright (C) 2018  Serge Bazanski <q3k@symbioticeda.com>
- *
- *  Permission to use, copy, modify, and/or distribute this software for any
- *  purpose with or without fee is hereby granted, provided that the above
- *  copyright notice and this permission notice appear in all copies.
- *
- *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *
- */
-
-#include <google/protobuf/text_format.h>
-
-#include "kernel/rtlil.h"
-#include "kernel/register.h"
-#include "kernel/sigtools.h"
-#include "kernel/celltypes.h"
-#include "kernel/cellaigs.h"
-#include "kernel/log.h"
-#include "yosys.pb.h"
-
-USING_YOSYS_NAMESPACE
-PRIVATE_NAMESPACE_BEGIN
-
-struct ProtobufDesignSerializer
-{
-	bool aig_mode_;
-	bool use_selection_;
-	yosys::pb::Design *pb_;
-
-	Design *design_;
-	Module *module_;
-
-	SigMap sigmap_;
-	int sigidcounter_;
-	dict<SigBit, uint64_t> sigids_;
-	pool<Aig> aig_models_;
-
-
-	ProtobufDesignSerializer(bool use_selection, bool aig_mode) :
-			aig_mode_(aig_mode), use_selection_(use_selection) { }
-
-	string get_name(IdString name)
-	{
-		return RTLIL::unescape_id(name);
-	}
-
-
-	void serialize_parameters(google::protobuf::Map<std::string, yosys::pb::Parameter> *out,
-		const dict<IdString, Const> &parameters)
-	{
-		for (auto &param : parameters) {
-			std::string key = get_name(param.first);
-
-
-			yosys::pb::Parameter pb_param;
-
-			if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0) {
-				pb_param.set_str(param.second.decode_string());
-			} else if (GetSize(param.second.bits) > 64) {
-				pb_param.set_str(param.second.as_string());
-			} else {
-				pb_param.set_int_(param.second.as_int());
-			}
-
-			(*out)[key] = pb_param;
-		}
-	}
-
-	void get_bits(yosys::pb::BitVector *out, SigSpec sig)
-	{
-		for (auto bit : sigmap_(sig)) {
-			auto sig = out->add_signal();
-
-			// Constant driver.
-			if (bit.wire == nullptr) {
-				if (bit == State::S0) sig->set_constant(sig->CONSTANT_DRIVER_LOW);
-				else if (bit == State::S1) sig->set_constant(sig->CONSTANT_DRIVER_HIGH);
-				else if (bit == State::Sz) sig->set_constant(sig->CONSTANT_DRIVER_Z);
-				else sig->set_constant(sig->CONSTANT_DRIVER_X);
-				continue;
-			}
-
-			// Signal - give it a unique identifier.
-			if (sigids_.count(bit) == 0) {
-				sigids_[bit] = sigidcounter_++;
-			}
-			sig->set_id(sigids_[bit]);
-		}
-	}
-
-	void serialize_module(yosys::pb::Module* out, Module *module)
-	{
-		module_ = module;
-		log_assert(module_->design == design_);
-		sigmap_.set(module_);
-		sigids_.clear();
-		sigidcounter_ = 0;
-
-		serialize_parameters(out->mutable_attribute(), module_->attributes);
-
-		for (auto n : module_->ports) {
-			Wire *w = module->wire(n);
-			if (use_selection_ && !module_->selected(w))
-				continue;
-
-			yosys::pb::Module::Port pb_port;
-			pb_port.set_direction(w->port_input ? w->port_output ?
-				yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT : yosys::pb::DIRECTION_OUTPUT);
-			get_bits(pb_port.mutable_bits(), w);
-			(*out->mutable_port())[get_name(n)] = pb_port;
-		}
-
-		for (auto c : module_->cells()) {
-			if (use_selection_ && !module_->selected(c))
-				continue;
-
-			yosys::pb::Module::Cell pb_cell;
-			pb_cell.set_hide_name(c->name[0] == '$');
-			pb_cell.set_type(get_name(c->type));
-
-			if (aig_mode_) {
-				Aig aig(c);
-				if (aig.name.empty())
-					continue;
-				pb_cell.set_model(aig.name);
-				aig_models_.insert(aig);
-			}
-			serialize_parameters(pb_cell.mutable_parameter(), c->parameters);
-			serialize_parameters(pb_cell.mutable_attribute(), c->attributes);
-
-			if (c->known()) {
-				for (auto &conn : c->connections()) {
-					yosys::pb::Direction direction = yosys::pb::DIRECTION_OUTPUT;
-					if (c->input(conn.first))
-						direction = c->output(conn.first) ? yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT;
-					(*pb_cell.mutable_port_direction())[get_name(conn.first)] = direction;
-				}
-			}
-			for (auto &conn : c->connections()) {
-				yosys::pb::BitVector vec;
-				get_bits(&vec, conn.second);
-				(*pb_cell.mutable_connection())[get_name(conn.first)] = vec;
-			}
-
-			(*out->mutable_cell())[get_name(c->name)] = pb_cell;
-		}
-
-		for (auto w : module_->wires()) {
-			if (use_selection_ && !module_->selected(w))
-				continue;
-
-			auto netname = out->add_netname();
-			netname->set_hide_name(w->name[0] == '$');
-			get_bits(netname->mutable_bits(), w);
-			serialize_parameters(netname->mutable_attributes(), w->attributes);
-		}
-	}
-
-
-	void serialize_models(google::protobuf::Map<string, yosys::pb::Model> *models)
-	{
-		for (auto &aig : aig_models_) {
-			yosys::pb::Model pb_model;
-			for (auto &node : aig.nodes) {
-				auto pb_node = pb_model.add_node();
-				if (node.portbit >= 0) {
-					if (node.inverter) {
-						pb_node->set_type(pb_node->TYPE_NPORT);
-					} else {
-						pb_node->set_type(pb_node->TYPE_PORT);
-					}
-					auto port = pb_node->mutable_port();
-					port->set_portname(log_id(node.portname));
-					port->set_bitindex(node.portbit);
-				} else if (node.left_parent < 0 && node.right_parent < 0) {
-					if (node.inverter) {
-						pb_node->set_type(pb_node->TYPE_TRUE);
-					} else {
-						pb_node->set_type(pb_node->TYPE_FALSE);
-					}
-				} else {
-					if (node.inverter) {
-						pb_node->set_type(pb_node->TYPE_NAND);
-					} else {
-						pb_node->set_type(pb_node->TYPE_AND);
-					}
-					auto gate = pb_node->mutable_gate();
-					gate->set_left(node.left_parent);
-					gate->set_right(node.right_parent);
-				}
-				for (auto &op : node.outports) {
-					auto pb_op = pb_node->add_out_port();
-					pb_op->set_name(log_id(op.first));
-					pb_op->set_bit_index(op.second);
-				}
-			}
-			(*models)[aig.name] = pb_model;
-		}
-	}
-
-	void serialize_design(yosys::pb::Design *pb, Design *design)
-	{
-		GOOGLE_PROTOBUF_VERIFY_VERSION;
-		pb_ = pb;
-		pb_->Clear();
-		pb_->set_creator(yosys_version_str);
-
-		design_ = design;
-		design_->sort();
-
-		auto modules = use_selection_ ? design_->selected_modules() : design_->modules();
-		for (auto mod : modules) {
-			yosys::pb::Module pb_mod;
-			serialize_module(&pb_mod, mod);
-			(*pb->mutable_modules())[mod->name.str()] = pb_mod;
-		}
-
-		serialize_models(pb_->mutable_models());
-	}
-};
-
-struct ProtobufBackend : public Backend {
-	ProtobufBackend(): Backend("protobuf", "write design to a Protocol Buffer file") { }
-	void help() override
-	{
-		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
-		log("\n");
-		log("    write_protobuf [options] [filename]\n");
-		log("\n");
-		log("Write a JSON netlist of the current design.\n");
-		log("\n");
-		log("    -aig\n");
-		log("        include AIG models for the different gate types\n");
-		log("\n");
-		log("    -text\n");
-		log("        output protobuf in Text/ASCII representation\n");
-		log("\n");
-		log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n");
-		log("Yosys source code distribution.\n");
-		log("\n");
-	}
-	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
-	{
-		bool aig_mode = false;
-		bool text_mode = false;
-
-		size_t argidx;
-		for (argidx = 1; argidx < args.size(); argidx++) {
-			if (args[argidx] == "-aig") {
-				aig_mode = true;
-				continue;
-			}
-			if (args[argidx] == "-text") {
-				text_mode = true;
-				continue;
-			}
-			break;
-		}
-		extra_args(f, filename, args, argidx, !text_mode);
-
-		log_header(design, "Executing Protobuf backend.\n");
-
-		yosys::pb::Design pb;
-		ProtobufDesignSerializer serializer(false, aig_mode);
-		serializer.serialize_design(&pb, design);
-
-		if (text_mode) {
-			string out;
-			google::protobuf::TextFormat::PrintToString(pb, &out);
-			*f << out;
-		} else {
-			pb.SerializeToOstream(f);
-		}
-	}
-} ProtobufBackend;
-
-struct ProtobufPass : public Pass {
-	ProtobufPass() : Pass("protobuf", "write design in Protobuf format") { }
-	void help() override
-	{
-		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
-		log("\n");
-		log("    protobuf [options] [selection]\n");
-		log("\n");
-		log("Write a JSON netlist of all selected objects.\n");
-		log("\n");
-		log("    -o <filename>\n");
-		log("        write to the specified file.\n");
-		log("\n");
-		log("    -aig\n");
-		log("        include AIG models for the different gate types\n");
-		log("\n");
-		log("    -text\n");
-		log("        output protobuf in Text/ASCII representation\n");
-		log("\n");
-		log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n");
-		log("Yosys source code distribution.\n");
-		log("\n");
-	}
-	void execute(std::vector<std::string> args, RTLIL::Design *design) override
-	{
-		std::string filename;
-		bool aig_mode = false;
-		bool text_mode = false;
-
-		size_t argidx;
-		for (argidx = 1; argidx < args.size(); argidx++)
-		{
-			if (args[argidx] == "-o" && argidx+1 < args.size()) {
-				filename = args[++argidx];
-				continue;
-			}
-			if (args[argidx] == "-aig") {
-				aig_mode = true;
-				continue;
-			}
-			if (args[argidx] == "-text") {
-				text_mode = true;
-				continue;
-			}
-			break;
-		}
-		extra_args(args, argidx, design);
-
-		std::ostream *f;
-		std::stringstream buf;
-
-		if (!filename.empty()) {
-			rewrite_filename(filename);
-			std::ofstream *ff = new std::ofstream;
-			ff->open(filename.c_str(), text_mode ? std::ofstream::trunc : (std::ofstream::trunc | std::ofstream::binary));
-			if (ff->fail()) {
-				delete ff;
-				log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
-			}
-			f = ff;
-		} else {
-			f = &buf;
-		}
-
-		yosys::pb::Design pb;
-		ProtobufDesignSerializer serializer(true, aig_mode);
-		serializer.serialize_design(&pb, design);
-
-		if (text_mode) {
-			string out;
-			google::protobuf::TextFormat::PrintToString(pb, &out);
-			*f << out;
-		} else {
-			pb.SerializeToOstream(f);
-		}
-
-		if (!filename.empty()) {
-			delete f;
-		} else {
-			log("%s", buf.str().c_str());
-		}
-	}
-} ProtobufPass;
-
-PRIVATE_NAMESPACE_END;
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 54783cf1b..7434b13da 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -559,6 +559,9 @@ struct Smt2Worker
 		if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_)))
 		{
 			registers.insert(cell);
+			SigBit q_bit = cell->getPort(ID::Q);
+			if (q_bit.is_wire())
+				decls.push_back(witness_signal("reg", 1, 0, "", idcounter, q_bit.wire));
 			makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q)));
 			register_bool(cell->getPort(ID::Q), idcounter++);
 			recursive_cells.erase(cell);
@@ -589,9 +592,12 @@ struct Smt2Worker
 			if (cell->type.in(ID($ff), ID($dff)))
 			{
 				registers.insert(cell);
-				for (auto chunk : cell->getPort(ID::Q).chunks())
+				int smtoffset = 0;
+				for (auto chunk : cell->getPort(ID::Q).chunks()) {
 					if (chunk.is_wire())
-						decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire));
+						decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset));
+					smtoffset += chunk.width;
+				}
 				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q)));
 				register_bv(cell->getPort(ID::Q), idcounter++);
 				recursive_cells.erase(cell);
@@ -1490,7 +1496,7 @@ struct Smt2Worker
 		return path;
 	}
 
-	std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire)
+	std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire, int smtoffset = 0)
 	{
 		std::vector<std::string> hiername;
 		const char *wire_name = wire->name.c_str();
@@ -1508,6 +1514,7 @@ struct Smt2Worker
 			{ "offset", offset },
 			{ "width", width },
 			{ "smtname", smtname.empty() ? json11::Json(smtid) : json11::Json(smtname) },
+			{ "smtoffset", smtoffset },
 			{ "path", witness_path(wire) },
 		}}).dump(line);
 		line += "\n";
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index cc108d52b..4c1f07229 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -676,7 +676,7 @@ if inywfile is not None:
                         if common_end <= common_offset:
                             continue
 
-                        smt_expr = smt.net_expr(topmod, f"s{t}", wire["smtpath"])
+                        smt_expr = smt.witness_net_expr(topmod, f"s{t}", wire)
 
                         if not smt_bool:
                             slice_high = common_end - offset - 1
@@ -1298,7 +1298,8 @@ def write_yw_trace(steps_start, steps_stop, index, allregs=False):
                 sigs = seqs
 
             for sig in sigs:
-                step_values[sig["sig"]] = smt.bv2bin(smt.get(smt.net_expr(topmod, f"s{k}", sig["smtpath"])))
+                value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig)))
+                step_values[sig["sig"]] = value
             yw.step(step_values)
 
         yw.end_trace()
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 5cd1a74fb..d445847dd 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -701,7 +701,7 @@ class SmtIo:
                 if witness["type"] == "mem":
                     if allregs and not witness["rom"]:
                         width, size = witness["width"], witness["size"]
-                        witness = {**witness, "uninitialized": {"width": width * size, "offset": 0}}
+                        witness = {**witness, "uninitialized": [{"width": width * size, "offset": 0}]}
                     if not witness["uninitialized"]:
                         continue
 
@@ -958,6 +958,15 @@ class SmtIo:
         nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
         return self.net_expr(nextmod, nextbase, path[1:])
 
+    def witness_net_expr(self, mod, base, witness):
+        net = self.net_expr(mod, base, witness["smtpath"])
+        is_bool = self.net_width(mod, witness["smtpath"]) == 1
+        if is_bool:
+            assert witness["width"] == 1
+            assert witness["smtoffset"] == 0
+            return net
+        return "((_ extract %d %d) %s)" % (witness["smtoffset"] + witness["width"] - 1, witness["smtoffset"], net)
+
     def net_width(self, mod, net_path):
         for i in range(len(net_path)-1):
             assert mod in self.modinfo
diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc
index 73d1f0ea7..ebbe082a2 100644
--- a/frontends/blif/blifparse.cc
+++ b/frontends/blif/blifparse.cc
@@ -21,6 +21,8 @@
 
 YOSYS_NAMESPACE_BEGIN
 
+const int lut_input_plane_limit = 12;
+
 static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count, std::istream &f)
 {
 	string strbuf;
@@ -513,6 +515,11 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool
 					sopmode = -1;
 					lastcell = sopcell;
 				}
+				else if (input_sig.size() > lut_input_plane_limit)
+				{
+					err_reason = stringf("names' input plane must have fewer than %d signals.", lut_input_plane_limit + 1);
+					goto error_with_reason;
+				}
 				else
 				{
 					RTLIL::Cell *cell = module->addCell(NEW_ID, ID($lut));
@@ -576,7 +583,7 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool
 
 		if (lutptr)
 		{
-			if (input_len > 12)
+			if (input_len > lut_input_plane_limit)
 				goto error;
 
 			for (int i = 0; i < (1 << input_len); i++) {
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 820ac042c..71b87755d 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -2533,6 +2533,10 @@ struct VerificPass : public Pass {
 		log("  -fullinit\n");
 		log("    Keep all register initializations, even those for non-FF registers.\n");
 		log("\n");
+		log("  -cells\n");
+		log("    Import all cell definitions from Verific loaded libraries even if they are\n");
+		log("    unused in design. Useful with \"-edif\" option.\n");
+		log("\n");
 		log("  -chparam name value \n");
 		log("    Elaborate the specified top modules (all modules when -all given) using\n");
 		log("    this parameter value. Modules on which this parameter does not exist will\n");
@@ -2791,6 +2795,20 @@ struct VerificPass : public Pass {
 		}
 
 		veri_file::RemoveAllLOptions();
+		veri_file::AddLOption("work");
+		for (int i = argidx; i < GetSize(args); i++)
+		{
+			if (args[i] == "-work" && i+1 < GetSize(args)) {
+				++i;
+				continue;
+			}
+			if (args[i] == "-L" && i+1 < GetSize(args)) {
+				if (args[++i] == "work")
+					veri_file::RemoveAllLOptions();
+				continue;
+			}
+			break;
+		}
 		for (; argidx < GetSize(args); argidx++)
 		{
 			if (args[argidx] == "-work" && argidx+1 < GetSize(args)) {
@@ -3038,7 +3056,7 @@ struct VerificPass : public Pass {
 			bool mode_all = false, mode_gates = false, mode_keep = false;
 			bool mode_nosva = false, mode_names = false, mode_verific = false;
 			bool mode_autocover = false, mode_fullinit = false;
-			bool flatten = false, extnets = false;
+			bool flatten = false, extnets = false, mode_cells = false;
 			string dumpfile;
 			string ppfile;
 			Map parameters(STRING_HASH);
@@ -3084,6 +3102,10 @@ struct VerificPass : public Pass {
 					mode_fullinit = true;
 					continue;
 				}
+				if (args[argidx] == "-cells") {
+					mode_cells = true;
+					continue;
+				}
 				if (args[argidx] == "-chparam"  && argidx+2 < GetSize(args)) {
 					const std::string &key = args[++argidx];
 					const std::string &value = args[++argidx];
@@ -3204,6 +3226,28 @@ struct VerificPass : public Pass {
 				}
 				delete netlists;
 			}
+			if (mode_cells) {
+				log("Importing all cells.\n");
+				Libset *gls = Libset::Global() ;
+				MapIter it ;
+				Library *l ;
+				FOREACH_LIBRARY_OF_LIBSET(gls,it,l) {
+					MapIter mi ;
+					Verific::Cell *c ;
+					FOREACH_CELL_OF_LIBRARY(l,mi,c) {
+						if (!mode_verific && (l == Library::Primitives() || l == Library::Operators())) continue;
+						MapIter ni ;
+						if (c->NumOfNetlists() == 1) {
+							c->GetFirstNetlist()->SetName("");
+						}
+						Netlist *nl;
+						FOREACH_NETLIST_OF_CELL(c, ni, nl) {
+							if (nl)
+								nl_todo.emplace(nl->CellBaseName(), nl);
+						}
+					}
+				}
+			}
 
 			if (!verific_error_msg.empty())
 				goto check_error;
diff --git a/kernel/log.h b/kernel/log.h
index 3bc9fd978..8ef6e6d0e 100644
--- a/kernel/log.h
+++ b/kernel/log.h
@@ -419,6 +419,18 @@ static inline void log_dump_val_worker(pool<K, OPS> &v) {
 	log(" }");
 }
 
+template<typename K>
+static inline void log_dump_val_worker(std::vector<K> &v) {
+	log("{");
+	bool first = true;
+	for (auto &it : v) {
+		log(first ? " " : ", ");
+		log_dump_val_worker(it);
+		first = false;
+	}
+	log(" }");
+}
+
 template<typename T>
 static inline void log_dump_val_worker(T *ptr) { log("%p", ptr); }
 
diff --git a/misc/yosys.proto b/misc/yosys.proto
deleted file mode 100644
index a583e6265..000000000
--- a/misc/yosys.proto
+++ /dev/null
@@ -1,175 +0,0 @@
-//
-// yosys -- Yosys Open SYnthesis Suite
-//
-// Copyright (C) 2018  Serge Bazanski <q3k@symbioticeda.com>
-//
-// Permission to use, copy, modify, and/or distribute this software for any
-// purpose with or without fee is hereby granted, provided that the above
-// copyright notice and this permission notice appear in all copies.
-//
-// THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
-// WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
-// MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
-// ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
-// WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
-// ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
-// OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
-//
-
-/// Protobuf definition of Yosys RTLIL dump/restore format for RTL designs.
-
-syntax = "proto3";
-
-package yosys.pb;
-
-// Port direction.
-enum Direction {
-    DIRECTION_INVALID = 0;
-    DIRECTION_INPUT = 1;
-    DIRECTION_OUTPUT = 2;
-    DIRECTION_INOUT = 3;
-}
-
-// A freeform parameter/attribute value.
-message Parameter {
-    oneof value {
-        int64 int = 1;
-        string str = 2;
-    }
-}
-
-// A signal in the design - either a unique identifier for one, or a constant
-// driver (low or high).
-message Signal {
-    // A constant signal driver in the design.
-    enum ConstantDriver {
-        CONSTANT_DRIVER_INVALID = 0;
-        CONSTANT_DRIVER_LOW = 1;
-        CONSTANT_DRIVER_HIGH = 2;
-        CONSTANT_DRIVER_Z = 3;
-        CONSTANT_DRIVER_X = 4;
-    }
-    oneof type {
-        // Signal uniquely identified by ID number.
-        int64 id = 1;
-        // Constant driver.
-        ConstantDriver constant = 2;
-    }
-}
-
-// A vector of signals.
-message BitVector {
-    repeated Signal signal = 1;
-}
-
-// A netlist module.
-message Module {
-    // Freeform attributes.
-    map<string, Parameter> attribute = 1;
-
-    // Named ports in this module.
-    message Port {
-        Direction direction = 1;
-        BitVector bits = 2;
-    }
-    map<string, Port> port = 2;
-
-    // Named cells in this module.
-    message Cell {
-        // Set to true when the name of this cell is automatically created and
-        // likely not of interest for a regular user.
-        bool hide_name = 1;
-        string type = 2;
-        // Set if this module has an AIG model available.
-        string model = 3;
-        // Freeform parameters.
-        map<string, Parameter> parameter = 4;
-        // Freeform attributes.
-        map<string, Parameter> attribute = 5;
-
-        /// Ports of the cell.
-        // Direction of the port, if interface is known.
-        map<string, Direction> port_direction = 6;
-        // Connection of named port to signal(s).
-        map<string, BitVector> connection = 7;
-    }
-    map<string, Cell> cell = 3;
-
-    // Nets in this module.
-    message Netname {
-        // Set to true when the name of this net is automatically created and
-        // likely not of interest for a regular user.
-        bool hide_name = 1;
-        // Signal(s) that make up this net.
-        BitVector bits = 2;
-        // Freeform attributes.
-        map<string, Parameter> attributes = 3;
-    }
-    repeated Netname netname = 4;
-}
-
-// And-Inverter-Graph model.
-message Model {
-    message Node {
-        // Type of AIG node - or, what its' value is.
-        enum Type {
-            TYPE_INVALID = 0;
-            // The node's value is the value of the specified input port bit.
-            TYPE_PORT = 1;
-            // The node's value is the inverted value of the specified input
-            // port bit.
-            TYPE_NPORT = 2;
-            // The node's value is the ANDed value of specified nodes.
-            TYPE_AND = 3;
-            // The node's value is the NANDed value of specified nodes.
-            TYPE_NAND = 4;
-            // The node's value is a constant 1.
-            TYPE_TRUE = 5;
-            // The node's value is a constant 0.
-            TYPE_FALSE = 6;
-        };
-        Type type = 1;
-
-        message Port {
-            // Name of port.
-            string portname = 1;
-            // Bit index in port.
-            int64 bitindex = 2;
-        }
-        message Gate {
-            // Node index of left side of operation.
-            int64 left = 1;
-            // Node index of right side of operation.
-            int64 right = 2;
-        }
-        oneof node {
-            // Set for PORT, NPORT
-            Port port = 2;
-            // Set for AND, NAND.
-            Gate gate = 3;
-        }
-
-        // Set when the node drives given output port(s).
-        message OutPort {
-            // Name of port.
-            string name = 1;
-            // Bit index in port.
-            int64 bit_index = 2;
-        }
-        repeated OutPort out_port = 4;
-    }
-
-    // List of  AIG nodes - each is explicitely numbered by its' index in this
-    // array.
-    repeated Node node = 1;
-}
-
-// A Yosys design netlist dumped from RTLIL.
-message Design {
-    // Human-readable freeform 'remark' string.
-    string creator = 1;
-    // List of named modules in design.
-    map<string, Module> modules = 2;
-    // List of named AIG models in design (if AIG export enabled).
-    map<string, Model> models = 3;
-}
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index 7ef2827bf..27cec7549 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -40,16 +40,6 @@ struct EquivMakeWorker
 	pool<SigBit> undriven_bits;
 	SigMap assign_map;
 
-	dict<SigBit, pool<Cell*>> bit2driven; // map: bit <--> and its driven cells
-
-	CellTypes comb_ct;
-
-	EquivMakeWorker()
-	{
-		comb_ct.setup_internals();
-		comb_ct.setup_stdcells();
-	}
-
 	void read_blacklists()
 	{
 		for (auto fn : blacklists)
@@ -147,6 +137,7 @@ struct EquivMakeWorker
 	{
 		SigMap assign_map(equiv_mod);
 		SigMap rd_signal_map;
+		SigPool primary_inputs;
 
 		// list of cells without added $equiv cells
 		auto cells_list = equiv_mod->cells().to_vector();
@@ -262,6 +253,9 @@ struct EquivMakeWorker
 				gate_wire->port_input = false;
 				equiv_mod->connect(gold_wire, wire);
 				equiv_mod->connect(gate_wire, wire);
+				primary_inputs.add(assign_map(gold_wire));
+				primary_inputs.add(assign_map(gate_wire));
+				primary_inputs.add(wire);
 			}
 			else
 			{
@@ -288,31 +282,19 @@ struct EquivMakeWorker
 			}
 		}
 
-		init_bit2driven();
-
-		pool<Cell*> visited_cells;
 		for (auto c : cells_list)
 		for (auto &conn : c->connections())
 			if (!ct.cell_output(c->type, conn.first)) {
 				SigSpec old_sig = assign_map(conn.second);
 				SigSpec new_sig = rd_signal_map(old_sig);
-
-				if(old_sig != new_sig) {
-					SigSpec tmp_sig = old_sig;
-					for (int i = 0; i < GetSize(old_sig); i++) {
-						SigBit old_bit = old_sig[i], new_bit = new_sig[i];
-
-						visited_cells.clear();
-						if (check_signal_in_fanout(visited_cells, old_bit, new_bit))
-							continue;
-
-						log("Changing input %s of cell %s (%s): %s -> %s\n",
-								log_id(conn.first), log_id(c), log_id(c->type),
-								log_signal(old_bit), log_signal(new_bit));
-
-						tmp_sig[i] = new_bit;
-					}
-					c->setPort(conn.first, tmp_sig);
+				for (int i = 0; i < GetSize(old_sig); i++)
+					if (primary_inputs.check(old_sig[i]))
+						new_sig[i] = old_sig[i];
+				if (old_sig != new_sig) {
+					log("Changing input %s of cell %s (%s): %s -> %s\n",
+							log_id(conn.first), log_id(c), log_id(c->type),
+							log_signal(old_sig), log_signal(new_sig));
+					c->setPort(conn.first, new_sig);
 				}
 			}
 
@@ -403,57 +385,6 @@ struct EquivMakeWorker
 		}
 	}
 
-	void init_bit2driven()
-	{
-		for (auto cell : equiv_mod->cells()) {
-			if (!ct.cell_known(cell->type) && !cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_), ID($ff), ID($_FF_)))
-				continue;
-			for (auto &conn : cell->connections())
-			{
-				if (yosys_celltypes.cell_input(cell->type, conn.first))
-					for (auto bit : assign_map(conn.second))
-					{
-						bit2driven[bit].insert(cell);
-					}
-			}
-		}
-	}
-
-	bool check_signal_in_fanout(pool<Cell*> & visited_cells, SigBit source_bit, SigBit target_bit)
-	{
-		if (source_bit == target_bit)
-			return true;
-
-		if (bit2driven.count(source_bit) == 0)
-			return false;
-
-		auto driven_cells = bit2driven.at(source_bit);
-		for (auto driven_cell: driven_cells)
-		{
-			bool is_comb = comb_ct.cell_known(driven_cell->type);
-			if (!is_comb)
-				continue;
-
-			if (visited_cells.count(driven_cell) > 0)
-				continue;
-			visited_cells.insert(driven_cell);
-
-			for (auto &conn: driven_cell->connections())
-			{
-				if (yosys_celltypes.cell_input(driven_cell->type, conn.first))
-					continue;
-
-				for (auto bit: conn.second) {
-					bool is_in_fanout = check_signal_in_fanout(visited_cells, bit, target_bit);
-					if (is_in_fanout == true)
-						return true;
-				}
-			}
-		}
-
-		return false;
-	}
-
 	void run()
 	{
 		copy_to_equiv();
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
index 4d0400448..f5eb75730 100644
--- a/passes/equiv/equiv_opt.cc
+++ b/passes/equiv/equiv_opt.cc
@@ -60,13 +60,16 @@ struct EquivOptPass:public ScriptPass
 		log("    -undef\n");
 		log("        enable modelling of undef states during equiv_induct.\n");
 		log("\n");
+		log("    -nocheck\n");
+		log("        disable running check before and after the command under test.\n");
+		log("\n");
 		log("The following commands are executed by this verification command:\n");
 		help_script();
 		log("\n");
 	}
 
 	std::string command, techmap_opts, make_opts;
-	bool assert, undef, multiclock, async2sync;
+	bool assert, undef, multiclock, async2sync, nocheck;
 
 	void clear_flags() override
 	{
@@ -77,6 +80,7 @@ struct EquivOptPass:public ScriptPass
 		undef = false;
 		multiclock = false;
 		async2sync = false;
+		nocheck = false;
 	}
 
 	void execute(std::vector < std::string > args, RTLIL::Design * design) override
@@ -110,6 +114,10 @@ struct EquivOptPass:public ScriptPass
 				undef = true;
 				continue;
 			}
+			if (args[argidx] == "-nocheck") {
+				nocheck = true;
+				continue;
+			}
 			if (args[argidx] == "-multiclock") {
 				multiclock = true;
 				continue;
@@ -153,10 +161,14 @@ struct EquivOptPass:public ScriptPass
 		if (check_label("run_pass")) {
 			run("hierarchy -auto-top");
 			run("design -save preopt");
+			if (!nocheck)
+				run("check -assert", "(unless -nocheck)");
 			if (help_mode)
 				run("[command]");
 			else
 				run(command);
+			if (!nocheck)
+				run("check -assert", "(unless -nocheck)");
 			run("design -stash postopt");
 		}
 
diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc
index 2384ffced..bba2cbbec 100644
--- a/passes/sat/clk2fflogic.cc
+++ b/passes/sat/clk2fflogic.cc
@@ -26,6 +26,11 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+struct SampledSig {
+	SigSpec sampled, current;
+	SigSpec &operator[](bool get_current) { return get_current ? current : sampled; }
+};
+
 struct Clk2fflogicPass : public Pass {
 	Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { }
 	void help() override
@@ -38,37 +43,65 @@ struct Clk2fflogicPass : public Pass {
 		log("implicit global clock. This is useful for formal verification of designs with\n");
 		log("multiple clocks.\n");
 		log("\n");
+		log("This pass assumes negative hold time for the async FF inputs. For example when\n");
+		log("a reset deasserts with the clock edge, then the FF output will still drive the\n");
+		log("reset value in the next cycle regardless of the data-in value at the time of\n");
+		log("the clock edge.\n");
+		log("\n");
 	}
-	SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, bool is_fine, IdString past_sig_id) {
-		if (!is_fine)
-			return wrap_async_control(module, sig, polarity, past_sig_id);
-		return wrap_async_control_gate(module, sig, polarity, past_sig_id);
+	// Active-high sampled and current value of a level-triggered control signal. Initial sampled values is low/non-asserted.
+	SampledSig sample_control(Module *module, SigSpec sig, bool polarity, bool is_fine) {
+		if (!polarity) {
+			if (is_fine)
+				sig = module->NotGate(NEW_ID, sig);
+			else
+				sig = module->Not(NEW_ID, sig);
+		}
+		std::string sig_str = log_signal(sig);
+		sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
+		Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
+		sampled_sig->attributes[ID::init] = RTLIL::Const(State::S0, GetSize(sig));
+		if (is_fine)
+			module->addFfGate(NEW_ID, sig, sampled_sig);
+		else
+			module->addFf(NEW_ID, sig, sampled_sig);
+		return {sampled_sig, sig};
 	}
-	SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) {
-		Wire *past_sig = module->addWire(past_sig_id, GetSize(sig));
-		past_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S0 : State::S1, GetSize(sig));
-		module->addFf(NEW_ID, sig, past_sig);
-		if (polarity)
-			sig = module->Or(NEW_ID, sig, past_sig);
+	// Active-high trigger signal for an edge-triggered control signal. Initial values is low/non-edge.
+	SigSpec sample_control_edge(Module *module, SigSpec sig, bool polarity, bool is_fine) {
+		std::string sig_str = log_signal(sig);
+		sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
+		Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
+		sampled_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S1 : State::S0, GetSize(sig));
+		if (is_fine)
+			module->addFfGate(NEW_ID, sig, sampled_sig);
 		else
-			sig = module->And(NEW_ID, sig, past_sig);
-		if (polarity)
-			return sig;
-		else
-			return module->Not(NEW_ID, sig);
+			module->addFf(NEW_ID, sig, sampled_sig);
+		return module->Eqx(NEW_ID, {sampled_sig, sig}, polarity ? SigSpec {State::S0, State::S1} : SigSpec {State::S1, State::S0});
 	}
-	SigSpec wrap_async_control_gate(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) {
-		Wire *past_sig = module->addWire(past_sig_id);
-		past_sig->attributes[ID::init] = polarity ? State::S0 : State::S1;
-		module->addFfGate(NEW_ID, sig, past_sig);
-		if (polarity)
-			sig = module->OrGate(NEW_ID, sig, past_sig);
+	// Sampled and current value of a data signal.
+	SampledSig sample_data(Module *module, SigSpec sig, RTLIL::Const init, bool is_fine) {
+		std::string sig_str = log_signal(sig);
+		sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
+		Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
+		sampled_sig->attributes[ID::init] = init;
+		if (is_fine)
+			module->addFfGate(NEW_ID, sig, sampled_sig);
 		else
-			sig = module->AndGate(NEW_ID, sig, past_sig);
-		if (polarity)
-			return sig;
+			module->addFf(NEW_ID, sig, sampled_sig);
+		return {sampled_sig, sig};
+	}
+	SigSpec mux(Module *module, SigSpec a, SigSpec b, SigSpec s, bool is_fine) {
+		if (is_fine)
+			return module->MuxGate(NEW_ID, a, b, s);
 		else
-			return module->NotGate(NEW_ID, sig);
+			return module->Mux(NEW_ID, a, b, s);
+	}
+	SigSpec bitwise_sr(Module *module, SigSpec a, SigSpec s, SigSpec r, bool is_fine) {
+		if (is_fine)
+			return module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r));
+		else
+			return module->And(NEW_ID, module->Or(NEW_ID, a, s), module->Not(NEW_ID, r));
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
@@ -177,96 +210,47 @@ struct Clk2fflogicPass : public Pass {
 
 					ff.remove();
 
-					// Strip spaces from signal name, since Yosys IDs can't contain spaces
-					// Spaces only occur when we have a signal that's a slice of a larger bus,
-					// e.g. "\myreg [5:0]", so removing spaces shouldn't result in loss of uniqueness
-					std::string sig_q_str = log_signal(ff.sig_q);
-					sig_q_str.erase(std::remove(sig_q_str.begin(), sig_q_str.end(), ' '), sig_q_str.end());
-
-					Wire *past_q = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_q_wire", sig_q_str.c_str())), ff.width);
-          
-					if (!ff.is_fine) {
-						module->addFf(NEW_ID, ff.sig_q, past_q);
-					} else {
-						module->addFfGate(NEW_ID, ff.sig_q, past_q);
-					}
-					if (!ff.val_init.is_fully_undef())
-						initvals.set_init(past_q, ff.val_init);
-
-					if (ff.has_clk) {
+					if (ff.has_clk)
 						ff.unmap_ce_srst();
 
-						Wire *past_clk = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_clk#%s", sig_q_str.c_str(), log_signal(ff.sig_clk))));
-						initvals.set_init(past_clk, ff.pol_clk ? State::S1 : State::S0);
+					auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine).sampled;
 
-						if (!ff.is_fine)
-							module->addFf(NEW_ID, ff.sig_clk, past_clk);
-						else
-							module->addFfGate(NEW_ID, ff.sig_clk, past_clk);
-
-						SigSpec clock_edge_pattern;
-
-						if (ff.pol_clk) {
-							clock_edge_pattern.append(State::S0);
-							clock_edge_pattern.append(State::S1);
-						} else {
-							clock_edge_pattern.append(State::S1);
-							clock_edge_pattern.append(State::S0);
-						}
-
-						SigSpec clock_edge = module->Eqx(NEW_ID, {ff.sig_clk, SigSpec(past_clk)}, clock_edge_pattern);
-
-						Wire *past_d = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_d_wire", sig_q_str.c_str())), ff.width);
-						if (!ff.is_fine)
-							module->addFf(NEW_ID, ff.sig_d, past_d);
-						else
-							module->addFfGate(NEW_ID, ff.sig_d, past_d);
-
-						if (!ff.val_init.is_fully_undef())
-							initvals.set_init(past_d, ff.val_init);
-
-						if (!ff.is_fine)
-							qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
-						else
-							qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge);
-					} else {
-						qval = past_q;
+					if (ff.has_clk) {
+						// The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs
+						auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine);
+						auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine);
+						next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine);
 					}
 
+					SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst;
 					// The check for a constant sig_aload is also done by opt_dff, but when using verific and running
 					// clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids
 					// generating a lot of extra logic.
-					if (ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1)) {
-						SigSpec sig_aload = wrap_async_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine, NEW_ID);
-
-						if (!ff.is_fine)
-							qval = module->Mux(NEW_ID, qval, ff.sig_ad, sig_aload);
-						else
-							qval = module->MuxGate(NEW_ID, qval, ff.sig_ad, sig_aload);
+					bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1);
+					if (has_nonconst_aload) {
+						sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine);
+						// The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs
+						sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine);
 					}
-
 					if (ff.has_sr) {
-						SigSpec setval = wrap_async_control(module, ff.sig_set, ff.pol_set, ff.is_fine, NEW_ID);
-						SigSpec clrval = wrap_async_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine, NEW_ID);
-						if (!ff.is_fine) {
-							clrval = module->Not(NEW_ID, clrval);
-							qval = module->Or(NEW_ID, qval, setval);
-							module->addAnd(NEW_ID, qval, clrval, ff.sig_q);
-						} else {
-							clrval = module->NotGate(NEW_ID, clrval);
-							qval = module->OrGate(NEW_ID, qval, setval);
-							module->addAndGate(NEW_ID, qval, clrval, ff.sig_q);
-						}
-					} else if (ff.has_arst) {
-						IdString id = NEW_ID_SUFFIX(stringf("%s#past_arst#%s", sig_q_str.c_str(), log_signal(ff.sig_arst)));
-						SigSpec arst = wrap_async_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine, id);
-						if (!ff.is_fine)
-							module->addMux(NEW_ID, qval, ff.val_arst, arst, ff.sig_q);
-						else
-							module->addMuxGate(NEW_ID, qval, ff.val_arst[0], arst, ff.sig_q);
-					} else {
-						module->connect(ff.sig_q, qval);
+						sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine);
+						sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine);
 					}
+					if (ff.has_arst)
+						sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine);
+
+					// First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous
+					// implementation, this approach correctly handles all the cases of multiple signals changing simultaneously.
+					for (int current = 0; current < 2; current++) {
+						if (has_nonconst_aload)
+							next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine);
+						if (ff.has_sr)
+							next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine);
+						if (ff.has_arst)
+							next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine);
+					}
+
+					module->connect(ff.sig_q, next_q);
 				}
 			}
 		}
diff --git a/tests/arch/ice40/bug1597.ys b/tests/arch/ice40/bug1597.ys
index b7983cfa4..c1509cabc 100644
--- a/tests/arch/ice40/bug1597.ys
+++ b/tests/arch/ice40/bug1597.ys
@@ -3,7 +3,7 @@ module top (
     input CLK, PIN_1, PIN_2, PIN_3, PIN_4, PIN_5,
         PIN_6, PIN_7, PIN_8, PIN_9, PIN_10, PIN_11, PIN_12, PIN_13, PIN_25,
     output USBPU, PIN_14, PIN_15, PIN_16, PIN_17, PIN_18,
-        PIN_19, PIN_20, PIN_21, PIN_22, PIN_23, PIN_24,
+        PIN_19,
 );
     assign USBPU = 0;
 
@@ -67,6 +67,7 @@ module SSCounter6o (input wire rst, clk, adv, jmp, input wire [5:0] in, output w
     SB_LUT4 #(.LUT_INIT(16'h8BB8)) l5 (lo[5], in[5], jmp, out[5], co[4]);
 endmodule
 EOT
+read_verilog -lib +/ice40/cells_sim.v
 hierarchy -top top
 flatten
-equiv_opt -multiclock -map +/ice40/cells_sim.v synth_ice40
+equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40
diff --git a/tests/arch/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys
index 71b68431e..e779ab207 100644
--- a/tests/arch/ice40/ice40_opt.ys
+++ b/tests/arch/ice40/ice40_opt.ys
@@ -21,6 +21,7 @@ module top(input CI, I0, output [1:0] CO, output O);
 endmodule
 EOT
 
+read_verilog -icells -lib +/ice40/abc9_model.v +/ice40/cells_sim.v
 equiv_opt -assert -map +/ice40/abc9_model.v -map +/ice40/cells_sim.v ice40_opt
 design -load postopt
 select -assert-count 1 t:*
diff --git a/tests/arch/intel_alm/counter.ys b/tests/arch/intel_alm/counter.ys
index 56c9cabb3..0a5b9356a 100644
--- a/tests/arch/intel_alm/counter.ys
+++ b/tests/arch/intel_alm/counter.ys
@@ -2,7 +2,7 @@ read_verilog ../common/counter.v
 hierarchy -top top
 proc
 flatten
-equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check
+equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 
@@ -17,7 +17,7 @@ read_verilog ../common/counter.v
 hierarchy -top top
 proc
 flatten
-equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check
+equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 
diff --git a/tests/arch/xilinx/abc9_dff.ys b/tests/arch/xilinx/abc9_dff.ys
index 0ba3901f7..79e5a322c 100644
--- a/tests/arch/xilinx/abc9_dff.ys
+++ b/tests/arch/xilinx/abc9_dff.ys
@@ -12,6 +12,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6]));
 FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7]));
 endmodule
 EOT
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 6 t:FD*
@@ -31,6 +32,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
 FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
 endmodule
 EOT
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 4 t:FD*
@@ -54,6 +56,7 @@ logger -expect warning "Whitebox '\$paramod\\FDRE\\INIT=.*1' with \(\* abc9_flop
 logger -expect warning "Whitebox '\$paramod\\FDRE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1
 logger -expect warning "Whitebox 'FDSE' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1
 logger -expect warning "Whitebox '\$paramod\\FDSE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 8 t:FD*
@@ -75,6 +78,7 @@ always @(posedge clk or posedge pre)
 endmodule
 EOT
 proc
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 1 t:FDCE
@@ -94,6 +98,7 @@ assign q = ~r;
 endmodule
 EOT
 proc
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 1 t:FDRE %co w:r %i
@@ -111,6 +116,7 @@ assign q2 = r;
 endmodule
 EOT
 proc
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 1 t:FDRE %co %a w:r %i
@@ -128,6 +134,7 @@ assign o = r1 | r2;
 endmodule
 EOT
 proc
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 
 
diff --git a/tests/arch/xilinx/opt_lut_ins.ys b/tests/arch/xilinx/opt_lut_ins.ys
index a01d02179..2328919a3 100644
--- a/tests/arch/xilinx/opt_lut_ins.ys
+++ b/tests/arch/xilinx/opt_lut_ins.ys
@@ -18,6 +18,7 @@ end
 
 EOF
 
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -map +/xilinx/cells_sim.v opt_lut_ins -tech xilinx
 
 design -load postopt
diff --git a/tests/arch/xilinx/xilinx_dffopt.ys b/tests/arch/xilinx/xilinx_dffopt.ys
index c09699411..9f0b27ced 100644
--- a/tests/arch/xilinx/xilinx_dffopt.ys
+++ b/tests/arch/xilinx/xilinx_dffopt.ys
@@ -5,7 +5,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;
 
@@ -52,7 +52,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;
 
@@ -100,7 +100,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;
 
@@ -137,7 +137,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;
 
@@ -183,7 +183,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;
 
@@ -232,7 +232,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;
 
diff --git a/tests/blif/bug3385.ys b/tests/blif/bug3385.ys
new file mode 100644
index 000000000..e1e45983d
--- /dev/null
+++ b/tests/blif/bug3385.ys
@@ -0,0 +1,9 @@
+logger -expect error "Syntax error in line 4: names' input plane must have fewer than 13 signals." 1
+read_blif <<EOF
+.model test
+.inputs w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 w16 w17 w18 w19 w20 w21 w22 w23 w24 w25 w26 w27 w28 w29 w30
+.outputs out
+.names w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 w16 w17 w18 w19 w20 w21 w22 w23 w24 w25 w26 w27 w28 w29 w30 out
+1101010001100110010001100111001 0
+.end
+EOF
diff --git a/tests/opt/opt_dff_en.ys b/tests/opt/opt_dff_en.ys
index 06ee6c63d..9538afcc2 100644
--- a/tests/opt/opt_dff_en.ys
+++ b/tests/opt/opt_dff_en.ys
@@ -6,7 +6,7 @@ module top(...);
 
 input CLK;
 input [1:0] D;
-output [15:0] Q;
+output [11:0] Q;
 input SRST;
 input ARST;
 input [1:0] CLR;
diff --git a/tests/opt/opt_dff_mux.ys b/tests/opt/opt_dff_mux.ys
index ed01bed59..f21f9e9b8 100644
--- a/tests/opt/opt_dff_mux.ys
+++ b/tests/opt/opt_dff_mux.ys
@@ -7,7 +7,7 @@ module top(...);
 input CLK;
 input NE, NS;
 input EN;
-output [23:0] Q;
+output [17:0] Q;
 input [23:0] D;
 input SRST;
 input ARST;
diff --git a/tests/opt/opt_dff_qd.ys b/tests/opt/opt_dff_qd.ys
index afc96c42f..7b0b4c224 100644
--- a/tests/opt/opt_dff_qd.ys
+++ b/tests/opt/opt_dff_qd.ys
@@ -7,7 +7,7 @@ module top(...);
 input CLK;
 input EN;
 (* init = 24'h555555 *)
-output [23:0] Q;
+output [19:0] Q;
 input SRST;
 input ARST;
 input [1:0] CLR;
diff --git a/tests/opt/opt_dff_sr.ys b/tests/opt/opt_dff_sr.ys
index 0961cb11e..1d3fd300e 100644
--- a/tests/opt/opt_dff_sr.ys
+++ b/tests/opt/opt_dff_sr.ys
@@ -22,10 +22,9 @@ EOT
 
 design -save orig
 
-# Equivalence check will fail for unmapped adlatch and dlatchsr due to negative hold hack.
-#equiv_opt -undef -assert -multiclock opt_dff
-#design -load postopt
-opt_dff
+equiv_opt -undef -assert -multiclock opt_dff
+design -load postopt
+
 select -assert-count 1 t:$dffsr
 select -assert-count 1 t:$dffsr r:WIDTH=2 %i
 select -assert-count 1 t:$dffsre
@@ -36,9 +35,9 @@ select -assert-none t:$sr
 
 design -load orig
 
-#equiv_opt -undef -assert -multiclock opt_dff -keepdc
-#design -load postopt
-opt_dff -keepdc
+equiv_opt -undef -assert -multiclock opt_dff -keepdc
+design -load postopt
+
 select -assert-count 1 t:$dffsr
 select -assert-count 1 t:$dffsr r:WIDTH=4 %i
 select -assert-count 1 t:$dffsre
@@ -51,9 +50,9 @@ select -assert-count 1 t:$sr r:WIDTH=4 %i
 design -load orig
 simplemap
 
-#equiv_opt -undef -assert -multiclock opt_dff
-#design -load postopt
-opt_dff
+equiv_opt -undef -assert -multiclock opt_dff
+design -load postopt
+
 select -assert-count 1 t:$_DFF_PP0_
 select -assert-count 1 t:$_DFF_PP1_
 select -assert-count 1 t:$_DFFE_PN0P_
@@ -65,9 +64,9 @@ select -assert-none t:$_DFF_PP0_ t:$_DFF_PP1_ t:$_DFFE_PN0P_ t:$_DFFE_PN1P_ t:$_
 design -load orig
 simplemap
 
-#equiv_opt -undef -assert -multiclock opt_dff -keepdc
-#design -load postopt
-opt_dff -keepdc
+equiv_opt -undef -assert -multiclock opt_dff -keepdc
+design -load postopt
+
 select -assert-count 1 t:$_DFF_PP0_
 select -assert-count 1 t:$_DFF_PP1_
 select -assert-count 2 t:$_DFFSR_PPP_
diff --git a/tests/opt/opt_expr_xor.ys b/tests/opt/opt_expr_xor.ys
index a879f3ec9..8874f2775 100644
--- a/tests/opt/opt_expr_xor.ys
+++ b/tests/opt/opt_expr_xor.ys
@@ -10,7 +10,7 @@ design -save read
 select -assert-count 2 t:$xor
 select -assert-count 2 t:$xnor
 
-equiv_opt opt_expr
+equiv_opt -assert opt_expr
 design -load postopt
 select -assert-none t:$xor
 select -assert-none t:$xnor
@@ -19,7 +19,7 @@ select -assert-count 2 t:$not
 
 design -load read
 simplemap
-equiv_opt opt_expr
+equiv_opt -assert opt_expr
 design -load postopt
 select -assert-none t:$_XOR_
 select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
@@ -34,7 +34,7 @@ $_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1]));
 endmodule
 EOT
 select -assert-count 2 t:$_XNOR_
-equiv_opt opt_expr
+equiv_opt -assert opt_expr
 design -load postopt
 select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
 select -assert-count 1 t:$_NOT_
@@ -49,7 +49,7 @@ assign y = a~^1'b0;
 assign z = a~^1'b1;
 endmodule
 EOT
-equiv_opt opt_expr
+equiv_opt -assert opt_expr
 
 
 # Single-bit $xor
diff --git a/tests/techmap/adff2dff.ys b/tests/techmap/adff2dff.ys
index 53f7d2f08..6d03d1963 100644
--- a/tests/techmap/adff2dff.ys
+++ b/tests/techmap/adff2dff.ys
@@ -16,4 +16,4 @@ EOT
 
 proc
 
-equiv_opt -async2sync techmap -map +/adff2dff.v
+#equiv_opt -assert -async2sync techmap -map +/adff2dff.v
diff --git a/tests/techmap/dff2ff.ys b/tests/techmap/dff2ff.ys
index 5adf14b07..6e7e6082b 100644
--- a/tests/techmap/dff2ff.ys
+++ b/tests/techmap/dff2ff.ys
@@ -13,4 +13,4 @@ EOT
 
 proc
 
-equiv_opt techmap -map +/dff2ff.v
+equiv_opt -assert techmap -map +/dff2ff.v
diff --git a/tests/techmap/dfflegalize_adlatch.ys b/tests/techmap/dfflegalize_adlatch.ys
index b242cc809..559363301 100644
--- a/tests/techmap/dfflegalize_adlatch.ys
+++ b/tests/techmap/dfflegalize_adlatch.ys
@@ -12,7 +12,7 @@ $_DLATCH_PN1_ ff1 (.E(E), .R(R), .D(D), .Q(Q[1]));
 $_DLATCH_NP1_ ff2 (.E(E), .R(R), .D(D), .Q(Q[2]));
 endmodule
 
-module top(input C, E, R, D, output [13:0] Q);
+module top(input C, E, R, D, output [5:0] Q);
 adlatch0 adlatch0_(.E(E), .R(R), .D(D), .Q(Q[2:0]));
 adlatch1 adlatch1_(.E(E), .R(R), .D(D), .Q(Q[5:3]));
 endmodule
diff --git a/tests/techmap/dfflegalize_adlatch_init.ys b/tests/techmap/dfflegalize_adlatch_init.ys
index a55082d1d..8e371c528 100644
--- a/tests/techmap/dfflegalize_adlatch_init.ys
+++ b/tests/techmap/dfflegalize_adlatch_init.ys
@@ -12,7 +12,7 @@ $_DLATCH_PN1_ ff1 (.E(E), .R(R), .D(D), .Q(Q[1]));
 $_DLATCH_NP1_ ff2 (.E(E), .R(R), .D(D), .Q(Q[2]));
 endmodule
 
-module top(input C, E, R, D, output [13:0] Q);
+module top(input C, E, R, D, output [5:0] Q);
 adlatch0 adlatch0_(.E(E), .R(R), .D(D), .Q(Q[2:0]));
 adlatch1 adlatch1_(.E(E), .R(R), .D(D), .Q(Q[5:3]));
 endmodule
diff --git a/tests/techmap/dfflegalize_aldff.ys b/tests/techmap/dfflegalize_aldff.ys
index 1ee9e3af6..5be3e9742 100644
--- a/tests/techmap/dfflegalize_aldff.ys
+++ b/tests/techmap/dfflegalize_aldff.ys
@@ -24,8 +24,8 @@ design -save orig
 flatten
 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ x
 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ x
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x
 
 
 # Convert everything to ALDFFs.
diff --git a/tests/techmap/dfflegalize_aldff_init.ys b/tests/techmap/dfflegalize_aldff_init.ys
index f4db8dd32..ffa7cbf16 100644
--- a/tests/techmap/dfflegalize_aldff_init.ys
+++ b/tests/techmap/dfflegalize_aldff_init.ys
@@ -26,10 +26,10 @@ equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 0
 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 1
 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 0
 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 1
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1
 
 
 # Convert everything to ALDFFs.
diff --git a/tests/techmap/dfflegalize_dffsr_init.ys b/tests/techmap/dfflegalize_dffsr_init.ys
index ce5a32f76..b6160bb87 100644
--- a/tests/techmap/dfflegalize_dffsr_init.ys
+++ b/tests/techmap/dfflegalize_dffsr_init.ys
@@ -41,18 +41,18 @@ EOT
 
 design -save orig
 flatten
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1
 
 
 # Convert everything to ADFFs.
diff --git a/tests/techmap/dfflegalize_dlatchsr_init.ys b/tests/techmap/dfflegalize_dlatchsr_init.ys
index b38a9eb3b..da4ca164e 100644
--- a/tests/techmap/dfflegalize_dlatchsr_init.ys
+++ b/tests/techmap/dfflegalize_dlatchsr_init.ys
@@ -14,7 +14,7 @@ $_DLATCHSR_PNP_ ff2 (.E(E), .R(R), .S(S), .D(D), .Q(Q[2]));
 $_DLATCHSR_NPP_ ff3 (.E(E), .R(R), .S(S), .D(D), .Q(Q[3]));
 endmodule
 
-module top(input C, E, R, S, D, output [17:0] Q);
+module top(input C, E, R, S, D, output [7:0] Q);
 dlatchsr0 dlatchsr0_(.E(E), .R(R), .S(S), .D(D), .Q(Q[3:0]));
 dlatchsr1 dlatchsr1_(.E(E), .R(R), .S(S), .D(D), .Q(Q[7:4]));
 endmodule
@@ -23,12 +23,12 @@ EOT
 
 design -save orig
 flatten
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1
 
 
 # Convert everything to ADLATCHs.
diff --git a/tests/techmap/dfflegalize_sr_init.ys b/tests/techmap/dfflegalize_sr_init.ys
index 9d724de29..7cb1c629d 100644
--- a/tests/techmap/dfflegalize_sr_init.ys
+++ b/tests/techmap/dfflegalize_sr_init.ys
@@ -21,18 +21,18 @@ EOT
 
 design -save orig
 flatten
-#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0
-#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0
+equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1
 
 
 # Convert everything to SRs.
diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys
index 04477eb14..b0a7d6b7e 100644
--- a/tests/techmap/dfflibmap.ys
+++ b/tests/techmap/dfflibmap.ys
@@ -17,9 +17,11 @@ EOT
 simplemap
 
 design -save orig
+read_liberty -lib dfflibmap.lib
+
+equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib
+equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib
 
-#equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib
-#equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib
 dfflibmap -prepare -liberty dfflibmap.lib
 equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib
 
diff --git a/tests/techmap/dffunmap.ys b/tests/techmap/dffunmap.ys
index b813078ee..247699f80 100644
--- a/tests/techmap/dffunmap.ys
+++ b/tests/techmap/dffunmap.ys
@@ -4,7 +4,7 @@ module top(...);
 
 input C, R, E, S;
 input [1:0] D;
-output [20:0] Q;
+output [17:0] Q;
 
 $dff #(.CLK_POLARITY(1'b0), .WIDTH(2)) ff0 (.CLK(C), .D(D), .Q(Q[1:0]));
 $dffe #(.CLK_POLARITY(1'b0), .EN_POLARITY(1'b0), .WIDTH(2)) ff1 (.CLK(C), .EN(E), .D(D), .Q(Q[3:2]));
diff --git a/tests/techmap/pmux2mux.ys b/tests/techmap/pmux2mux.ys
index 1714a6b87..1e08485ef 100644
--- a/tests/techmap/pmux2mux.ys
+++ b/tests/techmap/pmux2mux.ys
@@ -12,4 +12,4 @@ output [3:0] O;
 endmodule
 EOT
 
-equiv_opt techmap -map +/pmux2mux.v
+equiv_opt -assert techmap -map +/pmux2mux.v
diff --git a/tests/techmap/shiftx2mux.ys b/tests/techmap/shiftx2mux.ys
index f749e79b2..680681297 100644
--- a/tests/techmap/shiftx2mux.ys
+++ b/tests/techmap/shiftx2mux.ys
@@ -106,4 +106,4 @@ endmodule
 EOT
 opt
 wreduce
-equiv_opt techmap
+equiv_opt -assert techmap
diff --git a/tests/techmap/zinit.ys b/tests/techmap/zinit.ys
index bc07f40e6..562db0776 100644
--- a/tests/techmap/zinit.ys
+++ b/tests/techmap/zinit.ys
@@ -13,6 +13,8 @@ $_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5]));
 $_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6]));
 $_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7]));
 
+assign Q[8] = 0;
+
 $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9]));
 $adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11]));
 endmodule
@@ -44,6 +46,8 @@ $_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5]));
 $_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6]));
 $_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7]));
 
+assign Q[8] = 0;
+
 $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9]));
 $adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11]));
 endmodule
@@ -91,9 +95,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E),  .R(R), .Q(Q[23]));
 
 endmodule
 EOT
-#equiv_opt -assert -multiclock zinit
-#design -load postopt
-zinit
+equiv_opt -assert -multiclock zinit
+design -load postopt
 
 select -assert-count 48 t:$_NOT_
 select -assert-count 0 w:Q a:init %i
@@ -138,9 +141,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E),  .R(R), .Q(Q[23]));
 
 endmodule
 EOT
-#equiv_opt -assert -multiclock zinit
-#design -load postopt
-zinit
+equiv_opt -assert -multiclock zinit
+design -load postopt
 
 select -assert-count 0 t:$_NOT_
 select -assert-count 1 w:Q a:init=24'b0 %i
diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2
index 74e2f3fca..494e7cda0 100644
--- a/tests/various/smtlib2_module-expected.smt2
+++ b/tests/various/smtlib2_module-expected.smt2
@@ -4,14 +4,14 @@
 (declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
 (declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
 ; yosys-smt2-input a 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "type": "input", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "smtoffset": 0, "type": "input", "width": 8}
 (define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
 (declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
 ; yosys-smt2-input b 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "type": "input", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "smtoffset": 0, "type": "input", "width": 8}
 (define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
 ; yosys-smt2-output add 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "type": "blackbox", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "smtoffset": 0, "type": "blackbox", "width": 8}
 (define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
 (|a| (|smtlib2_n a| state))
 (|b| (|smtlib2_n b| state))
@@ -19,7 +19,7 @@
 (bvadd a b)
 ))
 ; yosys-smt2-output eq 1
-; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "type": "blackbox", "width": 1}
+; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "smtoffset": 0, "type": "blackbox", "width": 1}
 (define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
 (|a| (|smtlib2_n a| state))
 (|b| (|smtlib2_n b| state))
@@ -27,7 +27,7 @@
 (= a b)
 ))
 ; yosys-smt2-output sub 8
-; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "type": "blackbox", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "smtoffset": 0, "type": "blackbox", "width": 8}
 (define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
 (|a| (|smtlib2_n a| state))
 (|b| (|smtlib2_n b| state))
@@ -49,10 +49,10 @@
 (declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub
 (declare-fun |uut_h s| (|uut_s|) |smtlib2_s|)
 ; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26
-; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "type": "init", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "smtoffset": 0, "type": "init", "width": 8}
 (declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
 ; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
-; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "type": "init", "width": 8}
+; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "smtoffset": 0, "type": "init", "width": 8}
 (declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b
 (define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2
 (define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9