From a3d1f8637a8a9a97e3152fea1ceae23f798f54d8 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Fri, 22 May 2020 04:48:33 +0000 Subject: qbfsat: Use bit precise mapping for hole value wires and a more robust hole spec for writing to and specializing from a solution file. --- passes/sat/qbfsat.cc | 193 ++++++++++++++++++++++++++++++--------------------- 1 file changed, 113 insertions(+), 80 deletions(-) (limited to 'passes') diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 4686e985b..b3133c633 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -30,7 +30,7 @@ PRIVATE_NAMESPACE_BEGIN struct QbfSolutionType { std::vector stdout_lines; - dict hole_to_value; + dict, std::string> hole_to_value; bool sat; bool unknown; //true if neither 'sat' nor 'unsat' @@ -91,7 +91,10 @@ 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; + RTLIL::AttrObject tmp; + tmp.set_src_attribute(loc); + pool loc_pool = tmp.get_strpool_attribute(ID::src); + sol.hole_to_value[loc_pool] = val; } else if (YS_REGEX_NS::regex_search(x, sat_regex)) { sat_regex_found = true; @@ -134,18 +137,20 @@ void recover_solution(QbfSolutionType &sol) { #endif } -dict get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) { - dict hole_loc_to_name; +dict, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module, const QbfSolutionType &sol) { + dict, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit; for (auto cell : module->cells()) { - std::string cell_src = cell->get_src_attribute(); + pool 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 validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) { @@ -187,113 +192,141 @@ 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 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 the form: + // + //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, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol); + for (auto &x : sol.hole_to_value) { + RTLIL::AttrObject tmp; + tmp.set_strpool_attribute(ID::src, x.first); + std::string src_as_str = tmp.get_string_attribute(ID::src); + for (auto i = 0; i < GetSize(x.second); ++i) + fout << src_as_str.c_str() << "[" << i << "]#" << hole_loc_idx_to_sigbit[std::make_pair(x.first, i)].str() << "=" << 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_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.*)\\[([0-9]+)]#(.*)\\[([0-9]+)]=([01])$"); YS_REGEX_MATCH_TYPE m; - pool anyconsts_to_remove; - dict hole_name_to_value; + //(hole_loc, hole_bit, hole_name, hole_offset) -> (value, found) + dict, RTLIL::Cell*> anyconst_loc_to_cell; + dict 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; + 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 = m[1].str(); + unsigned int hole_bit = atoi(m[2].str().c_str()); + std::string hole_name = m[3].str(); + unsigned int hole_offset = atoi(m[4].str().c_str()); + RTLIL::State hole_value = atoi(m[5].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 { + RTLIL::AttrObject tmp; + tmp.set_src_attribute(hole_loc); + pool hole_loc_pool = tmp.get_strpool_attribute(ID::src); + 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 : 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 + for (auto &it : anyconst_loc_to_cell) + module->remove(it.second); - 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 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(), it.first.str().c_str(), it.second == RTLIL::State::S1? 1 : 0); + module->connect(lhs, rhs); } } void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = false) { - dict hole_loc_to_name = get_hole_loc_name_map(module, sol); + dict, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol); pool 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 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 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(), hole_sigbit.str().c_str(), 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 hole_loc_to_name = get_hole_loc_name_map(module, sol); + dict, 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 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 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", hole_sigbit.str().c_str(), hole_value[bit_idx]); + } } } -- cgit v1.2.3 From 4ab41c64359ea487e74b3c4901525ad155f11ec1 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Tue, 26 May 2020 23:12:15 +0000 Subject: qbfsat: Fixes three bugs. 1. Infinite loop in the optimization procedure when the first solution found while maximizing is at zero. 2. A signed-ness issue when maximizing. 3. Erroneously entering bisection mode with no wire to optimize. --- passes/sat/qbfsat.cc | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) (limited to 'passes') diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index b3133c633..f325d9e22 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -28,6 +28,13 @@ 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 stdout_lines; dict, std::string> hole_to_value; @@ -443,7 +450,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); @@ -460,7 +467,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"); @@ -498,8 +505,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; @@ -512,8 +520,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); -- cgit v1.2.3 From 08cede46691e65e09a69e964cd51261d327d0522 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Tue, 9 Jun 2020 05:27:09 +0000 Subject: qbfsat: Simplify solution format and replace `SigBit::str()` with `log_signal()`. Co-Authored-By: Claire Wolf --- passes/sat/qbfsat.cc | 56 ++++++++++++++++++++++++++++++++++------------------ 1 file changed, 37 insertions(+), 19 deletions(-) (limited to 'passes') diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index f325d9e22..77eca98ef 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -213,27 +213,29 @@ void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std //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 the form: + //the solution on a separate line. Each line is of one of two forms: // - //location[bit]#name[offset]=value + //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. + //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, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol); for (auto &x : sol.hole_to_value) { RTLIL::AttrObject tmp; tmp.set_strpool_attribute(ID::src, x.first); std::string src_as_str = tmp.get_string_attribute(ID::src); for (auto i = 0; i < GetSize(x.second); ++i) - fout << src_as_str.c_str() << "[" << i << "]#" << hole_loc_idx_to_sigbit[std::make_pair(x.first, i)].str() << "=" << x.second[GetSize(x.second) - 1 - i] << std::endl; + 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("^(.*)\\[([0-9]+)]#(.*)\\[([0-9]+)]=([01])$"); - YS_REGEX_MATCH_TYPE m; + 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, RTLIL::Cell*> anyconst_loc_to_cell; dict hole_assignments; @@ -248,13 +250,29 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { std::string buf; while (std::getline(fin, buf)) { - 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 = m[1].str(); - unsigned int hole_bit = atoi(m[2].str().c_str()); - std::string hole_name = m[3].str(); - unsigned int hole_offset = atoi(m[4].str().c_str()); - RTLIL::State hole_value = atoi(m[5].str().c_str()) == 1? RTLIL::State::S1 : RTLIL::State::S0; + std::string hole_loc; + unsigned int hole_bit; + std::string hole_name; + unsigned int hole_offset; + RTLIL::State hole_value; + + if (!YS_REGEX_NS::regex_search(buf, bit_m, hole_bit_assn_regex)) { + 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()); + } else { + hole_loc = m[1].str(); + hole_bit = atoi(m[2].str().c_str()); + hole_name = m[3].str(); + hole_offset = 0; + hole_value = atoi(m[4].str().c_str()) == 1? RTLIL::State::S1 : RTLIL::State::S0; + } + } else { + hole_loc = bit_m[1].str(); + hole_bit = atoi(bit_m[2].str().c_str()); + hole_name = bit_m[3].str(); + hole_offset = atoi(bit_m[4].str().c_str()); + hole_value = atoi(bit_m[5].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. @@ -283,7 +301,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { 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(), it.first.str().c_str(), it.second == RTLIL::State::S1? 1 : 0); + 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); } } @@ -312,7 +330,7 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = 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(), hole_sigbit.str().c_str(), hole_bit_val == RTLIL::State::S0? 0 : 1) + 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); } @@ -332,7 +350,7 @@ void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) { log_assert(it != hole_loc_idx_to_sigbit.end()); RTLIL::SigBit hole_sigbit = it->second; - log("\t%s = 1'b%c\n", hole_sigbit.str().c_str(), hole_value[bit_idx]); + log("\t%s = 1'b%c\n", log_signal(hole_sigbit), hole_value[bit_idx]); } } } -- cgit v1.2.3 From e1fedf054ec266be7bdc6897cc5c1fe66e4fafb1 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Tue, 9 Jun 2020 21:31:58 +0000 Subject: qbfsat: Avoid instantiating `AttrObject`s directly. Co-Authored-By: Claire Wolf --- passes/sat/qbfsat.cc | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) (limited to 'passes') diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 77eca98ef..d4fbee1ec 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -24,6 +24,7 @@ #include "kernel/rtlil.h" #include "kernel/register.h" #include +#include USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -98,9 +99,8 @@ 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 - RTLIL::AttrObject tmp; - tmp.set_src_attribute(loc); - pool loc_pool = tmp.get_strpool_attribute(ID::src); + auto locs = split_tokens(loc, "|"); + pool loc_pool(locs.begin(), locs.end()); sol.hole_to_value[loc_pool] = val; } else if (YS_REGEX_NS::regex_search(x, sat_regex)) { @@ -224,9 +224,7 @@ void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std //SigBit, and "value", which is either '0' or '1', represents the assignment for that bit. dict, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol); for (auto &x : sol.hole_to_value) { - RTLIL::AttrObject tmp; - tmp.set_strpool_attribute(ID::src, x.first); - std::string src_as_str = tmp.get_string_attribute(ID::src); + 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; } @@ -281,9 +279,8 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { RTLIL::Wire *hole_wire = module->wire(hole_name); hole_sigbit = RTLIL::SigSpec(hole_wire)[hole_offset]; } else { - RTLIL::AttrObject tmp; - tmp.set_src_attribute(hole_loc); - pool hole_loc_pool = tmp.get_strpool_attribute(ID::src); + auto locs = split_tokens(hole_loc, "|"); + pool 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; -- cgit v1.2.3 From 62a9e62a1bc016122c2224bb157e86d8dbad5613 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Tue, 9 Jun 2020 21:44:45 +0000 Subject: qbfsat: Simplify solution recovery parsing and tweak the solution regexes. --- passes/sat/qbfsat.cc | 34 ++++++++++++---------------------- 1 file changed, 12 insertions(+), 22 deletions(-) (limited to 'passes') diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index d4fbee1ec..35a0d0b1e 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -231,8 +231,8 @@ void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std } void specialize_from_file(RTLIL::Module *module, const std::string &file) { - 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_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, RTLIL::Cell*> anyconst_loc_to_cell; @@ -248,30 +248,20 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { std::string buf; while (std::getline(fin, buf)) { - std::string hole_loc; - unsigned int hole_bit; - std::string hole_name; - unsigned int hole_offset; - RTLIL::State hole_value; - + bool bit_assn = true; if (!YS_REGEX_NS::regex_search(buf, bit_m, hole_bit_assn_regex)) { - if (!YS_REGEX_NS::regex_search(buf, m, hole_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()); - } else { - hole_loc = m[1].str(); - hole_bit = atoi(m[2].str().c_str()); - hole_name = m[3].str(); - hole_offset = 0; - hole_value = atoi(m[4].str().c_str()) == 1? RTLIL::State::S1 : RTLIL::State::S0; - } - } else { - hole_loc = bit_m[1].str(); - hole_bit = atoi(bit_m[2].str().c_str()); - hole_name = bit_m[3].str(); - hole_offset = atoi(bit_m[4].str().c_str()); - hole_value = atoi(bit_m[5].str().c_str()) == 1? RTLIL::State::S1 : RTLIL::State::S0; } + 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; -- cgit v1.2.3