2 files changed, 28 insertions, 3 deletions

diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index 6cf255184..136259558 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -148,6 +148,9 @@ void recover_solution(QbfSolutionType &sol) {
 
 dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module, const QbfSolutionType &sol) {
 	dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit;
+	pool<RTLIL::SigBit> anyconst_sigbits;
+	dict<RTLIL::SigBit, RTLIL::SigBit> anyconst_sigbit_to_wire_sigbit;
+
 	for (auto cell : module->cells()) {
 		pool<std::string> cell_src = cell->get_strpool_attribute(ID::src);
 		auto pos = sol.hole_to_value.find(cell_src);
@@ -155,10 +158,30 @@ dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_m
 			RTLIL::SigSpec port_y = cell->getPort(ID::Y);
 			for (int i = GetSize(port_y) - 1; i >= 0; --i) {
 				hole_loc_idx_to_sigbit[std::make_pair(pos->first, i)] = port_y[i];
+				anyconst_sigbits.insert(port_y[i]);
 			}
 		}
 	}
 
+	for (auto &conn : module->connections()) {
+		auto lhs = conn.first;
+		auto rhs = conn.second;
+		for (auto i = 0; i < GetSize(rhs); ++i) {
+			if (anyconst_sigbits[rhs[i]]) {
+				auto pos = anyconst_sigbit_to_wire_sigbit.find(rhs[i]);
+				if (pos != anyconst_sigbit_to_wire_sigbit.end())
+					log_cmd_error("conflicting names for hole $anyconst sigbit %s\n", log_signal(rhs[i]));
+				anyconst_sigbit_to_wire_sigbit[rhs[i]] = lhs[i];
+			}
+		}
+	}
+
+	for (auto &it : hole_loc_idx_to_sigbit) {
+		auto pos = anyconst_sigbit_to_wire_sigbit.find(it.second);
+		if (pos != anyconst_sigbit_to_wire_sigbit.end())
+			it.second = pos->second;
+	}
+
 	return hole_loc_idx_to_sigbit;
 }
 
@@ -275,8 +298,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) {
 			pool<std::string> hole_loc_pool(locs.begin(), locs.end());
 			auto hole_cell_it = anyconst_loc_to_cell.find(hole_loc_pool);
 			if (hole_cell_it == anyconst_loc_to_cell.end())
-				YS_DEBUGTRAP;
-				//log_cmd_error("cannot find matching wire name or $anyconst cell location for hole spec \"%s\"\n", buf.c_str());
+				log_cmd_error("cannot find matching wire name or $anyconst cell location for hole spec \"%s\"\n", buf.c_str());
 
 			RTLIL::Cell *hole_cell = hole_cell_it->second;
 			hole_sigbit = hole_cell->getPort(ID::Y)[hole_bit];
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 1ab082b09..fb496ff87 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -163,7 +163,10 @@ struct SimInstance
 
 				mem_database[cell] = mem;
 			}
-
+			if (cell->type.in(ID($memwr),ID($memrd)))
+			{
+				log_error("$memrd and $memwr cells have to be merged to stand-alone $mem cells (execute memory_collect pass)\n");
+			}
 			if (cell->type.in(ID($assert), ID($cover), ID($assume))) {
 				formal_database.insert(cell);
 			}