diff --git a/Dockerfile b/Dockerfile
deleted file mode 100644
index 9806696e0..000000000
--- a/Dockerfile
+++ /dev/null
@@ -1,58 +0,0 @@
-ARG IMAGE="python:3-slim-buster"
-
-#---
-
-FROM $IMAGE AS base
-
-RUN apt-get update -qq \
- && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
-    ca-certificates \
-    clang \
-    lld \
-    curl \
-    libffi-dev \
-    libreadline-dev \
-    tcl-dev \
-    graphviz \
-    xdot \
- && apt-get autoclean && apt-get clean && apt-get -y autoremove \
- && update-ca-certificates \
- && rm -rf /var/lib/apt/lists
-
-#---
-
-FROM base AS build
-
-RUN apt-get update -qq \
- && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
-    bison \
-    flex \
-    gawk \
-    gcc \
-    git \
-    iverilog \
-    pkg-config \
- && apt-get autoclean && apt-get clean && apt-get -y autoremove \
- && rm -rf /var/lib/apt/lists
-
-COPY . /yosys
-
-ENV PREFIX /opt/yosys
-
-RUN cd /yosys \
- && make \
- && make install \
- && make test
-
-#---
-
-FROM base
-
-COPY --from=build /opt/yosys /opt/yosys
-
-ENV PATH /opt/yosys/bin:$PATH
-
-RUN useradd -m yosys
-USER yosys
-
-CMD ["yosys"]
diff --git a/Makefile b/Makefile
index 2123fc96c..d0c16aaba 100644
--- a/Makefile
+++ b/Makefile
@@ -177,7 +177,7 @@ ifeq ($(OS), Haiku)
 CXXFLAGS += -D_DEFAULT_SOURCE
 endif
 
-YOSYS_VER := 0.62+9
+YOSYS_VER := 0.62+55
 YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1)
 YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2)
 YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'.' -f3)
@@ -669,6 +669,7 @@ $(eval $(call add_include_file,kernel/yosys_common.h))
 $(eval $(call add_include_file,kernel/yw.h))
 $(eval $(call add_include_file,libs/ezsat/ezsat.h))
 $(eval $(call add_include_file,libs/ezsat/ezminisat.h))
+$(eval $(call add_include_file,libs/ezsat/ezcmdline.h))
 ifeq ($(ENABLE_ZLIB),1)
 $(eval $(call add_include_file,libs/fst/fstapi.h))
 endif
@@ -714,6 +715,7 @@ OBJS += libs/json11/json11.o
 
 OBJS += libs/ezsat/ezsat.o
 OBJS += libs/ezsat/ezminisat.o
+OBJS += libs/ezsat/ezcmdline.o
 
 OBJS += libs/minisat/Options.o
 OBJS += libs/minisat/SimpSolver.o
diff --git a/abc b/abc
index f37e4e136..bb9bc209f 160000
--- a/abc
+++ b/abc
@@ -1 +1 @@
-Subproject commit f37e4e1361d8ed14d2cadf1494143bb1a4d10cf2
+Subproject commit bb9bc209ff23e6690865935a70bcc9294101c5ce
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 054f9b31a..8e05a59a9 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -95,7 +95,8 @@ bool VERILOG_BACKEND::id_is_verilog_escaped(const std::string &str) {
 
 PRIVATE_NAMESPACE_BEGIN
 
-bool verbose, norename, noattr, srcattronly, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs, noparallelcase;
+bool verbose, norename, noattr, srcattronly, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs,
+  noparallelcase, default_params;
 int auto_name_counter, auto_name_offset, auto_name_digits, extmem_counter;
 dict<RTLIL::IdString, int> auto_name_map;
 std::set<RTLIL::IdString> reg_wires;
@@ -439,6 +440,13 @@ void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString,
 	}
 }
 
+void dump_parameter(std::ostream &f, std::string indent, RTLIL::IdString id_string, RTLIL::Const parameter)
+{
+	f << stringf("%sparameter %s = ", indent.c_str(), id(id_string).c_str());
+	dump_const(f, parameter);
+	f << ";\n";
+}
+
 void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
 {
 	dump_attributes(f, indent, wire->attributes, "\n", /*modattr=*/false, /*regattr=*/reg_wires.count(wire->name));
@@ -2456,6 +2464,10 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 		f << indent + "  " << "reg " << id(initial_id) << " = 0;\n";
 	}
 
+	if (default_params)
+		for (auto p : module->parameter_default_values)
+			dump_parameter(f, indent + "  ", p.first, p.second);
+
 	// first dump input / output according to their order in module->ports
 	for (auto port : module->ports)
 		dump_wire(f, indent + "  ", module->wire(port));
