Merge pull request #2093 from boqwxp/qbfsat-bugfixes

qbfsat: Multiple bugfixes

1 files changed, 136 insertions, 86 deletions

diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index 4686e985b..35a0d0b1e 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -24,13 +24,21 @@
 #include "kernel/rtlil.h"
 #include "kernel/register.h"
 #include <algorithm>
+#include <numeric>
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+static inline unsigned int difference(unsigned int a, unsigned int b) {
+	if (a < b)
+		return b - a;
+	else
+		return a - b;
+}
+
 struct QbfSolutionType {
 	std::vector<std::string> stdout_lines;
-	dict<std::string, std::string> hole_to_value;
+	dict<pool<std::string>, std::string> hole_to_value;
 	bool sat;
 	bool unknown; //true if neither 'sat' nor 'unsat'
 
@@ -91,7 +99,9 @@ void recover_solution(QbfSolutionType &sol) {
 			log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
 			log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
 #endif
-			sol.hole_to_value[loc] = val;
+			auto locs = split_tokens(loc, "|");
+			pool<std::string> loc_pool(locs.begin(), locs.end());
+			sol.hole_to_value[loc_pool] = val;
 		}
 		else if (YS_REGEX_NS::regex_search(x, sat_regex)) {
 			sat_regex_found = true;
@@ -134,18 +144,20 @@ void recover_solution(QbfSolutionType &sol) {
 #endif
 }
 
-dict<std::string, std::string> get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) {
-	dict<std::string, std::string> hole_loc_to_name;
+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;
 	for (auto cell : module->cells()) {
-		std::string cell_src = cell->get_src_attribute();
+		pool<std::string> cell_src = cell->get_strpool_attribute(ID::src);
 		auto pos = sol.hole_to_value.find(cell_src);
 		if (pos != sol.hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) {
-			log_assert(hole_loc_to_name.find(pos->first) == hole_loc_to_name.end());
-			hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str();
+			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];
+			}
 		}
 	}
 
-	return hole_loc_to_name;
+	return hole_loc_idx_to_sigbit;
 }
 
 pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
@@ -187,113 +199,146 @@ void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std
 	if (!fout)
 		log_cmd_error("could not open solution file for writing.\n");
 
-	dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
-	for(auto &x : sol.hole_to_value)
-		fout << hole_loc_to_name[x.first] << "=" << x.second << std::endl;
+	//There is a question here: How exactly shall we identify holes?
+	//There are at least two reasonable options:
+	//1. By the source location of the $anyconst cells
+	//2. By the name(s) of the wire(s) connected to each SigBit of the $anyconst cell->getPort(ID::Y) SigSpec.
+	//
+	//Option 1 has the benefit of being very precise.  There is very limited potential for confusion, as long
+	//as the source attribute has been set.  However, if the source attribute is not set, this won't work.
+	//More importantly, we want to have the ability to port hole assignments to other modules with compatible
+	//hole names and widths.  Obviously in those cases source locations of the $anyconst cells will not match.
+	//
+	//Option 2 has the benefits previously described, but wire names can be changed automatically by 
+	//optimization or techmapping passes, especially when (ex/im)porting from BLIF for optimization with ABC.
+	//
+	//The approach taken here is to allow both options.  We write the assignment information for each bit of
+	//the solution on a separate line.  Each line is of one of two forms:
+	//
+	//location bit name = value
+	//location bit name [offset] = value
+	//
+	//where '[', ']', and '=' are literal symbols, "location" is the $anyconst cell source location attribute,
+	//"bit" is the index of the $anyconst cell, "name" is the `wire->name` field of the SigBit corresponding
+	//to the current bit of the $anyconst cell->getPort(ID::Y), "offset" is the `offset` field of that same
+	//SigBit, and "value", which is either '0' or '1', represents the assignment for that bit.
+	dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol);
+	for (auto &x : sol.hole_to_value) {
+		std::string src_as_str = std::accumulate(x.first.begin(), x.first.end(), std::string(), [](const std::string &a, const std::string &b){return a + "|" + b;});
+		for (auto i = 0; i < GetSize(x.second); ++i)
+			fout << src_as_str.c_str() << " " << i << " " << log_signal(hole_loc_idx_to_sigbit[std::make_pair(x.first, i)]) << " = " << x.second[GetSize(x.second) - 1 - i] << std::endl;
+	}
 }
 
 void specialize_from_file(RTLIL::Module *module, const std::string &file) {
-	YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.*)=([01]+)$");
-	YS_REGEX_MATCH_TYPE m;
-	pool<RTLIL::Cell *> anyconsts_to_remove;
-	dict<std::string, std::string> hole_name_to_value;
+	YS_REGEX_TYPE hole_bit_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$");
+	YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified
+	YS_REGEX_MATCH_TYPE bit_m, m;
+	//(hole_loc, hole_bit, hole_name, hole_offset) -> (value, found)
+	dict<pool<std::string>, RTLIL::Cell*> anyconst_loc_to_cell;
+	dict<RTLIL::SigBit, RTLIL::State> hole_assignments;
+
+	for (auto cell : module->cells())
+		if (cell->type == "$anyconst")
+			anyconst_loc_to_cell[cell->get_strpool_attribute(ID::src)] = cell;
+
 	std::ifstream fin(file.c_str());
 	if (!fin)
 		log_cmd_error("could not read solution file.\n");
 
 	std::string buf;
 	while (std::getline(fin, buf)) {
-		log_assert(YS_REGEX_NS::regex_search(buf, m, hole_assn_regex));
-		std::string hole_name = m[1].str();
-		std::string hole_value = m[2].str();
-		hole_name_to_value[hole_name] = hole_value;
+		bool bit_assn = true;
+		if (!YS_REGEX_NS::regex_search(buf, bit_m, hole_bit_assn_regex)) {
+			bit_assn = false;
+			if (!YS_REGEX_NS::regex_search(buf, m, hole_assn_regex))
+				log_cmd_error("solution file is not formatted correctly: \"%s\"\n", buf.c_str());
+		}
+
+		std::string hole_loc = bit_assn? bit_m[1].str() : m[1].str();
+		unsigned int hole_bit = bit_assn? atoi(bit_m[2].str().c_str()) : atoi(m[2].str().c_str());
+		std::string hole_name = bit_assn? bit_m[3].str() : m[3].str();
+		unsigned int hole_offset = bit_assn? atoi(bit_m[4].str().c_str()) : 0;
+		RTLIL::State hole_value = bit_assn? (atoi(bit_m[5].str().c_str()) == 1? RTLIL::State::S1 : RTLIL::State::S0)
+		                                  : (atoi(m[4].str().c_str()) == 1? RTLIL::State::S1 : RTLIL::State::S0);
+
+		//We have two options to identify holes.  First, try to match wire names.  If we can't find a matching wire,
+		//then try to find a cell with a matching location.
+		RTLIL::SigBit hole_sigbit;
+		if (module->wire(hole_name) != nullptr) {
+			RTLIL::Wire *hole_wire = module->wire(hole_name);
+			hole_sigbit = RTLIL::SigSpec(hole_wire)[hole_offset];
+		} else {
+			auto locs = split_tokens(hole_loc, "|");
+			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());
+
+			RTLIL::Cell *hole_cell = hole_cell_it->second;
+			hole_sigbit = hole_cell->getPort(ID::Y)[hole_bit];
+		}
+		hole_assignments[hole_sigbit] = hole_value;
 	}
 
