Merge branch 'master' into struct

11 files changed, 310 insertions, 142 deletions

diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 1fb7210cb..6b910eecd 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -76,9 +76,11 @@ void aiger_encode(std::ostream &f, int x)
 
 struct XAigerWriter
 {
+	Design *design;
 	Module *module;
 	SigMap sigmap;
 
+	dict<SigBit, State> init_map;
 	pool<SigBit> input_bits, output_bits;
 	dict<SigBit, SigBit> not_map, alias_map;
 	dict<SigBit, pair<SigBit, SigBit>> and_map;
@@ -137,7 +139,7 @@ struct XAigerWriter
 		return a;
 	}
 
-	XAigerWriter(Module *module, bool holes_mode=false) : module(module), sigmap(module)
+	XAigerWriter(Module *module, bool dff_mode) : design(module->design), module(module), sigmap(module)
 	{
 		pool<SigBit> undriven_bits;
 		pool<SigBit> unused_bits;
@@ -157,7 +159,8 @@ struct XAigerWriter
 			if (wire->get_bool_attribute(ID::keep))
 				sigmap.add(wire);
 
-		for (auto wire : module->wires())
+		for (auto wire : module->wires()) {
+			auto it = wire->attributes.find(ID::init);
 			for (int i = 0; i < GetSize(wire); i++)
 			{
 				SigBit wirebit(wire, i);
@@ -174,17 +177,27 @@ struct XAigerWriter
 				undriven_bits.insert(bit);
 				unused_bits.insert(bit);
 
-				bool scc = wire->attributes.count(ID::abc9_scc);
-				if (wire->port_input || scc)
+				bool keep = wire->get_bool_attribute(ID::abc9_keep);
+				if (wire->port_input || keep)
 					input_bits.insert(bit);
 
-				bool keep = wire->get_bool_attribute(ID::keep);
-				if (wire->port_output || keep || scc) {
+				keep = keep || wire->get_bool_attribute(ID::keep);
+				if (wire->port_output || keep) {
 					if (bit != wirebit)
 						alias_map[wirebit] = bit;
 					output_bits.insert(wirebit);
 				}
+
+				if (it != wire->attributes.end()) {
+					auto s = it->second[i];
+					if (s != State::Sx) {
+						auto r = init_map.insert(std::make_pair(bit, it->second[i]));
+						if (!r.second && r.first->second != it->second[i])
+							log_error("Bit '%s' has a conflicting (* init *) value.\n", log_signal(bit));
+					}
+				}
 			}
+		}
 
 		TimingInfo timing;
 
@@ -212,10 +225,7 @@ struct XAigerWriter
 					continue;
 				}
 
-				if (cell->type == ID($__ABC9_FF_) &&
-						// The presence of an abc9_mergeability attribute indicates
-						//   that we do want to pass this flop to ABC
-						cell->attributes.count(ID::abc9_mergeability))
+				if (dff_mode && cell->type.in(ID($_DFF_N_), ID($_DFF_P_)) && !cell->get_bool_attribute(ID::abc9_keep))
 				{
 					SigBit D = sigmap(cell->getPort(ID::D).as_bit());
 					SigBit Q = sigmap(cell->getPort(ID::Q).as_bit());
@@ -231,31 +241,29 @@ struct XAigerWriter
 					continue;
 			}
 
-			RTLIL::Module* inst_module = module->design->module(cell->type);
-			if (inst_module) {
-				IdString derived_type = inst_module->derive(module->design, cell->parameters);
-				inst_module = module->design->module(derived_type);
-				log_assert(inst_module);
-
+			RTLIL::Module* inst_module = design->module(cell->type);
+			if (inst_module && inst_module->get_blackbox_attribute()) {
 				bool abc9_flop = false;
-				if (!cell->has_keep_attr()) {
-					auto it = cell->attributes.find(ID::abc9_box_seq);
-					if (it != cell->attributes.end()) {
-						int abc9_box_seq = it->second.as_int();
-						if (GetSize(box_list) <= abc9_box_seq)
-							box_list.resize(abc9_box_seq+1);
-						box_list[abc9_box_seq] = cell;
-						// Only flop boxes may have arrival times
-						//   (all others are combinatorial)
-						abc9_flop = inst_module->get_bool_attribute(ID::abc9_flop);
-						if (!abc9_flop)
-							continue;
-					}
+
+				auto it = cell->attributes.find(ID::abc9_box_seq);
+				if (it != cell->attributes.end()) {
+					log_assert(!cell->has_keep_attr());
+					log_assert(cell->parameters.empty());
+					int abc9_box_seq = it->second.as_int();
+					if (GetSize(box_list) <= abc9_box_seq)
+						box_list.resize(abc9_box_seq+1);
+					box_list[abc9_box_seq] = cell;
+					// Only flop boxes may have arrival times
+					//   (all others are combinatorial)
+					log_assert(cell->parameters.empty());
+					abc9_flop = inst_module->get_bool_attribute(ID::abc9_flop);
+					if (!abc9_flop)
+						continue;
 				}
 
-				if (!timing.count(derived_type))
+				if (!timing.count(inst_module->name))
 					timing.setup_module(inst_module);
-				auto &t = timing.at(derived_type).arrival;
+				auto &t = timing.at(inst_module->name).arrival;
 				for (const auto &conn : cell->connections()) {
 					auto port_wire = inst_module->wire(conn.first);
 					if (!port_wire->port_output)
@@ -269,7 +277,7 @@ struct XAigerWriter
 #ifndef NDEBUG
 						if (ys_debug(1)) {
 							static std::set<std::tuple<IdString,IdString,int>> seen;
-							if (seen.emplace(derived_type, conn.first, i).second) log("%s.%s[%d] abc9_arrival = %d\n",
+							if (seen.emplace(inst_module->name, conn.first, i).second) log("%s.%s[%d] abc9_arrival = %d\n",
 									log_id(cell->type), log_id(conn.first), i, d);
 						}
 #endif
@@ -280,10 +288,6 @@ struct XAigerWriter
 				if (abc9_flop)
 					continue;
 			}
-			else {
-				if (cell->type == ID($__ABC9_DELAY))
-					log_error("Cell type '%s' not recognised. Check that '+/abc9_model.v' has been read.\n", cell->type.c_str());
-			}
 
 			bool cell_known = inst_module || cell->known();
 			for (const auto &c : cell->connections()) {
@@ -317,9 +321,9 @@ struct XAigerWriter
 		for (auto cell : box_list) {
 			log_assert(cell);
 
-			RTLIL::Module* box_module = module->design->module(cell->type);
+			RTLIL::Module* box_module = design->module(cell->type);
 			log_assert(box_module);
-			log_assert(box_module->attributes.count(ID::abc9_box_id) || box_module->get_bool_attribute(ID::abc9_flop));
+			log_assert(box_module->has_attribute(ID::abc9_box_id));
 
 			auto r = box_ports.insert(cell->type);
 			if (r.second) {
@@ -383,27 +387,6 @@ struct XAigerWriter
 						undriven_bits.erase(O);
 					}
 			}
-
-			// Connect <cell>.abc9_ff.Q (inserted by abc9_map.v) as the last input to the flop box
-			if (box_module->get_bool_attribute(ID::abc9_flop)) {
-				SigSpec rhs = module->wire(stringf("%s.abc9_ff.Q", cell->name.c_str()));
-				if (rhs.empty())
-					log_error("'%s.abc9_ff.Q' is not a wire present in module '%s'.\n", log_id(cell), log_id(module));
-
-				for (auto b : rhs) {
-					SigBit I = sigmap(b);
-					if (b == RTLIL::Sx)
-						b = State::S0;
-					else if (I != b) {
-						if (I == RTLIL::Sx)
-							alias_map[b] = State::S0;
-						else
-							alias_map[b] = I;
-					}
-					co_bits.emplace_back(b);
-					unused_bits.erase(I);
-				}
-			}
 		}
 
 		for (auto bit : input_bits)
@@ -419,16 +402,14 @@ struct XAigerWriter
 			undriven_bits.erase(bit);
 		}
 
-		if (holes_mode) {
-			struct sort_by_port_id {
-				bool operator()(const RTLIL::SigBit& a, const RTLIL::SigBit& b) const {
-					return a.wire->port_id < b.wire->port_id ||
-					    (a.wire->port_id == b.wire->port_id && a.offset < b.offset);
-				}
-			};
-			input_bits.sort(sort_by_port_id());
-			output_bits.sort(sort_by_port_id());
-		}
+		struct sort_by_port_id {
+			bool operator()(const RTLIL::SigBit& a, const RTLIL::SigBit& b) const {
+				return a.wire->port_id < b.wire->port_id ||
+				    (a.wire->port_id == b.wire->port_id && a.offset < b.offset);
+			}
+		};
+		input_bits.sort(sort_by_port_id());
+		output_bits.sort(sort_by_port_id());
 
 		aig_map[State::S0] = 0;
 		aig_map[State::S1] = 1;
@@ -589,17 +570,14 @@ struct XAigerWriter
 			int box_count = 0;
 			for (auto cell : box_list) {
 				log_assert(cell);
+				log_assert(cell->parameters.empty());
 
-				RTLIL::Module* box_module = module->design->module(cell->type);
-				log_assert(box_module);
-
-				IdString derived_type = box_module->derive(box_module->design, cell->parameters);
-				box_module = box_module->design->module(derived_type);
-				log_assert(box_module);
-
-				auto r = cell_cache.insert(derived_type);
+				auto r = cell_cache.insert(cell->type);
 				auto &v = r.first->second;
 				if (r.second) {
+					RTLIL::Module* box_module = design->module(cell->type);
+					log_assert(box_module);
+
 					int box_inputs = 0, box_outputs = 0;
 					for (auto port_name : box_module->ports) {
 						RTLIL::Wire *w = box_module->wire(port_name);
@@ -610,11 +588,6 @@ struct XAigerWriter
 							box_outputs += GetSize(w);
 					}
 
-					// For flops only, create an extra 1-bit input that drives a new wire
-					//   called "<cell>.abc9_ff.Q" that is used below
-					if (box_module->get_bool_attribute(ID::abc9_flop))
-						box_inputs++;
-
 					std::get<0>(v) = box_inputs;
 					std::get<1>(v) = box_outputs;
 					std::get<2>(v) = box_module->attributes.at(ID::abc9_box_id).as_int();
@@ -635,23 +608,27 @@ struct XAigerWriter
 			auto write_s_buffer = std::bind(write_buffer, std::ref(s_buffer), std::placeholders::_1);
 			write_s_buffer(ff_bits.size());
 
+			dict<SigSpec, int> clk_to_mergeability;
 			for (const auto &i : ff_bits) {
 				const SigBit &d = i.first;
 				const Cell *cell = i.second;
 
-				int mergeability = cell->attributes.at(ID::abc9_mergeability).as_int();
+				SigSpec clk_and_pol{sigmap(cell->getPort(ID::C)), cell->type[6] == 'P' ? State::S1 : State::S0};
+				auto r = clk_to_mergeability.insert(std::make_pair(clk_and_pol, clk_to_mergeability.size()+1));
+				int mergeability = r.first->second;
 				log_assert(mergeability > 0);
 				write_r_buffer(mergeability);
 
-				Const init = cell->attributes.at(ID::abc9_init, State::Sx);
-				log_assert(GetSize(init) == 1);
+				SigBit Q = sigmap(cell->getPort(ID::Q));
+				State init = init_map.at(Q, State::Sx);
+				log_debug("Cell '%s' (type %s) has (* init *) value '%s'.\n", log_id(cell), log_id(cell->type), log_signal(init));
 				if (init == State::S1)
 					write_s_buffer(1);
 				else if (init == State::S0)
 					write_s_buffer(0);
 				else {
 					log_assert(init == State::Sx);
-					write_s_buffer(0);
+					write_s_buffer(2);
 				}
 
 				// Use arrival time from output of flop box
@@ -671,10 +648,16 @@ struct XAigerWriter
 			f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
 			f.write(buffer_str.data(), buffer_str.size());
 
-			RTLIL::Module *holes_module = module->design->module(stringf("%s$holes", module->name.c_str()));
+			RTLIL::Design *holes_design;
+			auto it = saved_designs.find("$abc9_holes");
+			if (it != saved_designs.end())
+				holes_design = it->second;
+			else
+				holes_design = nullptr;
+			RTLIL::Module *holes_module = holes_design ? holes_design->module(module->name) : nullptr;
 			if (holes_module) {
 				std::stringstream a_buffer;
-				XAigerWriter writer(holes_module, true /* holes_mode */);
+				XAigerWriter writer(holes_module, false /* dff_mode */);
 				writer.write_aiger(a_buffer, false /*ascii_mode*/);
 
 				f << "a";
@@ -704,10 +687,10 @@ struct XAigerWriter
 
 		f << stringf("Generated by %s\n", yosys_version_str);
 
-		module->design->scratchpad_set_int("write_xaiger.num_ands", and_map.size());
-		module->design->scratchpad_set_int("write_xaiger.num_wires", aig_map.size());
-		module->design->scratchpad_set_int("write_xaiger.num_inputs", input_bits.size());
-		module->design->scratchpad_set_int("write_xaiger.num_outputs", output_bits.size());
+		design->scratchpad_set_int("write_xaiger.num_ands", and_map.size());
+		design->scratchpad_set_int("write_xaiger.num_wires", aig_map.size());
+		design->scratchpad_set_int("write_xaiger.num_inputs", input_bits.size());
+		design->scratchpad_set_int("write_xaiger.num_outputs", output_bits.size());
 	}
 
 	void write_map(std::ostream &f)
@@ -761,10 +744,10 @@ struct XAigerBackend : public Backend {
 		log("    write_xaiger [options] [filename]\n");
 		log("\n");
 		log("Write the top module (according to the (* top *) attribute or if only one module\n");
-		log("is currently selected) to an XAIGER file. Any non $_NOT_, $_AND_, $_ABC9_FF_, or");
-		log("non (* abc9_box_id *) cells will be converted into psuedo-inputs and\n");
-		log("pseudo-outputs. Whitebox contents will be taken from the '<module-name>$holes'\n");
-		log("module, if it exists.\n");
+		log("is currently selected) to an XAIGER file. Any non $_NOT_, $_AND_, (optionally\n");
+		log("$_DFF_N_, $_DFF_P_), or non (* abc9_box *) cells will be converted into psuedo-\n");
+		log("inputs and pseudo-outputs. Whitebox contents will be taken from the equivalent\n");
+		log("module in the '$abc9_holes' design, if it exists.\n");
 		log("\n");
 		log("    -ascii\n");
 		log("        write ASCII version of AIGER format\n");
@@ -772,10 +755,13 @@ struct XAigerBackend : public Backend {
 		log("    -map <filename>\n");
 		log("        write an extra file with port and box symbols\n");
 		log("\n");
+		log("    -dff\n");
+		log("        write $_DFF_[NP]_ cells\n");
+		log("\n");
 	}
 	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
-		bool ascii_mode = false;
+		bool ascii_mode = false, dff_mode = false;
 		std::string map_filename;
 
 		log_header(design, "Executing XAIGER backend.\n");
@@ -791,6 +777,10 @@ struct XAigerBackend : public Backend {
 				map_filename = args[++argidx];
 				continue;
 			}
+			if (args[argidx] == "-dff") {
+				dff_mode = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(f, filename, args, argidx, !ascii_mode);
@@ -808,7 +798,7 @@ struct XAigerBackend : public Backend {
 		if (!top_module->memories.empty())
 			log_error("Found unmapped memories in module %s: unmapped memories are not supported in XAIGER backend!\n", log_id(top_module));
 
-		XAigerWriter writer(top_module);
+		XAigerWriter writer(top_module, dff_mode);
 		writer.write_aiger(*f, ascii_mode);
 
 		if (!map_filename.empty()) {
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 14c8484e8..2816d3246 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -266,20 +266,26 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in(ID($div), ID($mod)))
+		if (cell->type.in(ID($div), ID($mod), ID($modfloor)))
 		{
+			bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
+			bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
+
 			string btor_op;
 			if (cell->type == ID($div)) btor_op = "div";
+			// "rem" = truncating modulo
 			if (cell->type == ID($mod)) btor_op = "rem";
+			// "mod" = flooring modulo
+			if (cell->type == ID($modfloor)) {
+				// "umod" doesn't exist because it's the same as "urem"
+				btor_op = a_signed || b_signed ? "mod" : "rem";
+			}
 			log_assert(!btor_op.empty());
 
 			int width = GetSize(cell->getPort(ID::Y));
 			width = std::max(width, GetSize(cell->getPort(ID::A)));
 			width = std::max(width, GetSize(cell->getPort(ID::B)));
 
-			bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
-			bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
-
 			int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
 			int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
 
diff --git a/backends/btor/test_cells.sh b/backends/btor/test_cells.sh
index e0f1a0514..3f077201a 100644
--- a/backends/btor/test_cells.sh
+++ b/backends/btor/test_cells.sh
@@ -6,7 +6,7 @@ rm -rf test_cells.tmp
 mkdir -p test_cells.tmp
 cd test_cells.tmp
 
-../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod'
+../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor'
 
 for fn in test_*.il; do
 	../../../yosys -p "
diff --git a/backends/cxxrtl/cxxrtl.cc b/backends/cxxrtl/cxxrtl.cc
index f3ed3f623..0cceecbba 100644
--- a/backends/cxxrtl/cxxrtl.cc
+++ b/backends/cxxrtl/cxxrtl.cc
@@ -513,7 +513,6 @@ struct CxxrtlWorker {
 	bool elide_public = false;
 	bool localize_internal = false;
 	bool localize_public = false;
-	bool run_opt_clean_purge = false;
 	bool run_proc_flatten = false;
 	bool max_opt_level = false;
 
@@ -2009,6 +2008,7 @@ struct CxxrtlWorker {
 				log("Module `%s' contains feedback arcs through wires:\n", log_id(module));
 				for (auto wire : feedback_wires)
 					log("  %s\n", log_id(wire));
+				log("\n");
 			}
 
 			for (auto wire : module->wires()) {
@@ -2040,20 +2040,20 @@ struct CxxrtlWorker {
 				log("Module `%s' contains buffered combinatorial wires:\n", log_id(module));
 				for (auto wire : buffered_wires)
 					log("  %s\n", log_id(wire));
+				log("\n");
 			}
 
 			eval_converges[module] = feedback_wires.empty() && buffered_wires.empty();
 		}
 		if (has_feedback_arcs || has_buffered_wires) {
 			// Although both non-feedback buffered combinatorial wires and apparent feedback wires may be eliminated
-			// by optimizing the design, if after `opt_clean -purge` there are any feedback wires remaining, it is very
+			// by optimizing the design, if after `proc; flatten` there are any feedback wires remaining, it is very
 			// likely that these feedback wires are indicative of a true logic loop, so they get emphasized in the message.
 			const char *why_pessimistic = nullptr;
 			if (has_feedback_arcs)
 				why_pessimistic = "feedback wires";
 			else if (has_buffered_wires)
 				why_pessimistic = "buffered combinatorial wires";
-			log("\n");
 			log_warning("Design contains %s, which require delta cycles during evaluation.\n", why_pessimistic);
 			if (!max_opt_level)
 				log("Increasing the optimization level may eliminate %s from the design.\n", why_pessimistic);
@@ -2087,34 +2087,39 @@ struct CxxrtlWorker {
 
 	void prepare_design(RTLIL::Design *design)
 	{
+		bool did_anything = false;
 		bool has_sync_init, has_packed_mem;
 		log_push();
 		check_design(design, has_sync_init, has_packed_mem);
 		if (run_proc_flatten) {
 			Pass::call(design, "proc");
 			Pass::call(design, "flatten");
+			did_anything = true;
 		} else if (has_sync_init) {
 			// We're only interested in proc_init, but it depends on proc_prune and proc_clean, so call those
 			// in case they weren't already. (This allows `yosys foo.v -o foo.cc` to work.)
 			Pass::call(design, "proc_prune");
 			Pass::call(design, "proc_clean");
 			Pass::call(design, "proc_init");
+			did_anything = true;
 		}
-		if (has_packed_mem)
+		if (has_packed_mem) {
 			Pass::call(design, "memory_unpack");
+			did_anything = true;
+		}
 		// Recheck the design if it was modified.
 		if (has_sync_init || has_packed_mem)
 			check_design(design, has_sync_init, has_packed_mem);
 		log_assert(!(has_sync_init || has_packed_mem));
-		if (run_opt_clean_purge)
-			Pass::call(design, "opt_clean -purge");
 		log_pop();
+		if (did_anything)
+			log_spacer();
 		analyze_design(design);
 	}
 };
 
 struct CxxrtlBackend : public Backend {
-	static const int DEFAULT_OPT_LEVEL = 6;
+	static const int DEFAULT_OPT_LEVEL = 5;
 
 	CxxrtlBackend() : Backend("cxxrtl", "convert design to C++ RTL simulation") { }
 	void help() YS_OVERRIDE
@@ -2306,10 +2311,7 @@ struct CxxrtlBackend : public Backend {
 		log("        like -O3, and localize public wires not marked (*keep*) if possible.\n");
 		log("\n");
 		log("    -O5\n");
-		log("        like -O4, and run `opt_clean -purge` first.\n");
-		log("\n");
-		log("    -O6\n");
-		log("        like -O5, and run `proc; flatten` first.\n");
+		log("        like -O4, and run `proc; flatten` first.\n");
 		log("\n");
 	}
 	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
@@ -2343,13 +2345,11 @@ struct CxxrtlBackend : public Backend {
 		extra_args(f, filename, args, argidx);
 
 		switch (opt_level) {
-			case 6:
+			// the highest level here must match DEFAULT_OPT_LEVEL
+			case 5:
 				worker.max_opt_level = true;
 				worker.run_proc_flatten = true;
 				YS_FALLTHROUGH
-			case 5:
-				worker.run_opt_clean_purge = true;
-				YS_FALLTHROUGH
 			case 4:
 				worker.localize_public = true;
 				YS_FALLTHROUGH
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index f6dae1d8c..b1d8500bb 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -392,7 +392,34 @@ struct FirrtlWorker
 		return result;
 	}
 
-	void run()
+	void emit_extmodule()
+	{
+		std::string moduleFileinfo = getFileinfo(module);
+		f << stringf("  extmodule %s: %s\n", make_id(module->name), moduleFileinfo.c_str());
+		vector<std::string> port_decls;
+
+		for (auto wire : module->wires())
+		{
+			const auto wireName = make_id(wire->name);
+			std::string wireFileinfo = getFileinfo(wire);
+
+			if (wire->port_input && wire->port_output)
+			{
+				log_error("Module port %s.%s is inout!\n", log_id(module), log_id(wire));
+			}
+			port_decls.push_back(stringf("    %s %s: UInt<%d> %s\n", wire->port_input ? "input" : "output",
+					wireName, wire->width, wireFileinfo.c_str()));
+		}
+
+		for (auto &str : port_decls)
+		{
+			f << str;
+		}
+
+		f << stringf("\n");
+	}
+
+	void emit_module()
 	{
 		std::string moduleFileinfo = getFileinfo(module);
 		f << stringf("  module %s: %s\n", make_id(module->name), moduleFileinfo.c_str());
@@ -446,7 +473,7 @@ struct FirrtlWorker
 			string y_id = make_id(cell->name);
 			std::string cellFileinfo = getFileinfo(cell);
 
-			if (cell->type.in(ID($not), ID($logic_not), ID($neg), ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_bool), ID($reduce_xnor)))
+			if (cell->type.in(ID($not), ID($logic_not), ID($_NOT_), ID($neg), ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_bool), ID($reduce_xnor)))
 			{
 				string a_expr = make_expr(cell->getPort(ID::A));
 				wire_decls.push_back(stringf("    wire %s: UInt<%d> %s\n", y_id.c_str(), y_width, cellFileinfo.c_str()));
@@ -462,7 +489,7 @@ struct FirrtlWorker
 
 				// Assume the FIRRTL width is a single bit.
 				firrtl_width = 1;
-				if (cell->type == ID($not)) primop = "not";
+				if (cell->type.in(ID($not), ID($_NOT_))) primop = "not";
 				else if (cell->type == ID($neg)) {
 					primop = "neg";
 					firrtl_is_signed = true;	// Result of "neg" is signed (an SInt).
@@ -494,7 +521,7 @@ struct FirrtlWorker
 
 				continue;
 			}
-			if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($xnor), ID($and), ID($or), ID($eq), ID($eqx),
+			if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($_XOR_), ID($xnor), ID($and), ID($_AND_), ID($or), ID($_OR_), ID($eq), ID($eqx),
                                         ID($gt), ID($ge), ID($lt), ID($le), ID($ne), ID($nex), ID($shr), ID($sshr), ID($sshl), ID($shl),
                                         ID($logic_and), ID($logic_or), ID($pow)))
 			{
@@ -524,7 +551,7 @@ struct FirrtlWorker
 
 				// For the arithmetic ops, expand operand widths to result widths befor performing the operation.
 				// This corresponds (according to iverilog) to what verilog compilers implement.
-				if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($xnor), ID($and), ID($or)))
+				if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($_XOR_), ID($xnor), ID($and), ID($_AND_), ID($or), ID($_OR_)))
 				{
 					if (a_width < y_width) {
 						a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
@@ -558,19 +585,20 @@ struct FirrtlWorker
 					firrtl_is_signed = a_signed | b_signed;
 					firrtl_width = a_width;
 				} else if (cell->type == ID($mod)) {
+					// "rem" = truncating modulo
 					primop = "rem";
 					firrtl_width = min(a_width, b_width);
-				} else if (cell->type == ID($and)) {
+				} else if (cell->type.in(ID($and), ID($_AND_))) {
 					primop = "and";
 					always_uint = true;
 					firrtl_width = max(a_width, b_width);
 				}
-				else if (cell->type == ID($or) ) {
+				else if (cell->type.in(ID($or), ID($_OR_))) {
 					primop =  "or";
 					always_uint = true;
 					firrtl_width = max(a_width, b_width);
 				}
-				else if (cell->type == ID($xor)) {
+				else if (cell->type.in(ID($xor), ID($_XOR_))) {
 					primop = "xor";
 					always_uint = true;
 					firrtl_width = max(a_width, b_width);
@@ -694,7 +722,8 @@ struct FirrtlWorker
 					}
 				}
 
-				if (!cell->parameters.at(ID::B_SIGNED).as_bool()) {
+				auto it = cell->parameters.find(ID::B_SIGNED);
+				if (it == cell->parameters.end() || !it->second.as_bool()) {
 					b_expr = "asUInt(" + b_expr + ")";
 				}
 
@@ -723,9 +752,10 @@ struct FirrtlWorker
 				continue;
 			}
 
-			if (cell->type.in(ID($mux)))
+			if (cell->type.in(ID($mux), ID($_MUX_)))
 			{
-				int width = cell->parameters.at(ID::WIDTH).as_int();
+				auto it = cell->parameters.find(ID::WIDTH);
+				int width = it == cell->parameters.end()? 1 : it->second.as_int();
 				string a_expr = make_expr(cell->getPort(ID::A));
 				string b_expr = make_expr(cell->getPort(ID::B));
 				string s_expr = make_expr(cell->getPort(ID::S));
@@ -1076,6 +1106,18 @@ struct FirrtlWorker
 
 		for (auto str : wire_exprs)
 			f << str;
+
+		f << stringf("\n");
+	}
+
+	void run()
+	{
+		// Blackboxes should be emitted as `extmodule`s in firrtl. Only ports are
+		// emitted in such a case.
+		if (module->get_blackbox_attribute())
+			emit_extmodule();
+		else
+			emit_module();
 	}
 };
 
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 3e67e55f2..26f17bcb3 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -590,7 +590,17 @@ struct Smt2Worker
 			if (cell->type == ID($sub)) return export_bvop(cell, "(bvsub A B)");
 			if (cell->type == ID($mul)) return export_bvop(cell, "(bvmul A B)");
 			if (cell->type == ID($div)) return export_bvop(cell, "(bvUdiv A B)", 'd');
+			// "rem" = truncating modulo
 			if (cell->type == ID($mod)) return export_bvop(cell, "(bvUrem A B)", 'd');
+			// "mod" = flooring modulo
+			if (cell->type == ID($modfloor)) {
+				// bvumod doesn't exist because it's the same as bvurem
+				if (cell->getParam(ID::A_SIGNED).as_bool()) {
+					return export_bvop(cell, "(bvsmod A B)", 'd');
+				} else {
+					return export_bvop(cell, "(bvurem A B)", 'd');
+				}
+			}
 
 			if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)) &&
 					2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) {
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index d3015b066..03f001bfd 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -1511,7 +1511,7 @@ else:  # not tempind, covermode
                             smt_assert_consequent(get_constr_expr(constr_assumes, i))
                         print_msg("Re-solving with appended steps..")
                         if smt_check_sat() == "unsat":
-                            print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
+                            print("%s Cannot append steps without violating assumptions!" % smt.timestamp())
                             retstatus = "FAILED"
                             break
                     print_anyconsts(step)
@@ -1548,7 +1548,7 @@ else:  # not tempind, covermode
                         break
 
                     smt_pop()
-                if not retstatus:
+                if retstatus == "FAILED" or retstatus == "PREUNSAT":
                     break
 
         else:  # gentrace
@@ -1557,8 +1557,9 @@ else:  # not tempind, covermode
                 smt_assert(get_constr_expr(constr_asserts, i))
 
             print_msg("Solving for step %d.." % (last_check_step))
-            if smt_check_sat() != "sat":
-                print("%s No solution found!" % smt.timestamp())
+            status = smt_check_sat()
+            if status != "sat":
+                print("%s No solution found! (%s)" % (smt.timestamp(), status))
                 retstatus = "FAILED"
                 break
 
@@ -1568,7 +1569,7 @@ else:  # not tempind, covermode
 
         step += step_size
 
-    if gentrace and retstatus:
+    if gentrace and retstatus == "PASSED":
         print_anyconsts(0)
         write_trace(0, num_steps, '%')
 
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 69f59df79..9f7c8c6d9 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -121,6 +121,7 @@ class SmtIo:
         self.logic_bv = True
         self.logic_dt = False
         self.forall = False
+        self.timeout = 0
         self.produce_models = True
         self.smt2cache = [list()]
         self.p = None
@@ -135,6 +136,7 @@ class SmtIo:
             self.debug_file = opts.debug_file
             self.dummy_file = opts.dummy_file
             self.timeinfo = opts.timeinfo
+            self.timeout = opts.timeout
             self.unroll = opts.unroll
             self.noincr = opts.noincr
             self.info_stmts = opts.info_stmts
@@ -147,6 +149,7 @@ class SmtIo:
             self.debug_file = None
             self.dummy_file = None
             self.timeinfo = os.name != "nt"
+            self.timeout = 0
             self.unroll = False
             self.noincr = False
             self.info_stmts = list()
@@ -172,22 +175,32 @@ class SmtIo:
             self.unroll = False
 
         if self.solver == "yices":
-            if self.noincr:
+            if self.noincr or self.forall:
                 self.popen_vargs = ['yices-smt2'] + self.solver_opts
             else:
                 self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
+            if self.timeout != 0:
+                self.popen_vargs.append('-t')
+                self.popen_vargs.append('%d' % self.timeout);
 
         if self.solver == "z3":
             self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
+            if self.timeout != 0:
+                self.popen_vargs.append('-T:%d' % self.timeout);
 
         if self.solver == "cvc4":
             if self.noincr:
                 self.popen_vargs = ['cvc4', '--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
+            if self.timeout != 0:
+                self.popen_vargs.append('--tlimit=%d000' % self.timeout);
 
         if self.solver == "mathsat":
             self.popen_vargs = ['mathsat'] + self.solver_opts
+            if self.timeout != 0:
+                print('timeout option is not supported for mathsat.')
+                sys.exit(1)
 
         if self.solver == "boolector":
             if self.noincr:
@@ -195,6 +208,9 @@ class SmtIo:
             else:
                 self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
             self.unroll = True
+            if self.timeout != 0:
+                print('timeout option is not supported for boolector.')
+                sys.exit(1)
 
         if self.solver == "abc":
             if len(self.solver_opts) > 0:
@@ -204,6 +220,9 @@ class SmtIo:
             self.logic_ax = False
             self.unroll = True
             self.noincr = True
+            if self.timeout != 0:
+                print('timeout option is not supported for abc.')
+                sys.exit(1)
 
         if self.solver == "dummy":
             assert self.dummy_file is not None
@@ -232,12 +251,16 @@ class SmtIo:
             if self.logic_uf: self.logic += "UF"
             if self.logic_bv: self.logic += "BV"
             if self.logic_dt: self.logic = "ALL"
+            if self.solver == "yices" and self.forall: self.logic = "BV"
 
         self.setup_done = True
 
         for stmt in self.info_stmts:
             self.write(stmt)
 
+        if self.forall and self.solver == "yices":
+            self.write("(set-option :yices-ef-max-iters 1000000000)")
+
         if self.produce_models:
             self.write("(set-option :produce-models true)")
 
@@ -706,7 +729,7 @@ class SmtIo:
 
         if self.forall:
             result = self.read()
-            while result not in ["sat", "unsat", "unknown"]:
+            while result not in ["sat", "unsat", "unknown", "timeout", "interrupted", ""]:
                 print("%s %s: %s" % (self.timestamp(), self.solver, result))
                 result = self.read()
         else:
@@ -717,7 +740,7 @@ class SmtIo:
             print("(check-sat)", file=self.debug_file)
             self.debug_file.flush()
 
-        if result not in ["sat", "unsat"]:
+        if result not in ["sat", "unsat", "unknown", "timeout", "interrupted"]:
             if result == "":
                 print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True)
             else:
@@ -927,7 +950,7 @@ class SmtIo:
 class SmtOpts:
     def __init__(self):
         self.shortopts = "s:S:v"
-        self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
+        self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
         self.solver = "yices"
         self.solver_opts = list()
         self.debug_print = False
@@ -936,6 +959,7 @@ class SmtOpts:
         self.unroll = False
         self.noincr = False
         self.timeinfo = os.name != "nt"
+        self.timeout = 0
         self.logic = None
         self.info_stmts = list()
         self.nocomments = False
@@ -945,6 +969,8 @@ class SmtOpts:
             self.solver = a
         elif o == "-S":
             self.solver_opts.append(a)
+        elif o == "--timeout":
+            self.timeout = int(a)
         elif o == "-v":
             self.debug_print = True
         elif o == "--unroll":
@@ -976,6 +1002,9 @@ class SmtOpts:
     -S <opt>
         pass <opt> as command line argument to the solver
 
+    --timeout <value>
+        set the solver timeout to the specified value (in seconds).
+
     --logic <smt2_logic>
         use the specified SMT2 logic (e.g. QF_AUFBV)
 
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 7113ebc97..2fc7099f4 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -358,7 +358,8 @@ struct SmvWorker
 				continue;
 			}
 
-			if (cell->type.in(ID($div), ID($mod)))
+			// SMV has a "mod" operator, but its semantics don't seem to be well-defined - to be safe, don't generate it at all
+			if (cell->type.in(ID($div)/*, ID($mod), ID($modfloor)*/))
 			{
 				int width_y = GetSize(cell->getPort(ID::Y));
 				int width = max(width_y, GetSize(cell->getPort(ID::A)));
@@ -366,7 +367,7 @@ struct SmvWorker
 				string expr_a, expr_b, op;
 
 				if (cell->type == ID($div))  op = "/";
-				if (cell->type == ID($mod))  op = "mod";
+				//if (cell->type == ID($mod))  op = "mod";
 
 				if (cell->getParam(ID::A_SIGNED).as_bool())
 				{
diff --git a/backends/smv/test_cells.sh b/backends/smv/test_cells.sh
index 63de465c0..145b9c33b 100644
--- a/backends/smv/test_cells.sh
+++ b/backends/smv/test_cells.sh
@@ -7,8 +7,8 @@ mkdir -p test_cells.tmp
 cd test_cells.tmp
 
 # don't test $mul to reduce runtime
-# don't test $div and $mod to reduce runtime and avoid "div by zero" message
-../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$macc /$mul /$div /$mod'
+# don't test $div/$mod/$divfloor/$modfloor to reduce runtime and avoid "div by zero" message
+../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$macc /$mul /$div /$mod /$divfloor /$modfloor'
 
 cat > template.txt << "EOT"
 %module main
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 11b2ae10f..4f44a053a 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -740,6 +740,95 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 #undef HANDLE_UNIOP
 #undef HANDLE_BINOP
 
+	if (cell->type == ID($divfloor))
+	{
+		// wire [MAXLEN+1:0] _0_, _1_, _2_;
+		// assign _0_ = $signed(A);
+		// assign _1_ = $signed(B);
+		// assign _2_ = (A[-1] == B[-1]) || A == 0 ? _0_ : $signed(_0_ - (B[-1] ? _1_ + 1 : _1_ - 1));
+		// assign Y = $signed(_2_) / $signed(_1_);
+
+		if (cell->getParam(ID::A_SIGNED).as_bool() && cell->getParam(ID::B_SIGNED).as_bool()) {
+			SigSpec sig_a = cell->getPort(ID::A);
+			SigSpec sig_b = cell->getPort(ID::B);
+
+			std::string buf_a = next_auto_id();
+			std::string buf_b = next_auto_id();
+			std::string buf_num = next_auto_id();
+			int size_a = GetSize(sig_a);
+			int size_b = GetSize(sig_b);
+			int size_y = GetSize(cell->getPort(ID::Y));
+			int size_max = std::max(size_a, std::max(size_b, size_y));
+
+			// intentionally one wider than maximum width
+			f << stringf("%s" "wire [%d:0] %s, %s, %s;\n", indent.c_str(), size_max, buf_a.c_str(), buf_b.c_str(), buf_num.c_str());
+			f << stringf("%s" "assign %s = ", indent.c_str(), buf_a.c_str());
+			dump_cell_expr_port(f, cell, "A", true);
+			f << stringf(";\n");
+			f << stringf("%s" "assign %s = ", indent.c_str(), buf_b.c_str());
+			dump_cell_expr_port(f, cell, "B", true);
+			f << stringf(";\n");
+
+			f << stringf("%s" "assign %s = ", indent.c_str(), buf_num.c_str());
+			f << stringf("(");
+			dump_sigspec(f, sig_a.extract(sig_a.size()-1));
+			f << stringf(" == ");
+			dump_sigspec(f, sig_b.extract(sig_b.size()-1));
+			f << stringf(") || ");
+			dump_sigspec(f, sig_a);
+			f << stringf(" == 0 ? %s : ", buf_a.c_str());
+			f << stringf("$signed(%s - (", buf_a.c_str());
+			dump_sigspec(f, sig_b.extract(sig_b.size()-1));
+			f << stringf(" ? %s + 1 : %s - 1));\n", buf_b.c_str(), buf_b.c_str());
+
+
+			f << stringf("%s" "assign ", indent.c_str());
+			dump_sigspec(f, cell->getPort(ID::Y));
+			f << stringf(" = $signed(%s) / ", buf_num.c_str());
+			dump_attributes(f, "", cell->attributes, ' ');
+			f << stringf("$signed(%s);\n", buf_b.c_str());
+			return true;
+		} else {
+			// same as truncating division
+			dump_cell_expr_binop(f, indent, cell, "/");
+			return true;
+		}
+	}
+
+	if (cell->type == ID($modfloor))
+	{
+		// wire truncated = $signed(A) % $signed(B);
+		// assign Y = (A[-1] == B[-1]) || truncated == 0 ? truncated : $signed(B) + $signed(truncated);
+
+		if (cell->getParam(ID::A_SIGNED).as_bool() && cell->getParam(ID::B_SIGNED).as_bool()) {
+			SigSpec sig_a = cell->getPort(ID::A);
+			SigSpec sig_b = cell->getPort(ID::B);
+
+			std::string temp_id = next_auto_id();
+			f << stringf("%s" "wire [%d:0] %s = ", indent.c_str(), GetSize(cell->getPort(ID::A))-1, temp_id.c_str());
+			dump_cell_expr_port(f, cell, "A", true);
+			f << stringf(" %% ");
+			dump_attributes(f, "", cell->attributes, ' ');
+			dump_cell_expr_port(f, cell, "B", true);
+			f << stringf(";\n");
+
+			f << stringf("%s" "assign ", indent.c_str());
+			dump_sigspec(f, cell->getPort(ID::Y));
+			f << stringf(" = (");
+			dump_sigspec(f, sig_a.extract(sig_a.size()-1));
+			f << stringf(" == ");
+			dump_sigspec(f, sig_b.extract(sig_b.size()-1));
+			f << stringf(") || %s == 0 ? %s : ", temp_id.c_str(), temp_id.c_str());
+			dump_cell_expr_port(f, cell, "B", true);
+			f << stringf(" + $signed(%s);\n", temp_id.c_str());
+			return true;
+		} else {
+			// same as truncating modulo
+			dump_cell_expr_binop(f, indent, cell, "%");
+			return true;
+		}
+	}
+
 	if (cell->type == ID($shift))
 	{
 		f << stringf("%s" "assign ", indent.c_str());