1 files changed, 16 insertions, 8 deletions

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 081dcda99..eb4826051 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -536,6 +536,14 @@ struct Smt2Worker
 				if (cell->attributes.count("\\reg"))
 					infostr += " " + cell->attributes.at("\\reg").decode_string();
 				decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort("\\Y")), infostr.c_str()));
+				if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\maximize")){
+					decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter));
+					log("Wire %s is maximized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
+				}
+				else if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\minimize")){
+					decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter));
+					log("Wire %s is minimized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
+				}
 				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
 				if (cell->type == "$anyseq")
 					ex_input_eq.push_back(stringf("  (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
@@ -1386,7 +1394,7 @@ struct Smt2Backend : public Backend {
 		log("\n");
 		log("For this proof we create the following template (test.tpl).\n");
 		log("\n");
-		log("        ; we need QF_UFBV for this poof\n");
+		log("        ; we need QF_UFBV for this proof\n");
 		log("        (set-logic QF_UFBV)\n");
 		log("\n");
 		log("        ; insert the auto-generated code here\n");
@@ -1500,11 +1508,11 @@ struct Smt2Backend : public Backend {
 
 		// extract module dependencies
 		std::map<RTLIL::Module*, std::set<RTLIL::Module*>> module_deps;
-		for (auto &mod_it : design->modules_) {
-			module_deps[mod_it.second] = std::set<RTLIL::Module*>();
-			for (auto &cell_it : mod_it.second->cells_)
-				if (design->modules_.count(cell_it.second->type) > 0)
-					module_deps[mod_it.second].insert(design->modules_.at(cell_it.second->type));
+		for (auto mod : design->modules()) {
+			module_deps[mod] = std::set<RTLIL::Module*>();
+			for (auto cell : mod->cells())
+				if (design->has(cell->type))
+					module_deps[mod].insert(design->module(cell->type));
 		}
 
 		// simple good-enough topological sort
@@ -1515,12 +1523,12 @@ struct Smt2Backend : public Backend {
 				for (auto &dep : it.second)
 					if (module_deps.count(dep) > 0)
 						goto not_ready_yet;
-				// log("Next in topological sort: %s\n", RTLIL::id2cstr(it.first->name));
+				// log("Next in topological sort: %s\n", log_id(it.first->name));
 				sorted_modules.push_back(it.first);
 			not_ready_yet:;
 			}
 			if (sorted_modules_idx == sorted_modules.size())
-				log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", RTLIL::id2cstr(module_deps.begin()->first->name));
+				log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", log_id(module_deps.begin()->first->name));
 			while (sorted_modules_idx < sorted_modules.size())
 				module_deps.erase(sorted_modules.at(sorted_modules_idx++));
 		}