Merge branch 'YosysHQ:master' into master

2022-06-14 09:54:50 +12:00 · 2022-06-14 09:54:50 +12:00 · 756a890206
parent 5f1aa4ff8a 6b7efe12b7
commit 756a890206
30 changed files with 653 additions and 389 deletions
--- a/23
+++ b/23
@ -2,8 +2,25 @@
 List of major changes and improvements between releases
 =======================================================

-Yosys 0.17 .. Yosys 0.17-dev
+Yosys 0.18 .. Yosys 0.18-dev
 --------------------------
+
+Yosys 0.17 .. Yosys 0.18
+--------------------------
+ * Various
+    - Migrated most flows to use memory_libmap based memory inference
+
+ * New commands and options
+    - Added "memory_libmap" pass
+    - Added "memory_bmux2rom" pass - converts muxes to ROMs
+    - Added "memory_dff -no-rw-check"
+    - Added "opt_ffinv" pass - push inverters through FFs
+    - Added "proc_rom" pass - convert switches to ROMs
+    - Added "proc -norom" option - will omit the proc_rom pass
+    - Added option "-no-rw-check" to synth passes
+    - Added "synth_ice40 -spram" option for automatic inference of SB_SPRAM256KA
+    - Added options "-nobram" and "-nolutram" to synth_machxo2 pass
+
 * Formal Verification
    - Fixed the signedness of $past's return value to be the same as the
      argument's instead of always unsigned.
@ -17,6 +34,10 @@ Yosys 0.17 .. Yosys 0.17-dev
    - Fixed size and signedness computation of functions used in ternary
      expressions or case item expressions

+ * Verific support
+    - Proper file location for readmem commands
+    - Added "-vlog-libext" option to specify search extension for libraries
+
 Yosys 0.16 .. Yosys 0.17
 --------------------------
 * New commands and options
--- a/4
+++ b/4
@ -129,7 +129,7 @@ LDFLAGS += -rdynamic
 LDLIBS += -lrt
 endif

-YOSYS_VER := 0.17+67
+YOSYS_VER := 0.18+3

 # Note: We arrange for .gitcommit to contain the (short) commit hash in
 # tarballs generated with git-archive(1) using .gitattributes. The git repo
@ -145,7 +145,7 @@ endif
 OBJS = kernel/version_$(GIT_REV).o

 bumpversion:
-	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 6f9602b.. | wc -l`/;" Makefile
+	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 19ce3b4.. | wc -l`/;" Makefile

 # set 'ABCREV = default' to use abc/ as it is
 #
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@ -53,6 +53,8 @@ struct Smt2Worker
 	std::map<int, int> bvsizes;
 	dict<IdString, char*> ids;

+	bool is_smtlib2_module;
+
 	const char *get_id(IdString n)
 	{
 		if (ids.count(n) == 0) {
@ -112,9 +114,10 @@ struct Smt2Worker
 	}

 	Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, bool forallmode,
-			dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache) :
-			ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
-			verbose(verbose), statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width)
+		   dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache)
+	    : ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode), verbose(verbose),
+	      statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width),
+	      is_smtlib2_module(module->has_attribute(ID::smtlib2_module))
 	{
 		pool<SigBit> noclock;

@ -124,6 +127,9 @@ struct Smt2Worker
 		memories = Mem::get_all_memories(module);
 		for (auto &mem : memories)
 		{
+			if (is_smtlib2_module)
+				log_error("Memory %s.%s not allowed in module with smtlib2_module attribute", get_id(module), mem.memid.c_str());
+
 			mem.narrow();
 			mem_dict[mem.memid] = &mem;
 			for (auto &port : mem.wr_ports)
@ -893,10 +899,25 @@ struct Smt2Worker
 				log_id(cell->type), log_id(module), log_id(cell));
 	}

+	void verify_smtlib2_module()
+	{
+		if (!module->get_blackbox_attribute())
+			log_error("Module %s with smtlib2_module attribute must also have blackbox attribute.\n", log_id(module));
+		if (module->cells().size() > 0)
+			log_error("Module %s with smtlib2_module attribute must not have any cells inside it.\n", log_id(module));
+		for (auto wire : module->wires())
+			if (!wire->port_id)
+				log_error("Wire %s.%s must be input or output since module has smtlib2_module attribute.\n", log_id(module),
+					  log_id(wire));
+	}
+
 	void run()
 	{
 		if (verbose) log("=> export logic driving outputs\n");

+		if (is_smtlib2_module)
+			verify_smtlib2_module();
+
 		pool<SigBit> reg_bits;
 		for (auto cell : module->cells())
 			if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) {
@ -905,11 +926,25 @@ struct Smt2Worker
 					reg_bits.insert(bit);
 			}

+		std::string smtlib2_inputs;
+		std::vector<std::string> smtlib2_decls;
+		if (is_smtlib2_module) {
+			for (auto wire : module->wires()) {
+				if (!wire->port_input)
+					continue;
+				smtlib2_inputs += stringf("(|%s| (|%s_n %s| state))\n", get_id(wire), get_id(module), get_id(wire));
+			}
+		}
+
 		for (auto wire : module->wires()) {
 			bool is_register = false;
 			for (auto bit : SigSpec(wire))
 				if (reg_bits.count(bit))
 					is_register = true;
+			bool is_smtlib2_comb_expr = wire->has_attribute(ID::smtlib2_comb_expr);
+			if (is_smtlib2_comb_expr && !is_smtlib2_module)
+				log_error("smtlib2_comb_expr is only valid in a module with the smtlib2_module attribute: wire %s.%s", log_id(module),
+					  log_id(wire));
 			if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
 				RTLIL::SigSpec sig = sigmap(wire);
 				std::vector<std::string> comments;
@ -924,11 +959,22 @@ struct Smt2Worker
 				if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
 					comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
 							clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
+				std::string smtlib2_comb_expr;
+				if (is_smtlib2_comb_expr) {
+					smtlib2_comb_expr =
+					  "(let (\n" + smtlib2_inputs + ")\n" + wire->get_string_attribute(ID::smtlib2_comb_expr) + "\n)";
+					if (wire->port_input || !wire->port_output)
+						log_error("smtlib2_comb_expr is only valid on output: wire %s.%s", log_id(module), log_id(wire));
+					if (!bvmode && GetSize(sig) > 1)
+						log_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s",
+							  log_id(module), log_id(wire));
+				}
+				auto &out_decls = is_smtlib2_comb_expr ? smtlib2_decls : decls;
 				if (bvmode && GetSize(sig) > 1) {
-					std::string sig_bv = get_bv(sig);
+					std::string sig_bv = is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bv(sig);
 					if (!comments.empty())
-						decls.insert(decls.end(), comments.begin(), comments.end());
-					decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
+						out_decls.insert(out_decls.end(), comments.begin(), comments.end());
+					out_decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
 							get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str()));
 					if (wire->port_input)
 						ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
@ -936,19 +982,19 @@ struct Smt2Worker
 				} else {
 					std::vector<std::string> sig_bool;
 					for (int i = 0; i < GetSize(sig); i++) {
-						sig_bool.push_back(get_bool(sig[i]));
+						sig_bool.push_back(is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bool(sig[i]));
 					}
 					if (!comments.empty())
-						decls.insert(decls.end(), comments.begin(), comments.end());
+						out_decls.insert(out_decls.end(), comments.begin(), comments.end());
 					for (int i = 0; i < GetSize(sig); i++) {
 						if (GetSize(sig) > 1) {
-							decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
+							out_decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
 									get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str()));
 							if (wire->port_input)
 								ex_input_eq.push_back(stringf("  (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))",
 										get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
 						} else {
-							decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
+							out_decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
 									get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str()));
 							if (wire->port_input)
 								ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
@ -959,11 +1005,17 @@ struct Smt2Worker
 			}
 		}