@@ -2566,6 +2578,10 @@ struct VerilogBackend : public Backend {
 		log("        use 'defparam' statements instead of the Verilog-2001 syntax for\n");
 		log("        cell parameters.\n");
 		log("\n");
+		log("    -default_params\n");
+		log("        emit module parameter declarations from\n");
+		log("        parameter_default_values.\n");
+		log("\n");
 		log("    -blackboxes\n");
 		log("        usually modules with the 'blackbox' attribute are ignored. with\n");
 		log("        this option set only the modules with the 'blackbox' attribute\n");
@@ -2604,6 +2620,7 @@ struct VerilogBackend : public Backend {
 		siminit = false;
 		simple_lhs = false;
 		noparallelcase = false;
+		default_params = false;
 		auto_prefix = "";
 
 		bool blackboxes = false;
@@ -2668,6 +2685,10 @@ struct VerilogBackend : public Backend {
 				defparam = true;
 				continue;
 			}
+			if (arg == "-defaultparams") {
+				default_params = true;
+				continue;
+			}
 			if (arg == "-decimal") {
 				decimal = true;
 				continue;
diff --git a/frontends/json/jsonparse.cc b/frontends/json/jsonparse.cc
index 743ac5d9e..803931f32 100644
--- a/frontends/json/jsonparse.cc
+++ b/frontends/json/jsonparse.cc
@@ -302,6 +302,9 @@ void json_import(Design *design, string &modname, JsonNode *node)
 	if (node->data_dict.count("attributes"))
 		json_parse_attr_param(module->attributes, node->data_dict.at("attributes"));
 
+	if (node->data_dict.count("parameter_default_values"))
+		json_parse_attr_param(module->parameter_default_values, node->data_dict.at("parameter_default_values"));
+
 	dict<int, SigBit> signal_bits;
 
 	if (node->data_dict.count("ports"))
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 7815847b3..c53d20fe0 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -59,6 +59,7 @@ struct SatSolver
 
 struct ezSatPtr : public std::unique_ptr<ezSAT> {
 	ezSatPtr() : unique_ptr<ezSAT>(yosys_satsolver->create()) { }
+	explicit ezSatPtr(SatSolver *solver) : unique_ptr<ezSAT>((solver ? solver : yosys_satsolver)->create()) { }
 };
 
 struct SatGen
diff --git a/libs/ezsat/ezcmdline.cc b/libs/ezsat/ezcmdline.cc
new file mode 100644
index 000000000..57800591c
--- /dev/null
+++ b/libs/ezsat/ezcmdline.cc
@@ -0,0 +1,92 @@
+
+#include "ezcmdline.h"
+
+#include "../../kernel/yosys.h"
+
+ezCmdlineSAT::ezCmdlineSAT(const std::string &cmd) : command(cmd) {}
+
+ezCmdlineSAT::~ezCmdlineSAT() {}
+
+bool ezCmdlineSAT::solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions)
+{
+#if !defined(YOSYS_DISABLE_SPAWN)
+	const std::string tempdir_name = Yosys::make_temp_dir(Yosys::get_base_tmpdir() + "/yosys-sat-XXXXXX");
+	const std::string cnf_filename = Yosys::stringf("%s/problem.cnf", tempdir_name.c_str());
+	const std::string sat_command = Yosys::stringf("%s %s", command.c_str(), cnf_filename.c_str());
+	FILE *dimacs = fopen(cnf_filename.c_str(), "w");
+	if (dimacs == nullptr) {
+		Yosys::log_cmd_error("Failed to create CNF file `%s`.\n", cnf_filename.c_str());
+	}
+
+	std::vector<int> modelIdx;
+	for (auto id : modelExpressions)
+		modelIdx.push_back(bind(id));
+	std::vector<std::vector<int>> extraClauses;
+	for (auto id : assumptions)
+		extraClauses.push_back({bind(id)});
+
+	printDIMACS(dimacs, false, extraClauses);
+	fclose(dimacs);
+
+	bool status_sat = false;
+	bool status_unsat = false;
+	std::vector<bool> values;
+
+	auto line_callback = [&](const std::string &line) {
+		if (line.empty()) {
+			return;
+		}
+		if (line[0] == 's') {
+			if (line.substr(0, 5) == "s SAT") {
+				status_sat = true;
+			}
+			if (line.substr(0, 7) == "s UNSAT") {
+				status_unsat = true;
+			}
+			return;
+		}
+		if (line[0] == 'v') {
+			std::stringstream ss(line.substr(1));
+			int lit;
+			while (ss >> lit) {
+				if (lit == 0) {
+					return;
+				}
+				bool val = lit >= 0;
+				int ind = lit >= 0 ? lit - 1 : -lit - 1;
+				if (Yosys::GetSize(values) <= ind) {
+					values.resize(ind + 1);
+				}
+				values[ind] = val;
+			}
+		}
+	};
+	int return_code = Yosys::run_command(sat_command, line_callback);
+	if (return_code != 0 && return_code != 10 && return_code != 20) {
+		Yosys::log_cmd_error("Shell command failed!\n");
+	}
+
+	modelValues.clear();
+	modelValues.resize(modelIdx.size());
+
+	if (!status_sat && !status_unsat) {
+		solverTimeoutStatus = true;
+	}
+	if (!status_sat) {
+		return false;
+	}
+
+	for (size_t i = 0; i < modelIdx.size(); i++) {
+		int idx = modelIdx[i];
+		bool refvalue = true;
+
+		if (idx < 0)
+			idx = -idx, refvalue = false;
+
+		modelValues[i] = (values.at(idx - 1) == refvalue);
+	}
+	return true;
+#else
+	Yosys::log_error("SAT solver command not available in this build!\n");
+#endif
+}
diff --git a/libs/ezsat/ezcmdline.h b/libs/ezsat/ezcmdline.h
new file mode 100644
index 000000000..8ec8c7043
--- /dev/null
+++ b/libs/ezsat/ezcmdline.h
@@ -0,0 +1,36 @@
+/*
+ *  ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ *  Copyright (C) 2013  Claire Xenia Wolf <claire@yosyshq.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.
+ *
+ */
+
+#ifndef EZSATCOMMAND_H
+#define EZSATCOMMAND_H
+
+#include "ezsat.h"
+
+class ezCmdlineSAT : public ezSAT
+{
+private:
+	std::string command;
+
+public:
+	ezCmdlineSAT(const std::string &cmd);
+	virtual ~ezCmdlineSAT();
+	bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions) override;
+};
+
+#endif
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 30df625cb..1f4b8855f 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -103,7 +103,7 @@ bool ezMiniSAT::solver(const std::vector<int> &modelExpressions, std::vector<boo
 {
 	preSolverCallback();
 
-	solverTimoutStatus = false;
+	solverTimeoutStatus = false;
 
 	if (0) {
 contradiction:
@@ -206,7 +206,7 @@ contradiction:
 #if defined(HAS_ALARM)
 	if (solverTimeout > 0) {
 		if (alarmHandlerTimeout == 0)
-			solverTimoutStatus = true;
+			solverTimeoutStatus = true;
 		alarm(0);
 		sigaction(SIGALRM, &old_sig_action, NULL);
 		alarm(old_alarm_timeout);
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 20a210abe..8e3114705 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -54,7 +54,7 @@ ezSAT::ezSAT()
 	cnfClausesCount = 0;
 
 	solverTimeout = 0;
-	solverTimoutStatus = false;
+	solverTimeoutStatus = false;
 
 	literal("CONST_TRUE");
 	literal("CONST_FALSE");
@@ -1222,10 +1222,15 @@ ezSATvec ezSAT::vec(const std::vector<int> &vec)
 	return ezSATvec(*this, vec);
 }
 
-void ezSAT::printDIMACS(FILE *f, bool verbose) const
+void ezSAT::printDIMACS(FILE *f, bool verbose, const std::vector<std::vector<int>> &extraClauses) const
 {
+	if (f == nullptr) {
+		fprintf(stderr, "Usage error: printDIMACS() must not be called with a null FILE pointer\n");
+		abort();
+	}
+
 	if (cnfConsumed) {
-		fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!");
+		fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!\n");
 		abort();
 	}
 
@@ -1259,8 +1264,10 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const
 	std::vector<std::vector<int>> all_clauses;
 	getFullCnf(all_clauses);
 	assert(cnfClausesCount == int(all_clauses.size()));
+	for (auto c : extraClauses)
+		all_clauses.push_back(c);
 
-	fprintf(f, "p cnf %d %d\n", cnfVariableCount, cnfClausesCount);
+	fprintf(f, "p cnf %d %d\n", cnfVariableCount, (int) all_clauses.size());
 	int maxClauseLen = 0;
 	for (auto &clause : all_clauses)
 		maxClauseLen = std::max(int(clause.size()), maxClauseLen);
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 7f3bdf68d..445c8edba 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -78,7 +78,7 @@ protected:
 
 public:
 	int solverTimeout;
-	bool solverTimoutStatus;
+	bool solverTimeoutStatus;
 
 	ezSAT();
 	virtual ~ezSAT();
@@ -153,8 +153,8 @@ public:
 		solverTimeout = newTimeoutSeconds;
 	}
 
-	bool getSolverTimoutStatus() {
-		return solverTimoutStatus;
+	bool getSolverTimeoutStatus() {
+		return solverTimeoutStatus;
 	}
 
 	// manage CNF (usually only accessed by SAT solvers)
@@ -295,7 +295,7 @@ public:
 
 	// printing CNF and internal state
 
-	void printDIMACS(FILE *f, bool verbose = false) const;
+	void printDIMACS(FILE *f, bool verbose = false, const std::vector<std::vector<int>> &extraClauses = std::vector<std::vector<int>>()) const;
 	void printInternalState(FILE *f) const;
 
 	// more sophisticated constraints (designed to be used directly with assume(..))
diff --git a/passes/cmds/scratchpad.cc b/passes/cmds/scratchpad.cc
index f64ce943c..24ab5cfd8 100644
--- a/passes/cmds/scratchpad.cc
+++ b/passes/cmds/scratchpad.cc
@@ -37,7 +37,7 @@ struct ScratchpadPass : public Pass {
 		log("\n");
 		log("    scratchpad [options]\n");
 		log("\n");
-		log("This pass allows to read and modify values from the scratchpad of the current\n");
+		log("This pass allows reading and modifying values from the scratchpad of the current\n");
 		log("design. Options:\n");
 		log("\n");
 		log("    -get <identifier>\n");
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 90b85d709..8a0a45dcf 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -31,6 +31,22 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+static SatSolver *find_satsolver(const std::string &name)
+{
+	for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next)
+		if (solver->name == name)
+			return solver;
+	return nullptr;
+}
+
+static std::string list_satsolvers()
+{
+	std::string result;
+	for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next)
+		result += result.empty() ? solver->name : ", " + solver->name;
+	return result;
+}
+
 struct SatHelper
 {
 	RTLIL::Design *design;
@@ -60,8 +76,8 @@ struct SatHelper
 	int max_timestep, timeout;
 	bool gotTimeout;
 
-	SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef, bool set_def_formal) :
-		design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap)
+	SatHelper(RTLIL::Design *design, RTLIL::Module *module, SatSolver *solver, bool enable_undef, bool set_def_formal) :
+		design(design), module(module), sigmap(module), ct(design), ez(solver), satgen(ez.get(), &sigmap)
 	{
 		this->enable_undef = enable_undef;
 		satgen.model_undef = enable_undef;
@@ -441,7 +457,7 @@ struct SatHelper
 		log_assert(gotTimeout == false);
 		ez->setSolverTimeout(timeout);
 		bool success = ez->solve(modelExpressions, modelValues, assumptions);
-		if (ez->getSolverTimoutStatus())
+		if (ez->getSolverTimeoutStatus())
 			gotTimeout = true;
 		return success;
 	}
@@ -451,7 +467,7 @@ struct SatHelper
 		log_assert(gotTimeout == false);
 		ez->setSolverTimeout(timeout);
 		bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f);
-		if (ez->getSolverTimoutStatus())
+		if (ez->getSolverTimeoutStatus())
 			gotTimeout = true;
 		return success;
 	}
@@ -1066,6 +1082,10 @@ struct SatPass : public Pass {
 		log("    -timeout <N>\n");
 		log("        Maximum number of seconds a single SAT instance may take.\n");
 		log("\n");
+		log("    -select-solver <name>\n");
+		log("        Select SAT solver implementation for this invocation.\n");
+		log("        If not given, uses scratchpad key 'sat.solver' if set, otherwise default.\n");
+		log("\n");
 		log("    -verify\n");
 		log("        Return an error and stop the synthesis script if the proof fails.\n");
 		log("\n");
@@ -1097,8 +1117,14 @@ struct SatPass : public Pass {
 
 		log_header(design, "Executing SAT pass (solving SAT problems in the circuit).\n");
 
+		std::string solver_name = design->scratchpad_get_string("sat.solver", "");
+
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-select-solver" && argidx+1 < args.size()) {
+				solver_name = args[++argidx];
+				continue;
+			}
 			if (args[argidx] == "-all") {
 				loopcount = -1;
 				continue;
@@ -1336,6 +1362,14 @@ struct SatPass : public Pass {
 		}
 		extra_args(args, argidx, design);
 
+		SatSolver *solver = yosys_satsolver;
+		if (!solver_name.empty()) {
+			solver = find_satsolver(solver_name);
+			if (solver == nullptr)
+				log_cmd_error("Unknown SAT solver '%s'. Available solvers: %s\n",
+						solver_name, list_satsolvers());
+		}
+
 		RTLIL::Module *module = NULL;
 		for (auto mod : design->selected_modules()) {
 			if (module)
@@ -1398,13 +1432,15 @@ struct SatPass : public Pass {
 				shows.push_back(wire->name.str());
 		}
 
+		log("Using SAT solver `%s`.\n", solver->name.c_str());
+
 		if (tempinduct)
 		{
 			if (loopcount > 0 || max_undef)
 				log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
 
-			SatHelper basecase(design, module, enable_undef, set_def_formal);
-			SatHelper inductstep(design, module, enable_undef, set_def_formal);
+			SatHelper basecase(design, module, solver, enable_undef, set_def_formal);
+			SatHelper inductstep(design, module, solver, enable_undef, set_def_formal);
 
 			basecase.sets = sets;
 			basecase.set_assumes = set_assumes;
@@ -1593,7 +1629,7 @@ struct SatPass : public Pass {
 			if (maxsteps > 0)
 				log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
 
-			SatHelper sathelper(design, module, enable_undef, set_def_formal);
+			SatHelper sathelper(design, module, solver, enable_undef, set_def_formal);
 
 			sathelper.sets = sets;
 			sathelper.set_assumes = set_assumes;
diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index 46bdcfc92..7a5e849d4 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -277,7 +277,7 @@ using AbcSigMap = SigValMap<AbcSigVal>;
 struct RunAbcState {
 	const AbcConfig &config;
 
-	std::string tempdir_name;
+	std::string per_run_tempdir_name;
 	std::vector<gate_t> signal_list;
 	bool did_run = false;
 	bool err = false;
@@ -822,16 +822,23 @@ std::string fold_abc_cmd(std::string str)
 	return new_str;
 }
 
-std::string replace_tempdir(std::string text, std::string tempdir_name, bool show_tempdir)
+std::string replace_tempdir(std::string text, std::string_view global_tempdir_name, std::string_view per_run_tempdir_name, bool show_tempdir)
 {
 	if (show_tempdir)
 		return text;
 
 	while (1) {
-		size_t pos = text.find(tempdir_name);
+		size_t pos = text.find(global_tempdir_name);
 		if (pos == std::string::npos)
 			break;
-		text = text.substr(0, pos) + "<abc-temp-dir>" + text.substr(pos + GetSize(tempdir_name));
+		text = text.substr(0, pos) + "<abc-temp-dir>" + text.substr(pos + GetSize(global_tempdir_name));
+	}
+
+	while (1) {
+		size_t pos = text.find(per_run_tempdir_name);
+		if (pos == std::string::npos)
+			break;
+		text = text.substr(0, pos) + "<abc-temp-dir>" + text.substr(pos + GetSize(per_run_tempdir_name));
 	}
 
 	std::string  selfdir_name = proc_self_dirname();
@@ -853,11 +860,12 @@ struct abc_output_filter
 	bool got_cr;
 	int escape_seq_state;
 	std::string linebuf;
-	std::string tempdir_name;
+	std::string global_tempdir_name;
+	std::string per_run_tempdir_name;
 	bool show_tempdir;
 
-	abc_output_filter(RunAbcState& state, std::string tempdir_name, bool show_tempdir)
-		: state(state), tempdir_name(tempdir_name), show_tempdir(show_tempdir)
+	abc_output_filter(RunAbcState& state, std::string global_tempdir_name, std::string per_run_tempdir_name, bool show_tempdir)
+		: state(state), global_tempdir_name(global_tempdir_name), per_run_tempdir_name(per_run_tempdir_name), show_tempdir(show_tempdir)
 	{
 		got_cr = false;
 		escape_seq_state = 0;
@@ -884,7 +892,7 @@ struct abc_output_filter
 			return;
 		}
 		if (ch == '\n') {
-			state.logs.log("ABC: %s\n", replace_tempdir(linebuf, tempdir_name, show_tempdir));
+			state.logs.log("ABC: %s\n", replace_tempdir(linebuf, global_tempdir_name, per_run_tempdir_name, show_tempdir));
 			got_cr = false, linebuf.clear();
 			return;
 		}
@@ -985,15 +993,19 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module
 
 	const AbcConfig &config = run_abc.config;
 	if (config.cleanup)
-		run_abc.tempdir_name = get_base_tmpdir() + "/";
+		run_abc.per_run_tempdir_name = get_base_tmpdir() + "/";
 	else
-		run_abc.tempdir_name = "_tmp_";
-	run_abc.tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX";
-	run_abc.tempdir_name = make_temp_dir(run_abc.tempdir_name);
+		run_abc.per_run_tempdir_name = "_tmp_";
+	run_abc.per_run_tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX";
+	run_abc.per_run_tempdir_name = make_temp_dir(run_abc.per_run_tempdir_name);
 	log_header(design, "Extracting gate netlist of module `%s' to `%s/input.blif'..\n",
-			module->name.c_str(), replace_tempdir(run_abc.tempdir_name, run_abc.tempdir_name, config.show_tempdir).c_str());
+			module->name.c_str(), replace_tempdir(run_abc.per_run_tempdir_name, config.global_tempdir_name, run_abc.per_run_tempdir_name, config.show_tempdir).c_str());
 
-	std::string abc_script = stringf((std::string("read_blif") + (config.abc_node_retention ? stringf(" -M %d -r", config.abc_max_node_retention_origins) : "") + " \"%s/input.blif\"; ").c_str(), run_abc.tempdir_name);
+	std::string abc_script;
+	if (config.abc_node_retention)
+		abc_script = stringf("read_blif -M %d -r \"%s/input.blif\"; ", config.abc_max_node_retention_origins, run_abc.per_run_tempdir_name);
+	else
+		abc_script = stringf("read_blif \"%s/input.blif\"; ", run_abc.per_run_tempdir_name);
 
 	if (!config.liberty_files.empty() || !config.genlib_files.empty()) {
 		std::string dont_use_args;
@@ -1059,8 +1071,8 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module
 	for (size_t pos = abc_script.find("{S}"); pos != std::string::npos; pos = abc_script.find("{S}", pos))
 		abc_script = abc_script.substr(0, pos) + config.lutin_shared + abc_script.substr(pos+3);
 	if (config.abc_dress)
-		abc_script += stringf("; dress \"%s/input.blif\"", run_abc.tempdir_name);
-	abc_script += stringf("; write_blif %s/output.blif", run_abc.tempdir_name);
+		abc_script += stringf("; dress \"%s/input.blif\"", run_abc.per_run_tempdir_name);
+	abc_script += stringf("; write_blif %s/output.blif", run_abc.per_run_tempdir_name);
 	abc_script = add_echos_to_abc_cmd(abc_script);
 #if defined(__linux__) && !defined(YOSYS_DISABLE_SPAWN)
 	abc_script += "; echo; echo \"YOSYS_ABC_DONE\"\n";
@@ -1070,7 +1082,7 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module
 		if (abc_script[i] == ';' && abc_script[i+1] == ' ')
 			abc_script[i+1] = '\n';
 
-	std::string buffer = stringf("%s/abc.script", run_abc.tempdir_name);
+	std::string buffer = stringf("%s/abc.script", run_abc.per_run_tempdir_name);
 	FILE *f = fopen(buffer.c_str(), "wt");
 	if (f == nullptr)
 		log_error("Opening %s for writing failed: %s\n", buffer, strerror(errno));
@@ -1167,7 +1179,7 @@ bool read_until_abc_done(abc_output_filter &filt, int fd, DeferredLogs &logs) {
 
 void RunAbcState::run(ConcurrentStack<AbcProcess> &process_pool)
 {
-	std::string buffer = stringf("%s/input.blif", tempdir_name);
+	std::string buffer = stringf("%s/input.blif", per_run_tempdir_name);
 	FILE *f = fopen(buffer.c_str(), "wt");
 	if (f == nullptr) {
 		logs.log("Opening %s for writing failed: %s\n", buffer, strerror(errno));
@@ -1292,13 +1304,13 @@ void RunAbcState::run(ConcurrentStack<AbcProcess> &process_pool)
 			count_gates, GetSize(signal_list), count_input, count_output);
 	if (count_output > 0)
 	{
-		std::string tmp_script_name = stringf("%s/abc.script", tempdir_name);
-		logs.log("Running ABC script: %s\n", replace_tempdir(tmp_script_name, tempdir_name, config.show_tempdir));
+		std::string tmp_script_name = stringf("%s/abc.script", per_run_tempdir_name);
+		logs.log("Running ABC script: %s\n", replace_tempdir(tmp_script_name, config.global_tempdir_name, per_run_tempdir_name, config.show_tempdir));
 
 		errno = 0;
-		abc_output_filter filt(*this, tempdir_name, config.show_tempdir);
+		abc_output_filter filt(*this, config.global_tempdir_name, per_run_tempdir_name, config.show_tempdir);
 #ifdef YOSYS_LINK_ABC
-		string temp_stdouterr_name = stringf("%s/stdouterr.txt", tempdir_name);
+		string temp_stdouterr_name = stringf("%s/stdouterr.txt", per_run_tempdir_name);
 		FILE *temp_stdouterr_w = fopen(temp_stdouterr_name.c_str(), "w");
 		if (temp_stdouterr_w == NULL)
 			log_error("ABC: cannot open a temporary file for output redirection");
@@ -1360,7 +1372,7 @@ void RunAbcState::run(ConcurrentStack<AbcProcess> &process_pool)
 			process_pool.push_back(std::move(process));
 		}
 #else
-		std::string cmd = stringf("\"%s\" -s -f %s/abc.script 2>&1", config.exe_file.c_str(), tempdir_name.c_str());
+		std::string cmd = stringf("\"%s\" -s -f %s/abc.script 2>&1", config.exe_file.c_str(), per_run_tempdir_name.c_str());
 		int ret = run_command(cmd, std::bind(&abc_output_filter::next_line, filt, std::placeholders::_1));
 #endif
 		if (ret != 0) {
@@ -1442,7 +1454,7 @@ void AbcModuleState::extract(AbcSigMap &assign_map, dict<SigSpec, std::string> &
 		return;
 	}
 
-	std::string buffer = stringf("%s/%s", run_abc.tempdir_name, "output.blif");
+	std::string buffer = stringf("%s/%s", run_abc.per_run_tempdir_name, "output.blif");
 	std::ifstream ifs;
 	ifs.open(buffer);
 	if (ifs.fail())
@@ -1797,7 +1809,7 @@ void AbcModuleState::finish()
 	if (run_abc.config.cleanup)
 	{
 		log("Removing temp directory.\n");
-		remove_directory(run_abc.tempdir_name);
+		remove_directory(run_abc.per_run_tempdir_name);
 	}
 	log_pop();
 }
diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc
index 8b61a9299..16df82bb6 100644
--- a/passes/techmap/abc9.cc
+++ b/passes/techmap/abc9.cc
@@ -219,9 +219,7 @@ struct Abc9Pass : public ScriptPass
 		for (argidx = 1; argidx < args.size(); argidx++) {
 			std::string arg = args[argidx];
 			if ((arg == "-exe" || arg == "-script" || arg == "-D" ||
-						/*arg == "-S" ||*/ arg == "-lut" || arg == "-luts" ||
-						/*arg == "-box" ||*/ arg == "-W" || arg == "-genlib" ||
-						arg == "-constr" || arg == "-dont_use" || arg == "-liberty") &&
+						arg == "-lut" || arg == "-luts" || arg == "-W") &&
 					argidx+1 < args.size()) {
 				if (arg == "-lut" || arg == "-luts")
 					lut_mode = true;
diff --git a/techlibs/gowin/Makefile.inc b/techlibs/gowin/Makefile.inc
index df1b79317..0744b1389 100644
--- a/techlibs/gowin/Makefile.inc
+++ b/techlibs/gowin/Makefile.inc
@@ -12,3 +12,4 @@ $(eval $(call add_share_file,share/gowin,techlibs/gowin/brams_map_gw5a.v))
 $(eval $(call add_share_file,share/gowin,techlibs/gowin/brams.txt))
 $(eval $(call add_share_file,share/gowin,techlibs/gowin/lutrams_map.v))
 $(eval $(call add_share_file,share/gowin,techlibs/gowin/lutrams.txt))
+$(eval $(call add_share_file,share/gowin,techlibs/gowin/dsp_map.v))
diff --git a/techlibs/gowin/dsp_map.v b/techlibs/gowin/dsp_map.v
new file mode 100644
index 000000000..f03bcdff0
--- /dev/null
+++ b/techlibs/gowin/dsp_map.v
@@ -0,0 +1,70 @@
+module \$__MUL9X9 (input [8:0] A, input [8:0] B, output [17:0] Y);
+
+    parameter A_WIDTH = 9;
+    parameter B_WIDTH = 9;
+    parameter Y_WIDTH = 18;
+    parameter A_SIGNED = 0;
+    parameter B_SIGNED = 0;
+
+	MULT9X9 __TECHMAP_REPLACE__ (
+		.CLK(1'b0),
+		.CE(1'b0),
+		.RESET(1'b0),
+		.A(A),
+		.SIA({A_WIDTH{1'b0}}),
+		.ASEL(1'b0),
+		.ASIGN(A_SIGNED ? 1'b1 : 1'b0),
+		.B(B),
+		.SIB({B_WIDTH{1'b0}}),
+		.BSEL(1'b0),
+		.BSIGN(B_SIGNED ? 1'b1 : 1'b0),
+		.DOUT(Y)
+	);
+
+endmodule
+
+module \$__MUL18X18 (input [17:0] A, input [17:0] B, output [35:0] Y);
+
+    parameter A_WIDTH = 18;
+    parameter B_WIDTH = 18;
+    parameter Y_WIDTH = 36;
+    parameter A_SIGNED = 0;
+    parameter B_SIGNED = 0;
+
+	MULT18X18 __TECHMAP_REPLACE__ (
+		.CLK(1'b0),
+		.CE(1'b0),
+		.RESET(1'b0),
+		.A(A),
+		.SIA({A_WIDTH{1'b0}}),
+		.ASEL(1'b0),
+		.ASIGN(A_SIGNED ? 1'b1 : 1'b0),
+		.B(B),
+		.SIB({B_WIDTH{1'b0}}),
+		.BSEL(1'b0),
+		.BSIGN(B_SIGNED ? 1'b1 : 1'b0),
+		.DOUT(Y)
+	);
+
+endmodule
+
+module \$__MUL36X36 (input [35:0] A, input [35:0] B, output [71:0] Y);
+
+    parameter A_WIDTH = 36;
+    parameter B_WIDTH = 36;
+    parameter Y_WIDTH = 72;
+    parameter A_SIGNED = 0;
+    parameter B_SIGNED = 0;
+
+	MULT36X36 __TECHMAP_REPLACE__ (
+		.CLK(1'b0),
+		.RESET(1'b0),
+		.CE(1'b0),
+		.A(A),
+		.ASIGN(A_SIGNED ? 1'b1 : 1'b0),
+		.B(B),
+		.BSIGN(B_SIGNED ? 1'b1 : 1'b0),
+		.DOUT(Y)
+	);
+
+endmodule
diff --git a/techlibs/gowin/synth_gowin.cc b/techlibs/gowin/synth_gowin.cc
index b9902659c..cdc7d20f0 100644
--- a/techlibs/gowin/synth_gowin.cc
+++ b/techlibs/gowin/synth_gowin.cc
@@ -29,6 +29,21 @@ struct SynthGowinPass : public ScriptPass
 {
 	SynthGowinPass() : ScriptPass("synth_gowin", "synthesis for Gowin FPGAs") { }
 
+	struct DSPRule {
+		int a_maxwidth;
+		int b_maxwidth;
+		int a_minwidth;
+		int b_minwidth;
+		std::string prim;
+	};
+
+	const std::vector<DSPRule> dsp_rules = {
+		{36, 36, 22, 22, "$__MUL36X36"},
+		{18, 18, 10, 4, "$__MUL18X18"},
+		{18, 18, 4, 10, "$__MUL18X18"},
+		{9, 9, 4, 4, "$__MUL9X9"},
+	};
+
 	void help() override
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
@@ -97,13 +112,16 @@ struct SynthGowinPass : public ScriptPass
 		log("    -setundef\n");
 		log("        set undriven wires and parameters to zero\n");
 		log("\n");
+		log("    -nodsp\n");
+		log("        do not infer DSP multipliers\n");
+		log("\n");
 		log("The following commands are executed by this synthesis command:\n");
 		help_script();
 		log("\n");
 	}
 
 	string top_opt, vout_file, json_file, family;
-	bool retime, nobram, nolutram, flatten, nodffe, strict_gw5a_dffs, nowidelut, abc9, noiopads, noalu, no_rw_check, setundef;
+	bool retime, nobram, nolutram, flatten, nodffe, strict_gw5a_dffs, nowidelut, abc9, noiopads, noalu, no_rw_check, setundef, nodsp;
 
 	void clear_flags() override
 	{
@@ -123,6 +141,7 @@ struct SynthGowinPass : public ScriptPass
 		noalu = false;
 		no_rw_check = false;
 		setundef = false;
+		nodsp = false;
 	}
 
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
@@ -209,6 +228,10 @@ struct SynthGowinPass : public ScriptPass
 				setundef = true;
 				continue;
 			}
+			if (args[argidx] == "-nodsp") {
+				nodsp = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -239,17 +262,40 @@ struct SynthGowinPass : public ScriptPass
 			run(stringf("hierarchy -check %s", help_mode ? "-top <top>" : top_opt));
 		}
 
-		if (flatten && check_label("flatten", "(unless -noflatten)"))
-		{
-			run("proc");
-			run("flatten");
-			run("tribuf -logic");
-			run("deminout");
-		}
-
 		if (check_label("coarse"))
 		{
-			run("synth -run coarse" + no_rw_check_opt);
+			run("proc");
+			if (flatten || help_mode)
+				run("flatten", "(unless -noflatten)");
+			run("tribuf -logic");
+			run("deminout");
+			run("opt_expr");
+			run("opt_clean");
+			run("check");
+			run("opt -nodffe -nosdff");
+			run("fsm");
+			run("opt");
+			run("wreduce");
+			run("peepopt");
+			run("opt_clean");
+			run("share");
+
+			if (help_mode) {
+				run("techmap -map +/mul2dsp.v [...]", "(unless -nodsp and if -family gw1n or gw2a)");
+				run("techmap -map +/gowin/dsp_map.v", "(unless -nodsp and if -family gw1n or gw2a)");
+			} else if (!nodsp && (family == "gw1n" || family == "gw2a")) {
+				for (const auto &rule : dsp_rules) {
+					run(stringf("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=%d -D DSP_B_MAXWIDTH=%d -D DSP_A_MINWIDTH=%d -D DSP_B_MINWIDTH=%d -D DSP_NAME=%s",
+						rule.a_maxwidth, rule.b_maxwidth, rule.a_minwidth, rule.b_minwidth, rule.prim));
+					run("chtype -set $mul t:$__soft_mul");
+				}
+				run("techmap -map +/gowin/dsp_map.v");
+			}
+
+			run("alumacc");
+			run("opt");
+			run("memory -nomap" + no_rw_check_opt);
+			run("opt_clean");
 		}
 
 		if (check_label("map_ram"))
diff --git a/techlibs/xilinx/xilinx_dsp.cc b/techlibs/xilinx/xilinx_dsp.cc
index 22e6bce5b..194b9ac10 100644
--- a/techlibs/xilinx/xilinx_dsp.cc
+++ b/techlibs/xilinx/xilinx_dsp.cc
@@ -263,6 +263,7 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm)
 	log("Analysing %s.%s for Xilinx DSP packing.\n", log_id(pm.module), log_id(st.dsp));
 
 	log_debug("preAdd:     %s\n", log_id(st.preAdd, "--"));
+	log_debug("preSub:     %s\n", log_id(st.preSub, "--"));
 	log_debug("ffAD:       %s\n", log_id(st.ffAD, "--"));
 	log_debug("ffA2:       %s\n", log_id(st.ffA2, "--"));
 	log_debug("ffA1:       %s\n", log_id(st.ffA1, "--"));
@@ -278,17 +279,22 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm)
 
 	Cell *cell = st.dsp;
 
-	if (st.preAdd) {
-		log("  preadder %s (%s)\n", log_id(st.preAdd), log_id(st.preAdd->type));
-		bool A_SIGNED = st.preAdd->getParam(ID::A_SIGNED).as_bool();
-		bool D_SIGNED = st.preAdd->getParam(ID::B_SIGNED).as_bool();
-		if (st.sigA == st.preAdd->getPort(ID::B))
+	if (st.preAdd || st.preSub) {
+		Cell* preAdder = st.preAdd ? st.preAdd : st.preSub;
+
+		log("  preadder %s (%s)\n", log_id(preAdder), log_id(preAdder->type));
+		bool A_SIGNED = preAdder->getParam(ID::A_SIGNED).as_bool();
+		bool D_SIGNED = preAdder->getParam(ID::B_SIGNED).as_bool();
+		if (st.sigA == preAdder->getPort(ID::B))
 			std::swap(A_SIGNED, D_SIGNED);
 		st.sigA.extend_u0(30, A_SIGNED);
 		st.sigD.extend_u0(25, D_SIGNED);
 		cell->setPort(ID::A, st.sigA);
 		cell->setPort(ID::D, st.sigD);
-		cell->setPort(ID(INMODE), Const::from_string("00100"));
+		if (preAdder->type == ID($add))
+			cell->setPort(ID(INMODE), Const::from_string("00100"));
+		else
+			cell->setPort(ID(INMODE), Const::from_string("01100"));
 
 		if (st.ffAD) {
 			if (st.ffAD->type.in(ID($dffe), ID($sdffe))) {
@@ -303,7 +309,7 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm)
 
 		cell->setParam(ID(USE_DPORT), Const("TRUE"));
 
-		pm.autoremove(st.preAdd);
+		pm.autoremove(preAdder);
 	}
 	if (st.postAdd) {
 		log("  postadder %s (%s)\n", log_id(st.postAdd), log_id(st.postAdd->type));
diff --git a/techlibs/xilinx/xilinx_dsp.pmg b/techlibs/xilinx/xilinx_dsp.pmg
index ef0157621..6ec891290 100644
--- a/techlibs/xilinx/xilinx_dsp.pmg
+++ b/techlibs/xilinx/xilinx_dsp.pmg
@@ -6,6 +6,8 @@
 //        If ADREG matched, treat 'A' input as input of ADREG
 //   ( 3) Match the driver of the 'A' and 'D' inputs for a possible $add cell
 //       (pre-adder)
+// 	 (3.1) Match the driver of the 'A' and 'D' inputs for a possible $sub cell
+//         (pre-adder)
 //   ( 4) If pre-adder was present, find match 'A' input for A2REG
 //        If pre-adder was not present, move ADREG to A2REG
 //        If A2REG, then match 'A' input for A1REG
@@ -152,13 +154,41 @@ code sigA sigD
 	}
 endcode
 
+// (3.1) Match the driver of the 'A' and 'D' inputs for a possible $sub cell
+//     (pre-adder)
+match preSub
+	if sigD.empty() || sigD.is_fully_zero()
+	// Ensure that preAdder not already used
+	if param(dsp, \USE_DPORT).decode_string() == "FALSE"
+	if port(dsp, \INMODE, Const(0, 5)).is_fully_zero()
+
+	select preSub->type.in($sub)
+	// Output has to be 25 bits or less
+	select GetSize(port(preSub, \Y)) <= 25
+	select nusers(port(preSub, \Y)) == 2
+	// D port has to be 25 bits or less
+	select GetSize(port(preSub, \A)) <= 25
+	// A port has to be 30 bits or less
+	select GetSize(port(preSub, \B)) <= 30
+	index <SigSpec> port(preSub, \Y) === sigA
+
+	optional
+endmatch
+
+code sigA sigD
+	if (preSub) {
+		sigD = port(preSub, \A);
+		sigA = port(preSub, \B);
+	}
+endcode
+
 // (4) If pre-adder was present, find match 'A' input for A2REG
 //     If pre-adder was not present, move ADREG to A2REG
 //     Then match 'A' input for A1REG
 code argQ ffAD sigA clock ffA2 ffA1
 	// Only search for ffA2 if there was a pre-adder
 	//   (otherwise ffA2 would have been matched as ffAD)
-	if (preAdd) {
+	if (preAdd || preSub) {
 		if (param(dsp, \AREG).as_int() == 0) {
 			argQ = sigA;
 			subpattern(in_dffe);
diff --git a/tests/arch/gowin/mul_gw1n.ys b/tests/arch/gowin/mul_gw1n.ys
new file mode 100644
index 000000000..9b1748255
--- /dev/null
+++ b/tests/arch/gowin/mul_gw1n.ys
@@ -0,0 +1,53 @@
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
+hierarchy -top top
+proc
+# equivalence checking is somewhat slow (and missing simulation models)
+synth_gowin -family gw1n
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT9X9
+
+
+# Make sure that DSPs are not inferred with -nodsp option
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
+hierarchy -top top
+proc
+synth_gowin -family gw1n -nodsp
+cd top # Constrain all select calls below inside the top module
+select -assert-none t:MULT9X9
+
+
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32
+hierarchy -top top
+proc
+synth_gowin -family gw1n
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT18X18
+
+
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64
+hierarchy -top top
+proc
+# equivalence checking is too slow here
+synth_gowin
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT36X36
+
+
+# We end up with two 18x18 multipliers
+# 36x36 min width is 22
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48
+hierarchy -top top
+proc
+# equivalence checking is too slow here
+synth_gowin
+cd top # Constrain all select calls below inside the top module
+select -assert-count 2 t:MULT18X18
diff --git a/tests/arch/gowin/mul_gw2a.ys b/tests/arch/gowin/mul_gw2a.ys
new file mode 100644
index 000000000..895c580b7
--- /dev/null
+++ b/tests/arch/gowin/mul_gw2a.ys
@@ -0,0 +1,53 @@
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
+hierarchy -top top
+proc
+# equivalence checking is somewhat slow (and missing simulation models)
+synth_gowin -family gw2a
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT9X9
+
+
+# Make sure that DSPs are not inferred with -nodsp option
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
+hierarchy -top top
+proc
+synth_gowin -family gw2a -nodsp
+cd top # Constrain all select calls below inside the top module
+select -assert-none t:MULT9X9
+
+
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32
+hierarchy -top top
+proc
+synth_gowin -family gw2a
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT18X18
+
+
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64
+hierarchy -top top
+proc
+# equivalence checking is too slow here
+synth_gowin -family gw2a
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:MULT36X36
+
+
+# We end up with two 18x18 multipliers
+# 36x36 min width is 22
+design -reset
+read_verilog ../common/mul.v
+chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48
+hierarchy -top top
+proc
+# equivalence checking is too slow here
+synth_gowin -family gw2a
+cd top # Constrain all select calls below inside the top module
+select -assert-count 2 t:MULT18X18
diff --git a/tests/arch/xilinx/dsp_preadder_sub.ys b/tests/arch/xilinx/dsp_preadder_sub.ys
new file mode 100644
index 000000000..0e23ac373
--- /dev/null
+++ b/tests/arch/xilinx/dsp_preadder_sub.ys
@@ -0,0 +1,29 @@
+read_verilog <<EOT
+module top(
+	input  signed [7:0] A,
+	input  signed [7:0] D,
+	input  signed [7:0] B,
+	output signed [16:0] P
+);
+	assign P = (A - D) * B;
+endmodule
+EOT
+
+proc
+design -save gold
+synth_xilinx -noiopad
+design -save gate
+cd top
+select -assert-count 1 t:DSP48E1
+select -assert-count 1 t:DSP48E1 r:USE_DPORT=TRUE %i
+select -assert-none t:DSP48E1 %% t:* %D
+
+# Now prove functional equivalence of the mapped netlist against the original
+# (saved as `gold` above).
+design -reset
+design -copy-from gold -as gold top
+design -copy-from gate -as gate top
+techmap -wb -D EQUIV -autoproc -map +/xilinx/cells_sim.v
+equiv_make gold gate equiv
+equiv_induct equiv
+equiv_status -assert equiv
diff --git a/tests/techmap/abc_temp_dir_sanitization.ys b/tests/techmap/abc_temp_dir_sanitization.ys
new file mode 100644
index 000000000..ed87ff980
--- /dev/null
+++ b/tests/techmap/abc_temp_dir_sanitization.ys
@@ -0,0 +1,13 @@
+read_verilog <<EOT
+module simple(I1, I2, O);
+	input wire I1;
+	input wire I2;
+	output wire O;
+
+	assign O = I1 | I2;
+endmodule
+EOT
+techmap
+
+logger -warn " /tmp/" -werror " /tmp/"
+abc -g all
diff --git a/tests/various/.gitignore b/tests/various/.gitignore
index c2d13b8ee..1425c2063 100644
--- a/tests/various/.gitignore
+++ b/tests/various/.gitignore
@@ -7,6 +7,8 @@
 /plugin.so
 /plugin_search
 /plugin.so.dSYM
+/ezcmdline_plugin.so
+/ezcmdline_plugin.so.dSYM
 /temp
 /smtlib2_module.smt2
 /smtlib2_module-filtered.smt2
diff --git a/tests/various/ezcmdline_dummy_solver b/tests/various/ezcmdline_dummy_solver
new file mode 100755
index 000000000..db5b21b8e
--- /dev/null
+++ b/tests/various/ezcmdline_dummy_solver
@@ -0,0 +1,61 @@
+#!/bin/sh
+# Dummy SAT solver for ezCmdlineSAT tests.
+# Accepts exactly two CNF shapes:
+#  - SAT:   p cnf 1 1; clause: "1 0"  -> exits 10 with v 1
+#  - UNSAT: p cnf 1 2; clauses: "1 0" and "-1 0" -> exits 20
+set -e
+
+if [ "$#" -ne 1 ]; then
+	echo "usage: $0 <cnf>" >&2
+	exit 1
+fi
+
+awk '
+BEGIN {
+	vars = 0;
+	clauses = 0;
+	clause_count = 0;
+	clause_data = "";
+	current = "";
+}
+$1 == "c" {
+	next;
+}
+$1 == "p" && $2 == "cnf" {
+	vars = $3;
+	clauses = $4;
+	next;
+}
+{
+	for (i = 1; i <= NF; i++) {
+		lit = $i;
+		if (lit == 0) {
+			clause_count++;
+			if (clause_data != "")
+				clause_data = clause_data ";" current;
+			else
+				clause_data = current;
+			current = "";
+		} else {
+			if (current == "")
+				current = lit;
+			else
+				current = current "," lit;
+		}
+	}
+}
+END {
+	if (vars == 1 && clause_count == 1 && clause_data == "1") {
+		print "s SATISFIABLE";
+		print "v 1 0";
+		exit 10;
+	}
+	if (vars == 1 && clause_count == 2 && clause_data == "1;-1") {
+		print "s UNSATISFIABLE";
+		exit 20;
+	}
+	print "c unexpected CNF for dummy solver";
+	print "c vars=" vars " header_clauses=" clauses " parsed_clauses=" clause_count " data=" clause_data;
+	exit 1;
+}
+' "$1"
diff --git a/tests/various/ezcmdline_plugin.cc b/tests/various/ezcmdline_plugin.cc
new file mode 100644
index 000000000..b775829b3
--- /dev/null
+++ b/tests/various/ezcmdline_plugin.cc
@@ -0,0 +1,53 @@
+#include "kernel/yosys.h"
+#include "libs/ezsat/ezcmdline.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct EzCmdlineTestPass : public Pass {
+	EzCmdlineTestPass() : Pass("ezcmdline_test", "smoke-test ezCmdlineSAT") { }
+	void execute(std::vector<std::string> args, RTLIL::Design *design) override
+	{
+		std::string cmd;
+		size_t argidx = 1;
+
+		while (argidx < args.size()) {
+			if (args[argidx] == "-cmd" && argidx + 1 < args.size()) {
+				cmd = args[argidx + 1];
+				argidx += 2;
+				continue;
+			}
+			break;
+		}
+
+		extra_args(args, argidx, design);
+
+		if (cmd.empty())
+			log_error("Missing -cmd <solver> argument.\n");
+
+		ezCmdlineSAT sat(cmd);
+		sat.non_incremental();
+
+		// assume("A") adds a permanent CNF clause "A".
+		sat.assume(sat.VAR("A"));
+
+		std::vector<int> model_expressions;
+		std::vector<bool> model_values;
+		model_expressions.push_back(sat.VAR("A"));
+
+		// Expect SAT with A=true.
+		if (!sat.solve(model_expressions, model_values))
+			log_error("ezCmdlineSAT SAT case failed.\n");
+		if (model_values.size() != 1 || !model_values[0])
+			log_error("ezCmdlineSAT SAT model mismatch.\n");
+
+		// Passing NOT("A") here adds a temporary unit clause for this solve call,
+		// so the solver sees A && !A and must return UNSAT.
+		if (sat.solve(model_expressions, model_values, sat.NOT("A")))
+			log_error("ezCmdlineSAT UNSAT case failed.\n");
+
+		log("ezcmdline_test passed!\n");
+	}
+} EzCmdlineTestPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/tests/various/ezcmdline_plugin.sh b/tests/various/ezcmdline_plugin.sh
new file mode 100644
index 000000000..cad0475a8
--- /dev/null
+++ b/tests/various/ezcmdline_plugin.sh
@@ -0,0 +1,12 @@
+set -e
+
+DIR=$(cd "$(dirname "$0")" && pwd)
+BASEDIR=$(cd "$DIR/../.." && pwd)
+rm -f "$DIR/ezcmdline_plugin.so"
+chmod +x "$DIR/ezcmdline_dummy_solver"
+CXXFLAGS=$("$BASEDIR/yosys-config" --cxxflags)
+DATDIR=$("$BASEDIR/yosys-config" --datdir)
+DATDIR=${DATDIR//\//\\\/}
+CXXFLAGS=${CXXFLAGS//$DATDIR/..\/..\/share}
+"$BASEDIR/yosys-config" --exec --cxx ${CXXFLAGS} -I"$BASEDIR" --ldflags -shared -o "$DIR/ezcmdline_plugin.so" "$DIR/ezcmdline_plugin.cc"
+"$BASEDIR/yosys" -m "$DIR/ezcmdline_plugin.so" -p "ezcmdline_test -cmd $DIR/ezcmdline_dummy_solver" | grep -q "ezcmdline_test passed!"
diff --git a/tests/various/json_param_defaults.v b/tests/various/json_param_defaults.v
new file mode 100644
index 000000000..7d3b94a68
--- /dev/null
+++ b/tests/various/json_param_defaults.v
@@ -0,0 +1,10 @@
+module json_param_defaults #(
+	parameter WIDTH = 8,
+	parameter SIGNED = 1
+) (
+	input  [WIDTH-1:0] a,
+	output [WIDTH-1:0] y
+);
+	wire [WIDTH-1:0] y_int = a << SIGNED;
+	assign y = y_int;
+endmodule
diff --git a/tests/various/json_param_defaults.ys b/tests/various/json_param_defaults.ys
new file mode 100644
index 000000000..45e312de2
--- /dev/null
+++ b/tests/various/json_param_defaults.ys
@@ -0,0 +1,8 @@
+! mkdir -p temp
+read_verilog -sv json_param_defaults.v
+write_json temp/json_param_defaults.json
+design -reset
+read_json temp/json_param_defaults.json
+write_verilog -noattr -defaultparams temp/json_param_defaults.v
+! grep -qF "parameter WIDTH = 32'd8" temp/json_param_defaults.v
+! grep -qF "parameter SIGNED = 32'd1" temp/json_param_defaults.v