-	for (auto cell : module->cells())
-		if (cell->type == "$anyconst") {
-			auto anyconst_port_y = cell->getPort(ID::Y).as_wire();
-			if (anyconst_port_y == nullptr)
-				continue;
-			if (hole_name_to_value.find(anyconst_port_y->name.str()) != hole_name_to_value.end())
-				anyconsts_to_remove.insert(cell);
-		}
-	for (auto cell : anyconsts_to_remove)
-		module->remove(cell);
+	for (auto &it : anyconst_loc_to_cell)
+		module->remove(it.second);
 
-	for (auto &it : hole_name_to_value) {
-		std::string hole_name = it.first;
-		std::string hole_value = it.second;
-		RTLIL::Wire *wire = module->wire(hole_name);
-#ifndef NDEBUG
-		log_assert(wire != nullptr);
-		log_assert(wire->width > 0 && GetSize(hole_value) == wire->width);
-#endif
-
-		log("Specializing %s from file with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str());
-		std::vector<RTLIL::SigBit> value_bv;
-		value_bv.reserve(wire->width);
-		for (char c : hole_value)
-			value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0);
-		std::reverse(value_bv.begin(), value_bv.end());
-		module->connect(wire, value_bv);
+	for (auto &it : hole_assignments) {
+		RTLIL::SigSpec lhs(it.first);
+		RTLIL::SigSpec rhs(it.second);
+		log("Specializing %s from file with %s = %d.\n", module->name.c_str(), log_signal(it.first), it.second == RTLIL::State::S1? 1 : 0);
+		module->connect(lhs, rhs);
 	}
 }
 
 void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = false) {
-	dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
+	dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol);
 	pool<RTLIL::Cell *> anyconsts_to_remove;
 	for (auto cell : module->cells())
 		if (cell->type == "$anyconst")