+		decls.insert(decls.end(), smtlib2_decls.begin(), smtlib2_decls.end());
+
 		if (verbose) log("=> export logic associated with the initial state\n");

 		vector<string> init_list;
 		for (auto wire : module->wires())
 			if (wire->attributes.count(ID::init)) {
+				if (is_smtlib2_module)
+					log_error("init attribute not allowed on wires in module with smtlib2_module attribute: wire %s.%s",
+						  log_id(module), log_id(wire));
+
 				RTLIL::SigSpec sig = sigmap(wire);
 				Const val = wire->attributes.at(ID::init);
 				val.bits.resize(GetSize(sig), State::Sx);
@ -1687,7 +1739,10 @@ struct Smt2Backend : public Backend {

 		for (auto module : sorted_modules)
 		{
-			if (module->get_blackbox_attribute() || module->has_processes_warn())
+			if (module->get_blackbox_attribute() && !module->has_attribute(ID::smtlib2_module))
+				continue;
+
+			if (module->has_processes_warn())
 				continue;

 			log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@ -123,6 +123,7 @@ class SmtIo:
        self.forall = False
        self.timeout = 0
        self.produce_models = True
+        self.recheck = False
        self.smt2cache = [list()]
        self.smt2_options = dict()
        self.p = None
@ -176,7 +177,10 @@ class SmtIo:
            self.unroll = False

        if self.solver == "yices":
-            if self.noincr or self.forall:
+            if self.forall:
+                self.noincr = True
+
+            if self.noincr:
                self.popen_vargs = ['yices-smt2'] + self.solver_opts
            else:
                self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
@ -189,11 +193,12 @@ class SmtIo:
            if self.timeout != 0:
                self.popen_vargs.append('-T:%d' % self.timeout);

-        if self.solver == "cvc4":
+        if self.solver in ["cvc4", "cvc5"]:
+            self.recheck = True
            if self.noincr:
-                self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+                self.popen_vargs = [self.solver, '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
            else:
-                self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+                self.popen_vargs = [self.solver, '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
            if self.timeout != 0:
                self.popen_vargs.append('--tlimit=%d000' % self.timeout);

@ -404,6 +409,15 @@ class SmtIo:
            stmt = re.sub(r" *;.*", "", stmt)
            if stmt == "": return

+        recheck = None
+
+        if self.solver != "dummy":
+            if self.noincr:
+                # Don't close the solver yet, if we're just unrolling definitions
+                # required for a (get-...) statement
+                if self.p is not None and not stmt.startswith("(get-") and unroll:
+                    self.p_close()
+
        if unroll and self.unroll:
            stmt = self.unroll_buffer + stmt
            self.unroll_buffer = ""
@ -415,6 +429,9 @@ class SmtIo:

            s = self.parse(stmt)

+            if self.recheck and s and s[0].startswith("get-"):
+                recheck = self.unroll_idcnt
+
            if self.debug_print:
                print("-> %s" % s)

@ -440,6 +457,9 @@ class SmtIo:

            stmt = self.unparse(self.unroll_stmt(s))

+            if recheck is not None and recheck != self.unroll_idcnt:
+                self.check_sat(["sat"])
+
            if stmt == "(push 1)":
                self.unroll_stack.append((
                    copy(self.unroll_sorts),
@ -460,8 +480,6 @@ class SmtIo:

        if self.solver != "dummy":
            if self.noincr:
-                if self.p is not None and not stmt.startswith("(get-"):
-                    self.p_close()
                if stmt == "(push 1)":
                    self.smt2cache.append(list())
                elif stmt == "(pop 1)":
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@ -53,6 +53,9 @@ USING_YOSYS_NAMESPACE
 #include "VhdlUnits.h"
 #endif

+#include "VerificStream.h"
+#include "FileSystem.h"
+
 #ifdef YOSYSHQ_VERIFIC_EXTENSIONS
 #include "InitialAssertions.h"
 #endif
@ -83,7 +86,7 @@ bool verific_import_pending;
 string verific_error_msg;
 int verific_sva_fsm_limit;

-vector<string> verific_incdirs, verific_libdirs;
+vector<string> verific_incdirs, verific_libdirs, verific_libexts;

 void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
 {
@ -118,6 +121,34 @@ string get_full_netlist_name(Netlist *nl)
 	return nl->CellBaseName();
 }

+class YosysStreamCallBackHandler : public VerificStreamCallBackHandler
+{
+public:
+    YosysStreamCallBackHandler() : VerificStreamCallBackHandler() { }
+    virtual ~YosysStreamCallBackHandler() { }
+
+    virtual verific_stream *GetSysCallStream(const char *file_path)
+    {
+        if (!file_path) return nullptr;
+
+        linefile_type src_loc = GetFromLocation();
+
+        char *this_file_name = nullptr;
+        if (src_loc && !FileSystem::IsAbsolutePath(file_path)) {
+            const char *src_file_name = LineFile::GetFileName(src_loc);
+            char *dir_name = FileSystem::DirectoryPath(src_file_name);
+            if (dir_name) {
+                this_file_name = Strings::save(dir_name, "/", file_path);
+                Strings::free(dir_name);
+                file_path = this_file_name;
+            }
+        }
+        verific_stream *strm = new verific_ifstream(file_path);
+        Strings::free(this_file_name);
+        return strm;
+    }
+};
+
 // ==================================================================

 VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
@ -2292,6 +2323,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
 	LineFile::DeleteAllLineFiles();
 	verific_incdirs.clear();
 	verific_libdirs.clear();
+	verific_libexts.clear();
 	verific_import_pending = false;

 	if (!verific_error_msg.empty())
@ -2402,6 +2434,11 @@ struct VerificPass : public Pass {
 		log("find undefined modules.\n");
 		log("\n");
 		log("\n");
+		log("    verific -vlog-libext <extension>..\n");
+		log("\n");
+		log("Add Verilog library extensions, used when searching in library directories.\n");
+		log("\n");
+		log("\n");
 		log("    verific -vlog-define <macro>[=<value>]..\n");
 		log("\n");
 		log("Add Verilog defines.\n");
@ -2495,61 +2532,6 @@ struct VerificPass : public Pass {
 		log("\n");
 		log("  -vhdl\n");
 		log("    Save output for VHDL design units.\n");
-		log("\n");
-		log("\n");
-		log("    verific -app <application>..\n");
-		log("\n");
-		log("Execute YosysHQ formal application on loaded Verilog files.\n");
-		log("\n");
-		log("Application options:\n");
-		log("\n");
-		log("    -module <module>\n");
-		log("        Run formal application only on specified module.\n");
-		log("\n");
-		log("    -blacklist <filename[:lineno]>\n");
-		log("        Do not run application on modules from files that match the filename\n");
-		log("        or filename and line number if provided in such format.\n");
-		log("        Parameter can also contain comma separated list of file locations.\n");
-		log("\n");
-		log("    -blfile <file>\n");
-		log("        Do not run application on locations specified in file, they can\n");
-		log("        represent filename or filename and location in file.\n");
-		log("\n");
-		log("Applications:\n");
-		log("\n");
-#if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_FORMALAPPS)
-		VerificFormalApplications vfa;
-		log("%s\n",vfa.GetHelp().c_str());
-#else
-		log("  WARNING: Applications only available in commercial build.\n");
-
-#endif
-		log("\n");
-		log("\n");
-		log("    verific -template <name> <top_module>..\n");
-		log("\n");
-		log("Generate template for specified top module of loaded design.\n");
-		log("\n");
-		log("Template options:\n");
-		log("\n");
-		log("  -out\n");
-		log("    Specifies output file for generated template, by default output is stdout\n");
-		log("\n");
-		log("  -chparam name value \n");
-		log("    Generate template using this parameter value. Otherwise default parameter\n");
-		log("    values will be used for templat generate functionality. This option\n");
-		log("    can be specified multiple times to override multiple parameters.\n");
-		log("    String values must be passed in double quotes (\").\n");
-		log("\n");
-		log("Templates:\n");
-		log("\n");
-#if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_TEMPLATES)
-		VerificTemplateGenerator vfg;
-		log("%s\n",vfg.GetHelp().c_str());
-#else
-		log("  WARNING: Templates only available in commercial build.\n");
-		log("\n");
-#endif
 		log("\n");
 		log("\n");
 		log("    verific -cfg [<name> [<value>]]\n");
@ -2648,6 +2630,8 @@ struct VerificPass : public Pass {

 		int argidx = 1;
 		std::string work = "work";
+		YosysStreamCallBackHandler cb;
+		veri_file::RegisterCallBackVerificStream(&cb);

 		if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
 				args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
@ -2683,6 +2667,12 @@ struct VerificPass : public Pass {
 			goto check_error;
 		}

+		if (GetSize(args) > argidx && args[argidx] == "-vlog-libext") {
+			for (argidx++; argidx < GetSize(args); argidx++)
+				verific_libexts.push_back(args[argidx]);
+			goto check_error;
+		}
+
 		if (GetSize(args) > argidx && args[argidx] == "-vlog-define") {
 			for (argidx++; argidx < GetSize(args); argidx++) {
 				string name = args[argidx];
@ -2823,6 +2813,8 @@ struct VerificPass : public Pass {
 				veri_file::AddIncludeDir(dir.c_str());
 			for (auto &dir : verific_libdirs)
 				veri_file::AddYDir(dir.c_str());
+			for (auto &ext : verific_libexts)
+				veri_file::AddLibExt(ext.c_str());

 			while (argidx < GetSize(args))
 				file_names.Insert(args[argidx++].c_str());
@ -2874,101 +2866,6 @@ struct VerificPass : public Pass {
 		}
 #endif

-#ifdef YOSYSHQ_VERIFIC_FORMALAPPS
-		if (argidx < GetSize(args) && args[argidx] == "-app")
-		{
-			if (!(argidx+1 < GetSize(args)))
-				cmd_error(args, argidx, "No formal application specified.\n");
-
-			VerificFormalApplications vfa;
-			auto apps = vfa.GetApps();
-			std::string app = args[++argidx];
-			std::vector<std::string> blacklists;
-			if (apps.find(app) == apps.end())
-				log_cmd_error("Application '%s' does not exist.\n", app.c_str());
-
-			FormalApplication *application = apps[app];
-			application->setLogger([](std::string msg) { log("%s",msg.c_str()); } );
-			VeriModule *selected_module = nullptr;
-
-			for (argidx++; argidx < GetSize(args); argidx++) {
-				std::string error;
-				if (application->checkParams(args, argidx, error)) {
-					if (!error.empty())
-						cmd_error(args, argidx, error);
-					continue;
-				}
-
-				if (args[argidx] == "-module" && argidx < GetSize(args)) {
-					if (!(argidx+1 < GetSize(args)))
-						cmd_error(args, argidx+1, "No module name specified.\n");
-					std::string module = args[++argidx];
-					VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
-					selected_module = veri_lib ? veri_lib->GetModule(module.c_str(), 1) : nullptr;
-					if (!selected_module) {
-						log_error("Can't find module '%s'.\n", module.c_str());
-					}
-					continue;
-				}
-				if (args[argidx] == "-blacklist" && argidx < GetSize(args)) {
-					if (!(argidx+1 < GetSize(args)))
-						cmd_error(args, argidx+1, "No blacklist specified.\n");
-
-					std::string line = args[++argidx];
-					std::string p;
-					while (!(p = next_token(line, ",\t\r\n ")).empty())
-						blacklists.push_back(p);
-					continue;
-				}
-				if (args[argidx] == "-blfile" && argidx < GetSize(args)) {
-					if (!(argidx+1 < GetSize(args)))
-						cmd_error(args, argidx+1, "No blacklist file specified.\n");
-					std::string fn = args[++argidx];
-					std::ifstream f(fn);
-					if (f.fail())
-						log_cmd_error("Can't open blacklist file '%s'!\n", fn.c_str());
-
-					std::string line,p;
-					while (std::getline(f, line)) {
-						while (!(p = next_token(line, ",\t\r\n ")).empty())
-							blacklists.push_back(p);
-					}
-					continue;
-				}
-				break;
-			}
-			if (argidx < GetSize(args))
-				cmd_error(args, argidx, "unknown option/parameter");
-
-			application->setBlacklists(&blacklists);
-			application->setSingleModuleMode(selected_module!=nullptr);
-
-			const char *err = application->validate();
-			if (err)
-				cmd_error(args, argidx, err);
-
-			MapIter mi;
-			VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
-			log("Running formal application '%s'.\n", app.c_str());
-
-			if (selected_module) {
-				std::string out;
-				if (!application->execute(selected_module, out))
-					log_error("%s", out.c_str());
-			}
-			else {
-				VeriModule *module ;
-				FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, module) {
-					std::string out;
-					if (!application->execute(module, out)) {
-						log_error("%s", out.c_str());
-						break;
-					}
-				}
-			}
-			goto check_error;
-		}
-#endif
 		if (argidx < GetSize(args) && args[argidx] == "-pp")
 		{
 			const char* filename = nullptr;
@ -3017,91 +2914,6 @@ struct VerificPass : public Pass {
 			goto check_error;
 		}

-#ifdef YOSYSHQ_VERIFIC_TEMPLATES
-		if (argidx < GetSize(args) && args[argidx] == "-template")
-		{
-			if (!(argidx+1 < GetSize(args)))
-				cmd_error(args, argidx+1, "No template type specified.\n");
-
-			VerificTemplateGenerator vfg;
-			auto gens = vfg.GetGenerators();
-			std::string app = args[++argidx];
-			if (gens.find(app) == gens.end())
-				log_cmd_error("Template generator '%s' does not exist.\n", app.c_str());
-			TemplateGenerator *generator = gens[app];
-			if (!(argidx+1 < GetSize(args)))
-				cmd_error(args, argidx+1, "No top module specified.\n");
-			generator->setLogger([](std::string msg) { log("%s",msg.c_str()); } );
-
-			std::string module = args[++argidx];
-			VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
-			VeriModule *veri_module = veri_lib ? veri_lib->GetModule(module.c_str(), 1) : nullptr;
-			if (!veri_module) {
-				log_error("Can't find module/unit '%s'.\n", module.c_str());
-			}
-
-			log("Template '%s' is running for module '%s'.\n", app.c_str(),module.c_str());
-
-			Map parameters(STRING_HASH);
-			const char *out_filename = nullptr;
-
-			for (argidx++; argidx < GetSize(args); argidx++) {
-				std::string error;
-				if (generator->checkParams(args, argidx, error)) {
-					if (!error.empty())
-						cmd_error(args, argidx, error);
-					continue;
-				}
-
-				if (args[argidx] == "-chparam"  && argidx < GetSize(args)) {
-					if (!(argidx+1 < GetSize(args)))
-						cmd_error(args, argidx+1, "No param name specified.\n");
-					if (!(argidx+2 < GetSize(args)))
-						cmd_error(args, argidx+2, "No param value specified.\n");
-
-					const std::string &key = args[++argidx];
-					const std::string &value = args[++argidx];
-					unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
-									           1 /* force_overwrite */);
-					if (!new_insertion)
-						log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str());
-					continue;
-				}
-
-				if (args[argidx] == "-out" && argidx < GetSize(args)) {
-					if (!(argidx+1 < GetSize(args)))
-						cmd_error(args, argidx+1, "No output file specified.\n");
-					out_filename = args[++argidx].c_str();
-					continue;
-				}
-
-				break;
-			}
-			if (argidx < GetSize(args))
-				cmd_error(args, argidx, "unknown option/parameter");
-
-			const char *err = generator->validate();
-			if (err)
-				cmd_error(args, argidx, err);
-
-			std::string val;
-			if (!generator->generate(veri_module, val, &parameters))
-				log_error("%s", val.c_str());
-
-			FILE *of = stdout;
-			if (out_filename) {
-				of = fopen(out_filename, "w");
-				if (of == nullptr)
-					log_error("Can't open '%s' for writing: %s\n", out_filename, strerror(errno));
-				log("Writing output to '%s'\n",out_filename);
-			}
-			fprintf(of, "%s\n",val.c_str());
-			fflush(of);
-			if (of!=stdout)
-				fclose(of);
-			goto check_error;
-		}
-#endif
 		if (GetSize(args) > argidx && args[argidx] == "-import")
 		{
 			std::map<std::string,Netlist*> nl_todo, nl_done;
@ -3312,6 +3124,7 @@ struct VerificPass : public Pass {
 			LineFile::DeleteAllLineFiles();
 			verific_incdirs.clear();
 			verific_libdirs.clear();
+			verific_libexts.clear();
 			verific_import_pending = false;
 			goto check_error;
 		}
--- a/kernel/constids.inc
+++ b/kernel/constids.inc
@ -137,6 +137,7 @@ X(nomem2reg)
 X(nomeminit)
 X(nosync)
 X(nowrshmsk)
+X(no_rw_check)
 X(O)
 X(OFFSET)
 X(onehot)
@ -195,6 +196,8 @@ X(STATE_NUM)
 X(STATE_NUM_LOG2)
 X(STATE_RST)
 X(STATE_TABLE)
+X(smtlib2_module)
+X(smtlib2_comb_expr)
 X(submod)
 X(syn_ramstyle)
 X(syn_romstyle)
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@ -204,7 +204,7 @@ RTLIL::Const::Const()
 	flags = RTLIL::CONST_FLAG_NONE;
 }

-RTLIL::Const::Const(std::string str)
+RTLIL::Const::Const(const std::string &str)
 {
 	flags = RTLIL::CONST_FLAG_STRING;
 	bits.reserve(str.size() * 8);
@ -243,14 +243,6 @@ RTLIL::Const::Const(const std::vector<bool> &bits)
 		this->bits.emplace_back(b ? State::S1 : State::S0);
 }

-RTLIL::Const::Const(const RTLIL::Const &c)
-{
-	flags = c.flags;
-	this->bits.reserve(c.size());
-	for (const auto &b : c.bits)
-		this->bits.push_back(b);
-}
-
 bool RTLIL::Const::operator <(const RTLIL::Const &other) const
 {
 	if (bits.size() != other.bits.size())
@ -1850,6 +1842,8 @@ void RTLIL::Module::check()
 			log_assert(!it2.first.empty());
 	}

+	pool<IdString> packed_memids;
+
 	for (auto &it : cells_) {
 		log_assert(this == it.second->module);
 		log_assert(it.first == it.second->name);
@ -1865,6 +1859,14 @@ void RTLIL::Module::check()
 			log_assert(!it2.first.empty());
 		InternalCellChecker checker(this, it.second);
 		checker.check();
+		if (it.second->has_memid()) {
+			log_assert(memories.count(it.second->parameters.at(ID::MEMID).decode_string()));
+		} else if (it.second->is_mem_cell()) {
+			IdString memid = it.second->parameters.at(ID::MEMID).decode_string();
+			log_assert(!memories.count(memid));
+			log_assert(!packed_memids.count(memid));
+			packed_memids.insert(memid);
+		}
 	}

 	for (auto &it : processes) {
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@ -636,12 +636,12 @@ struct RTLIL::Const
 	std::vector<RTLIL::State> bits;

 	Const();
-	Const(std::string str);
+	Const(const std::string &str);
 	Const(int val, int width = 32);
 	Const(RTLIL::State bit, int width = 1);
 	Const(const std::vector<RTLIL::State> &bits) : bits(bits) { flags = CONST_FLAG_NONE; }
 	Const(const std::vector<bool> &bits);
-	Const(const RTLIL::Const &c);
+	Const(const RTLIL::Const &c) = default;
 	RTLIL::Const &operator =(const RTLIL::Const &other) = default;

 	bool operator <(const RTLIL::Const &other) const;
--- a/manual/command-reference-manual.tex
+++ b/manual/command-reference-manual.tex
@ -2744,14 +2744,15 @@ is used then the $macc cell is mapped to $add, $sub, etc. cells instead.
 \section{memory -- translate memories to basic cells}
 \label{cmd:memory}
 \begin{lstlisting}[numbers=left,frame=single]
-    memory [-nomap] [-nordff] [-nowiden] [-nosat] [-memx] [-bram <bram_rules>] [selection]
+    memory [-norom] [-nomap] [-nordff] [-nowiden] [-nosat] [-memx] [-no-rw-check] [-bram <bram_rules>] [selection]

 This pass calls all the other memory_* passes in a useful order:

    opt_mem
    opt_mem_priority
    opt_mem_feedback
-    memory_dff                          (skipped if called with -nordff or -memx)
+    memory_bmux2rom                     (skipped if called with -norom)
+    memory_dff [-no-rw-check]           (skipped if called with -nordff or -memx)
    opt_clean
    memory_share [-nowiden] [-nosat]
    opt_mem_widen
@ -2765,6 +2766,14 @@ This converts memories to word-wide DFFs and address decoders
 or multiport memory blocks if called with the -nomap option.
 \end{lstlisting}

+\section{memory\_bmux2rom -- convert muxes to ROMs}
+\label{cmd:memory_bmux2rom}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_bmux2rom [options] [selection]
+
+This pass converts $bmux cells with constant A input to ROMs.
+\end{lstlisting}
+
 \section{memory\_bram -- map memories to block rams}
 \label{cmd:memory_bram}
 \begin{lstlisting}[numbers=left,frame=single]
@ -2878,11 +2887,45 @@ memory cells.
 \section{memory\_dff -- merge input/output DFFs into memory read ports}
 \label{cmd:memory_dff}
 \begin{lstlisting}[numbers=left,frame=single]
-    memory_dff [options] [selection]
+    memory_dff [-no-rw-check] [selection]

 This pass detects DFFs at memory read ports and merges them into the memory port.
 I.e. it consumes an asynchronous memory port and the flip-flops at its
 interface and yields a synchronous memory port.
+
+    -no-rw-check
+        marks all recognized read ports as "return don't-care value on
+        read/write collision" (same result as setting the no_rw_check
+        attribute on all memories).
+\end{lstlisting}
+
+\section{memory\_libmap -- map memories to cells}
+\label{cmd:memory_libmap}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_libmap -lib <library_file> [-D <condition>] [selection]
+
+This pass takes a description of available RAM cell types and maps
+all selected memories to one of them, or leaves them  to be mapped to FFs.
+
+  -lib <library_file>
+    Selects a library file containing RAM cell definitions. This option
+    can be passed more than once to select multiple libraries.
+    See passes/memory/memlib.md for description of the library format.
+
+  -D <condition>
+    Enables a condition that can be checked within the library file
+    to eg. select between slightly different hardware variants.
+    This option can be passed any number of times.
+
+  -logic-cost-rom <num>
+  -logic-cost-ram <num>
+    Sets the cost of a single bit for memory lowered to soft logic.
+
+  -no-auto-distributed
+  -no-auto-block
+  -no-auto-huge
+    Disables automatic mapping of given kind of RAMs.  Manual mapping
+    (using ram_style or other attributes) is still supported.
 \end{lstlisting}

 \section{memory\_map -- translate multiport memories to basic cells}
@ -3270,6 +3313,15 @@ It also performs some simple expression rewriting.
        replaced by 'a'. the -keepdc option disables all such optimizations.
 \end{lstlisting}

+\section{opt\_ffinv -- push inverters through FFs}
+\label{cmd:opt_ffinv}
+\begin{lstlisting}[numbers=left,frame=single]
+    opt_ffinv [selection]
+
+This pass pushes inverters to the other side of a FF when they can be merged
+into LUTs on the other side.
+\end{lstlisting}
+
 \section{opt\_lut -- optimize LUT cells}
 \label{cmd:opt_lut}
 \begin{lstlisting}[numbers=left,frame=single]
@ -3595,6 +3647,7 @@ This pass calls all the other proc_* passes in the most common order.
    proc_prune
    proc_init
    proc_arst
+    proc_rom
    proc_mux
    proc_dlatch
    proc_dff
@ -3610,6 +3663,9 @@ The following options are supported:
    -nomux
        Will omit the proc_mux pass.

+    -norom
+        Will omit the proc_rom pass.
+
    -global_arst [!]<netname>
        This option is passed through to proc_arst.

@ -3716,6 +3772,14 @@ a later assignment to the same signal and removes them.
 This pass identifies unreachable branches in decision trees and removes them.
 \end{lstlisting}

+\section{proc\_rom -- convert switches to ROMs}
+\label{cmd:proc_rom}
+\begin{lstlisting}[numbers=left,frame=single]
+    proc_rom [selection]
+
+This pass converts switches into read-only memories when appropriate.
+\end{lstlisting}
+
 \section{qbfsat -- solve a 2QBF-SAT problem in the circuit}
 \label{cmd:qbfsat}
 \begin{lstlisting}[numbers=left,frame=single]
@ -4498,15 +4562,16 @@ described here.
    -unset <name>
        do not modify the current selection. instead remove a previously saved
        selection under the given name (see @<name> below).
+
    -assert-none
        do not modify the current selection. instead assert that the given
-        selection is empty. i.e. produce an error if any object matching the
-        selection is found.
+        selection is empty. i.e. produce an error if any object or module
+        matching the selection is found.

    -assert-any
        do not modify the current selection. instead assert that the given
-        selection is non-empty. i.e. produce an error if no object matching
-        the selection is found.
+        selection is non-empty. i.e. produce an error if no object or module
+        matching the selection is found.

    -assert-count N
        do not modify the current selection. instead assert that the given
@ -5257,6 +5322,11 @@ on partly selected designs.
    -flowmap
        use FlowMap LUT techmapping instead of ABC

+    -no-rw-check
+        marks all recognized read ports as "return don't-care value on
+        read/write collision" (same result as setting the no_rw_check
+        attribute on all memories).
+

 The following commands are executed by this synthesis command:

@ -5424,16 +5494,9 @@ The following commands are executed by this synthesis command:
    coarse:
        synth -run coarse

-    map_bram:    (skip if -nobram)
-        memory_bram -rules +/anlogic/brams.txt
-        techmap -map +/anlogic/brams_map.v
-        setundef -zero -params t:EG_PHY_BRAM
-        setundef -zero -params t:EG_PHY_BRAM32K
-
-    map_lutram:    (skip if -nolutram)
-        memory_bram -rules +/anlogic/lutrams.txt
-        techmap -map +/anlogic/lutrams_map.v
-        setundef -zero -params t:EG_LOGIC_DRAM16X4
+    map_ram:
+        memory_libmap -lib +/anlogic/lutrams.txt -lib +/anlogic/brams.txt [-no-auto-block] [-no-auto-distributed]    (-no-auto-block if -nobram, -no-auto-distributed if -nolutram)
+        techmap -map +/anlogic/lutrams_map.v -map +/anlogic/brams_map.v

    map_ffram:
        opt -fast -mux_undef -undriven -fine
@ -5697,6 +5760,11 @@ This command runs synthesis for ECP5 FPGAs.
    -nodsp
        do not map multipliers to MULT18X18D

+    -no-rw-check
+        marks all recognized read ports as "return don't-care value on
+        read/write collision" (same result as setting the no_rw_check
+        attribute on all memories).
+

 The following commands are executed by this synthesis command:

@ -5726,20 +5794,16 @@ The following commands are executed by this synthesis command:
        chtype -set $mul t:$__soft_mul    (unless -nodsp)
        alumacc
        opt
-        memory -nomap
+        memory -nomap [-no-rw-check]
        opt_clean

-    map_bram:    (skip if -nobram)
-        memory_bram -rules +/ecp5/brams.txt
-        techmap -map +/ecp5/brams_map.v
-
-    map_lutram:    (skip if -nolutram)
-        memory_bram -rules +/ecp5/lutrams.txt
-        techmap -map +/ecp5/lutrams_map.v
+    map_ram:
+        memory_libmap -lib +/ecp5/lutrams.txt -lib +/ecp5/brams.txt [-no-auto-block] [-no-auto-distributed]    (-no-auto-block if -nobram, -no-auto-distributed if -nolutram)
+        techmap -map +/ecp5/lutrams_map.v -map +/ecp5/brams_map.v

    map_ffram:
        opt -fast -mux_undef -undriven -fine
-        memory_map -iattr -attr !ram_block -attr !rom_block -attr logic_block -attr syn_ramstyle=auto -attr syn_ramstyle=registers -attr syn_romstyle=auto -attr syn_romstyle=logic
+        memory_map
        opt -undriven -fine

    map_gates:
@ -5835,9 +5899,10 @@ The following commands are executed by this synthesis command:

    coarse:
        synth -run coarse
-        memory_bram -rules +/efinix/brams.txt
+
+    map_ram:
+        memory_libmap -lib +/efinix/brams.txt
        techmap -map +/efinix/brams_map.v
-        setundef -zero -params t:EFX_RAM_5K

    map_ffram:
        opt -fast -mux_undef -undriven -fine
@ -5969,8 +6034,7 @@ The following commands are executed by this synthesis command:
        opt_clean

    map_bram:    (skip if '-nobram')
-        memory_bram -rules +/gatemate/brams.txt
-        setundef -zero -params t:$__CC_BRAM_CASCADE t:$__CC_BRAM_40K_SDP t:$__CC_BRAM_20K_SDP t:$__CC_BRAM_20K_TDP t:$__CC_BRAM_40K_TDP 
+        memory_libmap -lib +/gatemate/brams.txt
        techmap -map +/gatemate/brams_map.v

    map_ffram:
@ -6076,6 +6140,11 @@ This command runs synthesis for Gowin FPGAs. This work is experimental.
    -abc9
        use new ABC9 flow (EXPERIMENTAL)

+    -no-rw-check
+        marks all recognized read ports as "return don't-care value on
+        read/write collision" (same result as setting the no_rw_check
+        attribute on all memories).
+

 The following commands are executed by this synthesis command:

@ -6090,16 +6159,11 @@ The following commands are executed by this synthesis command:
        deminout

    coarse:
-        synth -run coarse
+        synth -run coarse [-no-rw-check]

-    map_bram:    (skip if -nobram)
-        memory_bram -rules +/gowin/brams.txt
-        techmap -map +/gowin/brams_map.v
-
-    map_lutram:    (skip if -nolutram)
-        memory_bram -rules +/gowin/lutrams.txt
-        techmap -map +/gowin/lutrams_map.v
-        setundef -params -zero t:RAM16S4
+    map_ram:
+        memory_libmap -lib +/gowin/lutrams.txt -lib +/gowin/brams.txt [-no-auto-block] [-no-auto-distributed]    (-no-auto-block if -nobram, -no-auto-distributed if -nolutram)
+        techmap -map +/gowin/lutrams_map.v -map +/gowin/brams_map.v

    map_ffram:
        opt -fast -mux_undef -undriven -fine
@ -6283,6 +6347,9 @@ This command runs synthesis for iCE40 FPGAs.
    -nobram
        do not use SB_RAM40_4K* cells in output netlist

+    -spram
+        enable automatic inference of SB_SPRAM256KA
+
    -dsp
        use iCE40 UltraPlus DSP cells for large arithmetic

@ -6302,6 +6369,11 @@ This command runs synthesis for iCE40 FPGAs.
    -flowmap
        use FlowMap LUT techmapping instead of abc (EXPERIMENTAL)

+    -no-rw-check
+        marks all recognized read ports as "return don't-care value on
+        read/write collision" (same result as setting the no_rw_check
+        attribute on all memories).
+

 The following commands are executed by this synthesis command:

@ -6329,7 +6401,7 @@ The following commands are executed by this synthesis command:
        techmap -map +/cmp2lut.v -D LUT_WIDTH=4
        opt_expr
        opt_clean
-        memory_dff
+        memory_dff [-no-rw-check]
        wreduce t:$mul
        techmap -map +/mul2dsp.v -map +/ice40/dsp_map.v -D DSP_A_MAXWIDTH=16 -D DSP_B_MAXWIDTH=16 -D DSP_A_MINWIDTH=2 -D DSP_B_MINWIDTH=2 -D DSP_Y_MINWIDTH=11 -D DSP_NAME=$__MUL16X16    (if -dsp)
        select a:mul2dsp                  (if -dsp)
@ -6341,17 +6413,17 @@ The following commands are executed by this synthesis command:
        chtype -set $mul t:$__soft_mul    (if -dsp)
        alumacc
        opt
-        memory -nomap
+        memory -nomap [-no-rw-check]
        opt_clean

-    map_bram:    (skip if -nobram)
-        memory_bram -rules +/ice40/brams.txt
-        techmap -map +/ice40/brams_map.v
+    map_ram:
+        memory_libmap -lib +/ice40/brams.txt -lib +/ice40/spram.txt -no-auto-huge [-no-auto-huge] [-no-auto-block]    (-no-auto-huge unless -spram, -no-auto-block if -nobram)
+        techmap -map +/ice40/brams_map.v -map +/ice40/spram_map.v
        ice40_braminit

    map_ffram:
        opt -fast -mux_undef -undriven -fine
-        memory_map -iattr -attr !ram_block -attr !rom_block -attr logic_block -attr syn_ramstyle=auto -attr syn_ramstyle=registers -attr syn_romstyle=auto -attr syn_romstyle=logic
+        memory_map
        opt -undriven -fine

    map_gates:
@ -6669,6 +6741,12 @@ This command runs synthesis for MachXO2 FPGAs.
        from label is synonymous to 'begin', and empty to label is
        synonymous to the end of the command list.

+    -nobram
+        do not use block RAM cells in output netlist
+
+    -nolutram
+        do not use LUT RAM cells in output netlist
+
    -noflatten
        do not flatten design before synthesis

@ -6695,6 +6773,10 @@ The following commands are executed by this synthesis command:
    coarse:
        synth -run coarse

+    map_ram:
+        memory_libmap -lib +/machxo2/lutrams.txt -lib +/machxo2/brams.txt [-no-auto-block] [-no-auto-distributed]    (-no-auto-block if -nobram, -no-auto-distributed if -nolutram)
+        techmap -map +/machxo2/lutrams_map.v -map +/machxo2/brams_map.v
+
    fine:
        memory_map
        opt -full
@ -6830,24 +6912,13 @@ The following commands are executed by this synthesis command:
        memory -nomap
        opt_clean

-    map_lram:    (skip if -nolram)
-        memory_bram -rules +/nexus/lrams.txt
-        setundef -zero -params t:$__NX_PDPSC512K
-        techmap -map +/nexus/lrams_map.v
-
-    map_bram:    (skip if -nobram)
-        memory_bram -rules +/nexus/brams.txt
-        setundef -zero -params t:$__NX_PDP16K
-        techmap -map +/nexus/brams_map.v
-
-    map_lutram:    (skip if -nolutram)
-        memory_bram -rules +/nexus/lutrams.txt
-        setundef -zero -params t:$__NEXUS_DPR16X4
-        techmap -map +/nexus/lutrams_map.v
+    map_ram:
+        memory_libmap -lib +/nexus/lutrams.txt -lib +/nexus/brams.txt -lib +/nexus/lrams.txt -no-auto-huge [-no-auto-block] [-no-auto-distributed]    (-no-auto-block if -nobram, -no-auto-distributed if -nolutram)
+        techmap -map +/nexus/lutrams_map.v -map +/nexus/brams_map.v -map +/nexus/lrams_map.v

    map_ffram:
        opt -fast -mux_undef -undriven -fine
-        memory_map -iattr -attr !ram_block -attr !rom_block -attr logic_block -attr syn_ramstyle=auto -attr syn_ramstyle=registers -attr syn_romstyle=auto -attr syn_romstyle=logic
+        memory_map
        opt -undriven -fine

    map_gates:
@ -7238,17 +7309,10 @@ The following commands are executed by this synthesis command:
        memory -nomap
        opt_clean

-    map_uram:    (only if '-uram')
-        memory_bram -rules +/xilinx/{family}_urams.txt
-        techmap -map +/xilinx/{family}_urams_map.v
-
-    map_bram:    (skip if '-nobram')
-        memory_bram -rules +/xilinx/{family}_brams.txt
-        techmap -map +/xilinx/{family}_brams_map.v
-
-    map_lutram:    (skip if '-nolutram')
-        memory_bram -rules +/xilinx/lut[46]_lutrams.txt
-        techmap -map +/xilinx/lutrams_map.v
+    map_memory:
+        memory_libmap [...]
+        techmap -map +/xilinx/lutrams_<family>_map.v
+        techmap -map +/xilinx/brams_<family>_map.v

    map_ffram:
        opt -fast -full
@ -7718,31 +7782,36 @@ Like -sv, but define FORMAL instead of SYNTHESIS.
 Load the specified VHDL files into Verific.


-    verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal] <command-file>
+    verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|
+                     -sv2012|-sv|-formal] <command-file>

 Load and execute the specified command file.
 Override verilog parsing mode can be set.
 The macros YOSYS, SYNTHESIS/FORMAL, and VERIFIC are defined implicitly.

-Command file parser supports following commands:
-    +define    - defines macro
-    -u         - upper case all identifier (makes Verilog parser case insensitive)
-    -v         - register library name (file)
-    -y         - register library name (directory)
-    +incdir    - specify include dir
-    +libext    - specify library extension
-    +liborder  - add library in ordered list
-    +librescan - unresolved modules will be always searched starting with the first
-                 library specified by -y/-v options.
-    -f/-file   - nested -f option
-    -F         - nested -F option
+Command file parser supports following commands in file:
+    +define+<MACRO>=<VALUE> - defines macro
+    -u                      - upper case all identifier (makes Verilog parser
+                              case insensitive)
+    -v <filepath>           - register library name (file)
+    -y <filepath>           - register library name (directory)
+    +incdir+<filepath>      - specify include dir
+    +libext+<filepath>      - specify library extension
+    +liborder+<id>          - add library in ordered list
+    +librescan              - unresolved modules will be always searched
+                              starting with the first library specified
+                              by -y/-v options.
+    -f/-file <filepath>     - nested -f option
+    -F <filepath>           - nested -F option (relative path)
+    parse files:
+        <filepath>
+        +systemverilogext+<filepath>
+        +verilog1995ext+<filepath>
+        +verilog2001ext+<filepath>

-    parse mode:
+    analysis mode:
        -ams
-        +systemverilogext
        +v2k
-        +verilog1995ext
-        +verilog2001ext
        -sverilog


@ -7769,6 +7838,11 @@ Add Verilog library directories. Verific will search in this directories to
 find undefined modules.


+    verific -vlog-libext <extension>..
+
+Add Verilog library extensions, used when searching in library directories.
+
+
    verific -vlog-define <macro>[=<value>]..

 Add Verilog defines.
@ -7879,8 +7953,8 @@ Application options:
        Parameter can also contain comma separated list of file locations.

    -blfile <file>
-        Do not run application on locations specified in file, they can represent filename
-        or filename and location in file.
+        Do not run application on locations specified in file, they can
+        represent filename or filename and location in file.

 Applications:

@ -7988,6 +8062,9 @@ Options:
        Do not change the width of memory address ports. Use this options in
        flows that use the 'memory_memx' pass.

+    -mux_undef
+        remove 'undef' inputs from $mux, $pmux and $_MUX_ cells
+
    -keepdc
        Do not optimize explicit don't-care values.
 \end{lstlisting}
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@ -66,7 +66,7 @@ static std::string derive_name_from_src(const std::string &src, int counter)
 		return stringf("\\%s$%d", src_base.c_str(), counter);
 }

-static IdString derive_name_from_cell_output_wire(const RTLIL::Cell *cell)
+static IdString derive_name_from_cell_output_wire(const RTLIL::Cell *cell, string suffix)
 {
 	// Find output
 	const SigSpec *output = nullptr;
@ -99,7 +99,10 @@ static IdString derive_name_from_cell_output_wire(const RTLIL::Cell *cell)
 		}
 	}

-	return name + cell->type.str();
+	if (suffix.empty()) {
+		suffix = cell->type.str();
+	}
+	return name + suffix;
 }

 struct RenamePass : public Pass {
@ -127,10 +130,12 @@ struct RenamePass : public Pass {
 		log("cells with private names.\n");
 		log("\n");
 		log("\n");
-		log("    rename -wire [selection]\n");
+		log("    rename -wire [selection] [-suffix <suffix>]\n");
 		log("\n");
 		log("Assign auto-generated names based on the wires they drive to all selected\n");
 		log("cells with private names. Ignores cells driving privatly named wires.\n");
+		log("By default, the cell is named after the wire with the cell type as suffix.\n");
+		log("The -suffix option can be used to set the suffix to the given string instead.\n");
 		log("\n");
 		log("\n");
 		log("    rename -enumerate [-pattern <pattern>] [selection]\n");
@ -155,6 +160,7 @@ struct RenamePass : public Pass {
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
 		std::string pattern_prefix = "_", pattern_suffix = "_";
+		std::string cell_suffix = "";
 		bool flag_src = false;
 		bool flag_wire = false;
 		bool flag_enumerate = false;
@ -203,6 +209,9 @@ struct RenamePass : public Pass {
 				pattern_suffix = args[argidx].substr(pos+1);
 				continue;
 			}
+			if (arg == "-suffix" && argidx + 1 < args.size()) {
+				cell_suffix = args[++argidx];
+			}
 			break;
 		}

@ -240,7 +249,7 @@ struct RenamePass : public Pass {
 				dict<RTLIL::Cell *, IdString> new_cell_names;
 				for (auto cell : module->selected_cells())
 					if (cell->name[0] == '$')
-						new_cell_names[cell] = derive_name_from_cell_output_wire(cell);
+						new_cell_names[cell] = derive_name_from_cell_output_wire(cell, cell_suffix);
 				for (auto &it : new_cell_names)
 					module->rename(it.first, it.second);
 			}
--- a/passes/cmds/select.cc
+++ b/passes/cmds/select.cc
@ -1456,7 +1456,10 @@ struct SelectPass : public Pass {
 				}
 			}
 			if (count_mode)
+			{
+				design->scratchpad_set_int("select.count", total_count);
 				log("%d objects.\n", total_count);
+			}
 			if (f != nullptr)
 				fclose(f);
 		#undef LOG_OBJECT
--- a/passes/cmds/show.cc
+++ b/passes/cmds/show.cc
@ -191,7 +191,12 @@ struct ShowWorker

 		std::string str;
 		for (char ch : id) {
-			if (ch == '\\' || ch == '"')
+			if (ch == '\\') {
+				 // new graphviz have bug with escaping '\'
+				str += "&#9586;";
+				continue;
+			}
+			if (ch == '"')
 				str += "\\";
 			str += ch;
 		}
--- a/passes/cmds/sta.cc
+++ b/passes/cmds/sta.cc
@ -58,10 +58,13 @@ struct StaWorker
 	{
 		TimingInfo timing;

+		pool<IdString> unrecognised_cells;
+
 		for (auto cell : module->cells())
 		{
 			Module *inst_module = design->module(cell->type);
 			if (!inst_module) {
+				if (unrecognised_cells.insert(cell->type).second)
 					log_warning("Cell type '%s' not recognised! Ignoring.\n", log_id(cell->type));
 				continue;
 			}
--- a/passes/cmds/stat.cc
+++ b/passes/cmds/stat.cc
@ -381,6 +381,15 @@ struct StatPass : public Pass {

 			log("\n");
 			data.log_data(top_mod->name, true);
+			design->scratchpad_set_int("stat.num_wires", data.num_wires);
+			design->scratchpad_set_int("stat.num_wire_bits", data.num_wire_bits);
+			design->scratchpad_set_int("stat.num_pub_wires", data.num_pub_wires);
+			design->scratchpad_set_int("stat.num_pub_wire_bits", data.num_pub_wire_bits);
+			design->scratchpad_set_int("stat.num_memories", data.num_memories);
+			design->scratchpad_set_int("stat.num_memory_bits", data.num_memory_bits);
+			design->scratchpad_set_int("stat.num_processes", data.num_processes);
+			design->scratchpad_set_int("stat.num_cells", data.num_cells);
+			design->scratchpad_set_int("stat.area", data.area);
 		}

 		log("\n");
--- a/passes/fsm/fsmdata.h
+++ b/passes/fsm/fsmdata.h
@ -91,8 +91,8 @@ struct FsmData
 		if (reset_state < 0 || reset_state >= state_num)
 			reset_state = -1;

-		RTLIL::Const state_table = cell->parameters[ID::STATE_TABLE];
-		RTLIL::Const trans_table = cell->parameters[ID::TRANS_TABLE];
+		const RTLIL::Const &state_table = cell->parameters[ID::STATE_TABLE];
+		const RTLIL::Const &trans_table = cell->parameters[ID::TRANS_TABLE];

 		for (int i = 0; i < state_num; i++) {
 			RTLIL::Const state_code;
--- a/passes/memory/memory.cc
+++ b/passes/memory/memory.cc
@ -31,7 +31,7 @@ struct MemoryPass : public Pass {
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    memory [-norom] [-nomap] [-nordff] [-nowiden] [-nosat] [-memx] [-bram <bram_rules>] [selection]\n");
+		log("    memory [-norom] [-nomap] [-nordff] [-nowiden] [-nosat] [-memx] [-no-rw-check] [-bram <bram_rules>] [selection]\n");
 		log("\n");
 		log("This pass calls all the other memory_* passes in a useful order:\n");
 		log("\n");
@ -39,7 +39,7 @@ struct MemoryPass : public Pass {
 		log("    opt_mem_priority\n");
 		log("    opt_mem_feedback\n");
 		log("    memory_bmux2rom                     (skipped if called with -norom)\n");
-		log("    memory_dff                          (skipped if called with -nordff or -memx)\n");
+		log("    memory_dff [-no-rw-check]           (skipped if called with -nordff or -memx)\n");
 		log("    opt_clean\n");
 		log("    memory_share [-nowiden] [-nosat]\n");
 		log("    opt_mem_widen\n");
@ -59,6 +59,7 @@ struct MemoryPass : public Pass {
 		bool flag_nomap = false;
 		bool flag_nordff = false;
 		bool flag_memx = false;
+		string memory_dff_opts;
 		string memory_bram_opts;
 		string memory_share_opts;

@ -92,6 +93,10 @@ struct MemoryPass : public Pass {
 				memory_share_opts += " -nosat";
 				continue;
 			}
+			if (args[argidx] == "-no-rw-check") {
+				memory_dff_opts += " -no-rw-check";
+				continue;
+			}
 			if (argidx+1 < args.size() && args[argidx] == "-bram") {
 				memory_bram_opts += " -rules " + args[++argidx];
 				continue;
@ -106,7 +111,7 @@ struct MemoryPass : public Pass {
 		if (!flag_norom)
 			Pass::call(design, "memory_bmux2rom");
 		if (!flag_nordff)
-			Pass::call(design, "memory_dff");
+			Pass::call(design, "memory_dff" + memory_dff_opts);
 		Pass::call(design, "opt_clean");
 		Pass::call(design, "memory_share" + memory_share_opts);
 		Pass::call(design, "opt_mem_widen");
--- a/passes/memory/memory_dff.cc
+++ b/passes/memory/memory_dff.cc
@ -220,8 +220,9 @@ struct MemoryDffWorker
 	ModWalker modwalker;
 	FfInitVals initvals;
 	FfMergeHelper merger;
+	bool flag_no_rw_check;

-	MemoryDffWorker(Module *module) : module(module), modwalker(module->design)
+	MemoryDffWorker(Module *module, bool flag_no_rw_check) : module(module), modwalker(module->design), flag_no_rw_check(flag_no_rw_check)
 	{
 		modwalker.setup(module);
 		initvals.set(&modwalker.sigmap, module);
@ -357,6 +358,14 @@ struct MemoryDffWorker
 			return;
 		}

+		// Check for no_rw_check
+		bool no_rw_check = flag_no_rw_check || mem.get_bool_attribute(ID::no_rw_check);
+		for (auto attr: {ID::ram_block, ID::rom_block, ID::ram_style, ID::rom_style, ID::ramstyle, ID::romstyle, ID::syn_ramstyle, ID::syn_romstyle}) {
+			if (mem.get_string_attribute(attr) == "no_rw_check") {
+				no_rw_check = true;
+			}
+		}
+
 		// Construct cache.
 		MemQueryCache cache(qcsat, mem, port, ff);

@ -392,6 +401,8 @@ struct MemoryDffWorker
 						pd.uncollidable_mask[j] = true;
 						pd.collision_x_mask[j] = true;
 					}
+					if (no_rw_check)
+						pd.collision_x_mask[j] = true;
 				}
 			}
 			portdata.push_back(pd);
@ -618,25 +629,35 @@ struct MemoryDffPass : public Pass {
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    memory_dff [options] [selection]\n");
+		log("    memory_dff [-no-rw-check] [selection]\n");
 		log("\n");
 		log("This pass detects DFFs at memory read ports and merges them into the memory port.\n");
 		log("I.e. it consumes an asynchronous memory port and the flip-flops at its\n");
 		log("interface and yields a synchronous memory port.\n");
 		log("\n");
+		log("    -no-rw-check\n");
+		log("        marks all recognized read ports as \"return don't-care value on\n");
+		log("        read/write collision\" (same result as setting the no_rw_check\n");
+		log("        attribute on all memories).\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
+		bool flag_no_rw_check = false;
 		log_header(design, "Executing MEMORY_DFF pass (merging $dff cells to $memrd).\n");

 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-no-rw-check") {
+				flag_no_rw_check = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);

 		for (auto mod : design->selected_modules()) {
-			MemoryDffWorker worker(mod);
+			MemoryDffWorker worker(mod, flag_no_rw_check);
 			worker.run();
 		}
 	}
--- a/passes/memory/memory_libmap.cc
+++ b/passes/memory/memory_libmap.cc
@ -443,6 +443,9 @@ void MemMapping::determine_style() {
 			std::string val_s = val.decode_string();
 			for (auto &c: val_s)
 				c = std::tolower(c);
+			// Handled in memory_dff.
+			if (val_s == "no_rw_check")
+				continue;
 			if (val_s == "auto") {
 				// Nothing.
 			} else if (val_s == "logic" || val_s == "registers") {
--- a/passes/opt/opt_ffinv.cc
+++ b/passes/opt/opt_ffinv.cc
@ -72,6 +72,8 @@ struct OptFfInvWorker
 		for (auto &port: q_ports) {
 			if (port.cell == ff.cell && port.port == ID::Q)
 				continue;
+			if (port.cell == d_inv)
+				return false;
 			if (port.port != ID::A)
 				return false;
 			if (!port.cell->type.in(ID($not), ID($_NOT_), ID($lut)))
@ -148,6 +150,8 @@ struct OptFfInvWorker
 		for (auto &port: q_ports) {
 			if (port.cell == ff.cell && port.port == ID::Q)
 				continue;
+			if (port.cell == d_lut)
+				return false;
 			if (port.port != ID::A)
 				return false;
 			if (port.cell->type.in(ID($not), ID($_NOT_))) {
@ -197,10 +201,13 @@ struct OptFfInvWorker
 	{
 		log("Discovering LUTs.\n");

-		for (Cell *cell : module->selected_cells()) {
-			if (!RTLIL::builtin_ff_cell_types().count(cell->type))
-				continue;
+		std::vector<Cell *> ffs;

+		for (Cell *cell : module->selected_cells())
+			if (RTLIL::builtin_ff_cell_types().count(cell->type))
+				ffs.push_back(cell);
+
+		for (Cell *cell : ffs) {
 			FfData ff(&initvals, cell);
 			if (ff.has_sr)
 				continue;
--- a/passes/opt/wreduce.cc
+++ b/passes/opt/wreduce.cc
@ -30,6 +30,7 @@ struct WreduceConfig
 {
 	pool<IdString> supported_cell_types;
 	bool keepdc = false;
+	bool mux_undef = false;

 	WreduceConfig()
 	{
@ -83,7 +84,7 @@ struct WreduceWorker

 			SigBit ref = sig_a[i];
 			for (int k = 0; k < GetSize(sig_s); k++) {
-				if ((config->keepdc || (ref != State::Sx && sig_b[k*GetSize(sig_a) + i] != State::Sx)) && ref != sig_b[k*GetSize(sig_a) + i])
+				if ((config->keepdc || !config->mux_undef || (ref != State::Sx && sig_b[k*GetSize(sig_a) + i] != State::Sx)) && ref != sig_b[k*GetSize(sig_a) + i])
 					goto no_match_ab;
 				if (sig_b[k*GetSize(sig_a) + i] != State::Sx)
 					ref = sig_b[k*GetSize(sig_a) + i];
@ -479,6 +480,9 @@ struct WreducePass : public Pass {
 		log("        Do not change the width of memory address ports. Use this options in\n");
 		log("        flows that use the 'memory_memx' pass.\n");
 		log("\n");
+		log("    -mux_undef\n");
+		log("        remove 'undef' inputs from $mux, $pmux and $_MUX_ cells\n");
+		log("\n");
 		log("    -keepdc\n");
 		log("        Do not optimize explicit don't-care values.\n");
 		log("\n");
@ -500,6 +504,10 @@ struct WreducePass : public Pass {
 				config.keepdc = true;
 				continue;
 			}
+			if (args[argidx] == "-mux_undef") {
+				config.mux_undef = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
--- a/passes/sat/fmcombine.cc
+++ b/passes/sat/fmcombine.cc
@ -64,6 +64,9 @@ struct FmcombineWorker
 		c->parameters = cell->parameters;
 		c->attributes = cell->attributes;

+		if (cell->is_mem_cell())
+			c->parameters[ID::MEMID] = cell->parameters[ID::MEMID].decode_string() + suffix;
+
 		for (auto &conn : cell->connections())
 			c->setPort(conn.first, import_sig(conn.second, suffix));

--- a/passes/techmap/iopadmap.cc
+++ b/passes/techmap/iopadmap.cc
@ -240,13 +240,13 @@ struct IopadmapPass : public Pass {
 		for (auto module : design->selected_modules())
 		{
 			dict<Wire *, dict<int, pair<Cell *, IdString>>> rewrite_bits;
-			pool<SigSig> remove_conns;
+			dict<SigSig, pool<int>> remove_conns;

 			if (!toutpad_celltype.empty() || !tinoutpad_celltype.empty())
 			{
 				dict<SigBit, Cell *> tbuf_bits;
 				pool<SigBit> driven_bits;
-				dict<SigBit, SigSig> z_conns;
+				dict<SigBit, std::pair<SigSig, int>> z_conns;

 				// Gather tristate buffers and always-on drivers.
 				for (auto cell : module->cells())
@ -266,7 +266,7 @@ struct IopadmapPass : public Pass {
 						SigBit dstbit = conn.first[i];
 						SigBit srcbit = conn.second[i];
 						if (!srcbit.wire && srcbit.data == State::Sz) {
-							z_conns[dstbit] = conn;
+							z_conns[dstbit] = {conn, i};
 							continue;
 						}
 						driven_bits.insert(dstbit);
@ -317,8 +317,9 @@ struct IopadmapPass : public Pass {
 							// enable.
 							en_sig = SigBit(State::S0);
 							data_sig = SigBit(State::Sx);
-							if (z_conns.count(wire_bit))
-								remove_conns.insert(z_conns[wire_bit]);
+							auto it = z_conns.find(wire_bit);
+							if (it != z_conns.end())
+								remove_conns[it->second.first].insert(it->second.second);
 						}

 						if (wire->port_input)
@ -477,9 +478,22 @@ struct IopadmapPass : public Pass {

 			if (!remove_conns.empty()) {
 				std::vector<SigSig> new_conns;
-				for (auto &conn : module->connections())
-					if (!remove_conns.count(conn))
+				for (auto &conn : module->connections()) {
+					auto it = remove_conns.find(conn);
+					if (it == remove_conns.end()) {
 						new_conns.push_back(conn);
+					} else {
+						SigSpec lhs, rhs;
+						for (int i = 0; i < GetSize(conn.first); i++) {
+							if (!it->second.count(i)) {
+								lhs.append(conn.first[i]);
+								rhs.append(conn.second[i]);
+							}
+						}
+						new_conns.push_back(SigSig(lhs, rhs));
+
+					}
+				}
 				module->new_connections(new_conns);
 			}

--- a/techlibs/common/synth.cc
+++ b/techlibs/common/synth.cc
@ -81,6 +81,11 @@ struct SynthPass : public ScriptPass
 		log("    -flowmap\n");
 		log("        use FlowMap LUT techmapping instead of ABC\n");
 		log("\n");
+		log("    -no-rw-check\n");
+		log("        marks all recognized read ports as \"return don't-care value on\n");
+		log("        read/write collision\" (same result as setting the no_rw_check\n");
+		log("        attribute on all memories).\n");
+		log("\n");
 		log("\n");
 		log("The following commands are executed by this synthesis command:\n");
 		help_script();
@ -175,6 +180,10 @@ struct SynthPass : public ScriptPass
 				flowmap = true;
 				continue;
 			}
+			if (args[argidx] == "-no-rw-check") {
+				memory_opts += " -no-rw-check";
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
--- a/techlibs/ecp5/synth_ecp5.cc
+++ b/techlibs/ecp5/synth_ecp5.cc
@ -103,6 +103,11 @@ struct SynthEcp5Pass : public ScriptPass
 		log("    -nodsp\n");
 		log("        do not map multipliers to MULT18X18D\n");
 		log("\n");
+		log("    -no-rw-check\n");
+		log("        marks all recognized read ports as \"return don't-care value on\n");
+		log("        read/write collision\" (same result as setting the no_rw_check\n");
+		log("        attribute on all memories).\n");
+		log("\n");
 		log("\n");
 		log("The following commands are executed by this synthesis command:\n");
 		help_script();
@ -110,7 +115,7 @@ struct SynthEcp5Pass : public ScriptPass
 	}

 	string top_opt, blif_file, edif_file, json_file;
-	bool noccu2, nodffe, nobram, nolutram, nowidelut, asyncprld, flatten, dff, retime, abc2, abc9, nodsp, vpr;
+	bool noccu2, nodffe, nobram, nolutram, nowidelut, asyncprld, flatten, dff, retime, abc2, abc9, nodsp, vpr, no_rw_check;

 	void clear_flags() override
 	{
@ -131,6 +136,7 @@ struct SynthEcp5Pass : public ScriptPass
 		vpr = false;
 		abc9 = false;
 		nodsp = false;
+		no_rw_check = false;
 	}

 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
@ -221,6 +227,10 @@ struct SynthEcp5Pass : public ScriptPass
 				nodsp = true;
 				continue;
 			}
+			if (args[argidx] == "-no-rw-check") {
+				no_rw_check = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@ -241,6 +251,12 @@ struct SynthEcp5Pass : public ScriptPass

 	void script() override
 	{
+		std::string no_rw_check_opt = "";
+		if (no_rw_check)
+			no_rw_check_opt = " -no-rw-check";
+		if (help_mode)
+			no_rw_check_opt = " [-no-rw-check]";
+
 		if (check_label("begin"))
 		{
 			run("read_verilog -lib -specify +/ecp5/cells_sim.v +/ecp5/cells_bb.v");
@ -273,7 +289,7 @@ struct SynthEcp5Pass : public ScriptPass
 			}
 			run("alumacc");
 			run("opt");
-			run("memory -nomap");
+			run("memory -nomap" + no_rw_check_opt);
 			run("opt_clean");
 		}

--- a/techlibs/gowin/synth_gowin.cc
+++ b/techlibs/gowin/synth_gowin.cc
@ -81,6 +81,11 @@ struct SynthGowinPass : public ScriptPass
 		log("    -abc9\n");
 		log("        use new ABC9 flow (EXPERIMENTAL)\n");
 		log("\n");
+		log("    -no-rw-check\n");
+		log("        marks all recognized read ports as \"return don't-care value on\n");
+		log("        read/write collision\" (same result as setting the no_rw_check\n");
+		log("        attribute on all memories).\n");
+		log("\n");
 		log("\n");
 		log("The following commands are executed by this synthesis command:\n");
 		help_script();
@ -88,7 +93,7 @@ struct SynthGowinPass : public ScriptPass
 	}

 	string top_opt, vout_file, json_file;
-	bool retime, nobram, nolutram, flatten, nodffe, nowidelut, abc9, noiopads, noalu;
+	bool retime, nobram, nolutram, flatten, nodffe, nowidelut, abc9, noiopads, noalu, no_rw_check;

 	void clear_flags() override
 	{
@ -104,6 +109,7 @@ struct SynthGowinPass : public ScriptPass
 		abc9 = false;
 		noiopads = false;
 		noalu = false;
+		no_rw_check = false;
 	}

 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
@ -172,6 +178,10 @@ struct SynthGowinPass : public ScriptPass
 				noiopads = true;
 				continue;
 			}
+			if (args[argidx] == "-no-rw-check") {
+				no_rw_check = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@ -189,6 +199,12 @@ struct SynthGowinPass : public ScriptPass

 	void script() override
 	{
+		std::string no_rw_check_opt = "";
+		if (no_rw_check)
+			no_rw_check_opt = " -no-rw-check";
+		if (help_mode)
+			no_rw_check_opt = " [-no-rw-check]";
+
 		if (check_label("begin"))
 		{
 			run("read_verilog -specify -lib +/gowin/cells_sim.v");
@ -205,7 +221,7 @@ struct SynthGowinPass : public ScriptPass

 		if (check_label("coarse"))
 		{
-			run("synth -run coarse");
+			run("synth -run coarse" + no_rw_check_opt);
 		}

 		if (check_label("map_ram"))
--- a/techlibs/ice40/synth_ice40.cc
+++ b/techlibs/ice40/synth_ice40.cc
@ -112,6 +112,11 @@ struct SynthIce40Pass : public ScriptPass
 		log("    -flowmap\n");
 		log("        use FlowMap LUT techmapping instead of abc (EXPERIMENTAL)\n");
 		log("\n");
+		log("    -no-rw-check\n");
+		log("        marks all recognized read ports as \"return don't-care value on\n");
+		log("        read/write collision\" (same result as setting the no_rw_check\n");
+		log("        attribute on all memories).\n");
+		log("\n");
 		log("\n");
 		log("The following commands are executed by this synthesis command:\n");
 		help_script();
@ -119,7 +124,7 @@ struct SynthIce40Pass : public ScriptPass
 	}

 	string top_opt, blif_file, edif_file, json_file, device_opt;
-	bool nocarry, nodffe, nobram, spram, dsp, flatten, retime, noabc, abc2, vpr, abc9, dff, flowmap;
+	bool nocarry, nodffe, nobram, spram, dsp, flatten, retime, noabc, abc2, vpr, abc9, dff, flowmap, no_rw_check;
 	int min_ce_use;

 	void clear_flags() override
@ -142,6 +147,7 @@ struct SynthIce40Pass : public ScriptPass
 		abc9 = false;
 		flowmap = false;
 		device_opt = "hx";
+		no_rw_check = false;
 	}

 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
@ -244,6 +250,10 @@ struct SynthIce40Pass : public ScriptPass
 				flowmap = true;
 				continue;
 			}
+			if (args[argidx] == "-no-rw-check") {
+				no_rw_check = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@ -279,6 +289,12 @@ struct SynthIce40Pass : public ScriptPass
 			define = "-D ICE40_U";
 		else
 			define = "-D ICE40_HX";
+		std::string no_rw_check_opt = "";
+		if (no_rw_check)
+			no_rw_check_opt = " -no-rw-check";
+		if (help_mode)
+			no_rw_check_opt = " [-no-rw-check]";
+
 		if (check_label("begin"))
 		{
 			run("read_verilog " + define + " -lib -specify +/ice40/cells_sim.v");
@ -311,7 +327,7 @@ struct SynthIce40Pass : public ScriptPass
 			run("opt_expr");
 			run("opt_clean");
 			if (help_mode || dsp) {
-				run("memory_dff"); // ice40_dsp will merge registers, reserve memory port registers first
+				run("memory_dff" + no_rw_check_opt); // ice40_dsp will merge registers, reserve memory port registers first
 				run("wreduce t:$mul");
 				run("techmap -map +/mul2dsp.v -map +/ice40/dsp_map.v -D DSP_A_MAXWIDTH=16 -D DSP_B_MAXWIDTH=16 "
 						"-D DSP_A_MINWIDTH=2 -D DSP_B_MINWIDTH=2 -D DSP_Y_MINWIDTH=11 "
@ -326,7 +342,7 @@ struct SynthIce40Pass : public ScriptPass
 			}
 			run("alumacc");
 			run("opt");
-			run("memory -nomap");
+			run("memory -nomap" + no_rw_check_opt);
 			run("opt_clean");
 		}

--- a/tests/various/.gitignore
+++ b/tests/various/.gitignore
@ -6,3 +6,5 @@
 /plugin.so
 /plugin.so.dSYM
 /temp
+/smtlib2_module.smt2
+/smtlib2_module-filtered.smt2
--- a/tests/various/smtlib2_module-expected.smt2
+++ b/tests/various/smtlib2_module-expected.smt2
@ -0,0 +1,88 @@
+; SMT-LIBv2 description generated by Yosys $VERSION
+; yosys-smt2-module smtlib2
+(declare-sort |smtlib2_s| 0)
+(declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
+(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
+; yosys-smt2-input a 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
+(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
+; yosys-smt2-output add 8
+(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(bvadd a b)
+))
+; yosys-smt2-output eq 1
+(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(= a b)
+))
+; yosys-smt2-output sub 8
+(define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
+(|a| (|smtlib2_n a| state))
+(|b| (|smtlib2_n b| state))
+)
+(bvadd a (bvneg b))
+))
+(define-fun |smtlib2_a| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_u| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_i| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_h| ((state |smtlib2_s|)) Bool true)
+(define-fun |smtlib2_t| ((state |smtlib2_s|) (next_state |smtlib2_s|)) Bool true) ; end of module smtlib2
+; yosys-smt2-module uut
+(declare-sort |uut_s| 0)
+(declare-fun |uut_is| (|uut_s|) Bool)
+; yosys-smt2-cell smtlib2 s
+(declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add
+(declare-fun |uut#1| (|uut_s|) Bool) ; \eq
+(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
+(declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
+; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
+(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
+; yosys-smt2-assert 0 $assert$smtlib2_module.v:28$19 smtlib2_module.v:28.17-29.22
+(define-fun |uut_a 0| ((state |uut_s|)) Bool (or (|uut#6| state) (not true))) ; $assert$smtlib2_module.v:28$19
+(define-fun |uut#7| ((state |uut_s|)) (_ BitVec 8) (bvsub (|uut#3| state) (|uut#4| state))) ; \sub2
+(define-fun |uut#8| ((state |uut_s|)) Bool (= (|uut#2| state) (|uut#7| state))) ; $0$formal$smtlib2_module.v:29$2_CHECK[0:0]$11
+; yosys-smt2-assert 1 $assert$smtlib2_module.v:29$20 smtlib2_module.v:29.23-30.22
+(define-fun |uut_a 1| ((state |uut_s|)) Bool (or (|uut#8| state) (not true))) ; $assert$smtlib2_module.v:29$20
+(define-fun |uut#9| ((state |uut_s|)) Bool (= (|uut#3| state) (|uut#4| state))) ; $eq$smtlib2_module.v:31$17_Y
+(define-fun |uut#10| ((state |uut_s|)) Bool (= (ite (|uut#1| state) #b1 #b0) (ite (|uut#9| state) #b1 #b0))) ; $0$formal$smtlib2_module.v:30$3_CHECK[0:0]$13
+; yosys-smt2-assert 2 $assert$smtlib2_module.v:30$21 smtlib2_module.v:30.23-31.25
+(define-fun |uut_a 2| ((state |uut_s|)) Bool (or (|uut#10| state) (not true))) ; $assert$smtlib2_module.v:30$21
+(define-fun |uut_a| ((state |uut_s|)) Bool (and
+  (|uut_a 0| state)
+  (|uut_a 1| state)
+  (|uut_a 2| state)
+  (|smtlib2_a| (|uut_h s| state))
+))
+(define-fun |uut_u| ((state |uut_s|)) Bool
+  (|smtlib2_u| (|uut_h s| state))
+)
+(define-fun |uut_i| ((state |uut_s|)) Bool
+  (|smtlib2_i| (|uut_h s| state))
+)
+(define-fun |uut_h| ((state |uut_s|)) Bool (and
+  (= (|uut_is| state) (|smtlib2_is| (|uut_h s| state)))
+  (= (|uut#3| state) (|smtlib2_n a| (|uut_h s| state))) ; smtlib2.a
+  (= (|uut#0| state) (|smtlib2_n add| (|uut_h s| state))) ; smtlib2.add
+  (= (|uut#4| state) (|smtlib2_n b| (|uut_h s| state))) ; smtlib2.b
+  (= (|uut#1| state) (|smtlib2_n eq| (|uut_h s| state))) ; smtlib2.eq
+  (= (|uut#2| state) (|smtlib2_n sub| (|uut_h s| state))) ; smtlib2.sub
+  (|smtlib2_h| (|uut_h s| state))
+))
+(define-fun |uut_t| ((state |uut_s|) (next_state |uut_s|)) Bool (and
+  (= (|uut#4| state) (|uut#4| next_state)) ; $anyconst$5 \b
+  (= (|uut#3| state) (|uut#3| next_state)) ; $anyconst$4 \a
+  (|smtlib2_t| (|uut_h s| state) (|uut_h s| next_state))
+)) ; end of module uut
+; yosys-smt2-topmod uut
+; end of yosys output
--- a/tests/various/smtlib2_module.sh
+++ b/tests/various/smtlib2_module.sh
@ -0,0 +1,5 @@
+#!/bin/bash
+set -ex
+../../yosys -q -p 'read_verilog -formal smtlib2_module.v; prep; write_smt2 smtlib2_module.smt2'
+sed 's/; SMT-LIBv2 description generated by Yosys .*/; SMT-LIBv2 description generated by Yosys $VERSION/;s/  *$//' smtlib2_module.smt2 > smtlib2_module-filtered.smt2
+diff -au smtlib2_module-expected.smt2 smtlib2_module-filtered.smt2
--- a/tests/various/smtlib2_module.v
+++ b/tests/various/smtlib2_module.v
@ -0,0 +1,33 @@
+(* smtlib2_module *)
+module smtlib2(a, b, add, sub, eq);
+	input [7:0] a, b;
+	(* smtlib2_comb_expr = "(bvadd a b)" *)
+	output [7:0] add;
+	(* smtlib2_comb_expr = "(bvadd a (bvneg b))" *)
+	output [7:0] sub;
+	(* smtlib2_comb_expr = "(= a b)" *)
+	output eq;
+endmodule
+
+(* top *)
+module uut;
+	wire [7:0] a = $anyconst, b = $anyconst, add, sub, add2, sub2;
+	wire eq;
+
+	assign add2 = a + b;
+	assign sub2 = a - b;
+
+	smtlib2 s (
+		.a(a),
+		.b(b),
+		.add(add),
+		.sub(sub),
+		.eq(eq)
+	);
+
+	always @* begin
+		assert(add == add2);
+		assert(sub == sub2);
+		assert(eq == (a == b));
+	end
+endmodule