Merge branch 'YosysHQ:master' into master

2022-10-20 19:36:03 +02:00 · 2022-10-20 19:36:03 +02:00 · 6936394eed
parent 2ba435b6bc be1a12595a
commit 6936394eed
42 changed files with 326 additions and 847 deletions
--- 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
-
--- a/6
+++ b/6
@ -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
--- a/backends/protobuf/.gitignore
+++ b/backends/protobuf/.gitignore
@ -1,2 +0,0 @@
-yosys.pb.cc
-yosys.pb.h
--- a/backends/protobuf/Makefile.inc
+++ b/backends/protobuf/Makefile.inc
@ -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
--- a/backends/protobuf/protobuf.cc
+++ b/backends/protobuf/protobuf.cc
@ -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;
--- 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";
--- 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()
--- 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
--- 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++) {
--- 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;
--- 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); }

--- a/misc/yosys.proto
+++ b/misc/yosys.proto
@ -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;
-}
--- 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();
--- 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");
 		}

--- 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);
 				}
 			}
 		}
--- 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
--- 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:*
--- 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

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


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

--- a/tests/blif/bug3385.ys
+++ 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
--- 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;
--- 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;
--- 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;
--- 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_
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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.
--- 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.
--- 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.
--- 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.
--- 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.
--- 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

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