-			if (hole_loc_to_name.find(cell->get_src_attribute()) != hole_loc_to_name.end())
+			if (hole_loc_idx_to_sigbit.find(std::make_pair(cell->get_strpool_attribute(ID::src), 0)) != hole_loc_idx_to_sigbit.end())
 				anyconsts_to_remove.insert(cell);
 	for (auto cell : anyconsts_to_remove)
 		module->remove(cell);
 	for (auto &it : sol.hole_to_value) {
-		std::string hole_loc = it.first;
+		pool<std::string> hole_loc = it.first;
 		std::string hole_value = it.second;
 
-#ifndef NDEBUG
-		auto pos = hole_loc_to_name.find(hole_loc);
-		log_assert(pos != hole_loc_to_name.end());
-#endif
-
-		std::string hole_name = hole_loc_to_name[hole_loc];
-		RTLIL::Wire *wire = module->wire(hole_name);
-#ifndef NDEBUG
-		log_assert(wire != nullptr);
-		log_assert(wire->width > 0 && GetSize(hole_value) == wire->width);
-#endif
-
-		if (!quiet)
-			log("Specializing %s with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str());
-		std::vector<RTLIL::SigBit> value_bv;
-		value_bv.reserve(wire->width);
-		for (char c : hole_value)
-			value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0);
-		std::reverse(value_bv.begin(), value_bv.end());
-		module->connect(wire, value_bv);
+		for (unsigned int i = 0; i < hole_value.size(); ++i) {
+			int bit_idx = GetSize(hole_value) - 1 - i;
+			auto it = hole_loc_idx_to_sigbit.find(std::make_pair(hole_loc, i));
+			log_assert(it != hole_loc_idx_to_sigbit.end());
+
+			RTLIL::SigBit hole_sigbit = it->second;
+			log_assert(hole_sigbit.wire != nullptr);
+			log_assert(hole_value[bit_idx] == '0' || hole_value[bit_idx] == '1');
+			RTLIL::SigSpec lhs(hole_sigbit.wire, hole_sigbit.offset, 1);
+			RTLIL::State hole_bit_val = hole_value[bit_idx] == '1'? RTLIL::State::S1 : RTLIL::State::S0;
+			if (!quiet)
+				log("Specializing %s with %s = %d.\n", module->name.c_str(), log_signal(hole_sigbit), hole_bit_val == RTLIL::State::S0? 0 : 1)
+;
+			module->connect(lhs, hole_bit_val);
+		}
 	}
 }
 
 void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) {
 	log("Satisfiable model:\n");
-	dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
+	dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol);
 	for (auto &it : sol.hole_to_value) {
-		std::string hole_loc = it.first;
+		pool<std::string> hole_loc = it.first;
 		std::string hole_value = it.second;
 
-#ifndef NDEBUG
-		auto pos = hole_loc_to_name.find(hole_loc);
-		log_assert(pos != hole_loc_to_name.end());
-#endif
+		for (unsigned int i = 0; i < hole_value.size(); ++i) {
+			int bit_idx = GetSize(hole_value) - 1 - i;
+			auto it = hole_loc_idx_to_sigbit.find(std::make_pair(hole_loc, i));
+			log_assert(it != hole_loc_idx_to_sigbit.end());
 
-		std::string hole_name = hole_loc_to_name[hole_loc];
-		log("\t%s = %lu'b%s\n", hole_name.c_str(), hole_value.size(), hole_value.c_str());
-		std::vector<RTLIL::SigBit> value_bv;
-		value_bv.reserve(hole_value.size());
-		for (char c : hole_value)
-			value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0);
-		std::reverse(value_bv.begin(), value_bv.end());
+			RTLIL::SigBit hole_sigbit = it->second;
+			log("\t%s = 1'b%c\n", log_signal(hole_sigbit), hole_value[bit_idx]);
+		}
 	}
 }
 
@@ -410,7 +455,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
 		maximize = wire_to_optimize->get_bool_attribute("\\maximize");
 	}
 
-	if (opt.nobisection || opt.nooptimize) {
+	if (opt.nobisection || opt.nooptimize || wire_to_optimize == nullptr) {
 		if (wire_to_optimize != nullptr && opt.nooptimize) {
 			wire_to_optimize->set_bool_attribute("\\maximize", false);
 			wire_to_optimize->set_bool_attribute("\\minimize", false);
@@ -427,7 +472,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
 		log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), log_signal(wire_to_optimize));
 
 		//If maximizing, grow until we get a failure.  Then bisect success and failure.
-		while (failure == 0 || success - failure > 1) {
+		while (failure == 0 || difference(success, failure) > 1) {
 			Pass::call(design, "design -push-copy");
 			log_header(design, "Preparing QBF-SAT problem.\n");
 
@@ -465,8 +510,9 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
 				//sometimes this happens if we get an 'unknown' or timeout
 				if (!maximize && success < failure)
 					break;
-				else if (maximize && success > failure)
+				else if (maximize && failure != 0 && success > failure)
 					break;
+
 			} else {
 				//Treat 'unknown' as UNSAT
 				failure = cur_thresh;
@@ -479,8 +525,12 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
 			}
 
 			iter_num++;
-			cur_thresh = (maximize && failure == 0)? 2 * success //growth
-			                                       : (success + failure) / 2; //bisection
+			if (maximize && failure == 0 && success == 0)
+				cur_thresh = 2;
+			else if (maximize && failure == 0)
+				cur_thresh = 2 * success; //growth
+			else //if (!maximize || failure != 0)
+				cur_thresh = (success + failure) / 2; //bisection
 		}
 		if (success != 0 || failure != 0) {
 			log("Wire %s is %s at %d.\n", wire_to_optimize_name.c_str(), (maximize? "maximized" : "minimized"), success);