From a4598d64ef5f8386b28019bb64b7ad2d6e0c9d7e Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 25 Mar 2020 22:37:54 +0000 Subject: [PATCH] Hole value recovery and specialization implementation for `qbfsat` command. --- kernel/log.h | 7 ++++ passes/sat/qbfsat.cc | 83 +++++++++++++++++++++++++++++++++----------- 2 files changed, 70 insertions(+), 20 deletions(-) diff --git a/kernel/log.h b/kernel/log.h index cd0e8185c..5478482ac 100644 --- a/kernel/log.h +++ b/kernel/log.h @@ -29,18 +29,25 @@ #if defined(__GNUC__) && !defined( __clang__) && ( __GNUC__ == 4 && __GNUC_MINOR__ <= 8) #include #define YS_REGEX_TYPE boost::xpressive::sregex + #define YS_REGEX_MATCH_TYPE boost::xpressive::smatch #define YS_REGEX_NS boost::xpressive #define YS_REGEX_COMPILE(param) boost::xpressive::sregex::compile(param, \ boost::xpressive::regex_constants::nosubs | \ boost::xpressive::regex_constants::optimize) + #define YS_REGEX_COMPILE_WITH_SUBS(param) boost::xpressive::sregex::compile(param, \ + boost::xpressive::regex_constants::optimize) # else #include #define YS_REGEX_TYPE std::regex + #define YS_REGEX_MATCH_TYPE std::smatch #define YS_REGEX_NS std #define YS_REGEX_COMPILE(param) std::regex(param, \ std::regex_constants::nosubs | \ std::regex_constants::optimize | \ std::regex_constants::egrep) + #define YS_REGEX_COMPILE_WITH_SUBS(param) std::regex(param, \ + std::regex_constants::optimize | \ + std::regex_constants::egrep) #endif #ifndef _WIN32 diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index dd57b91c9..3045c2284 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -39,6 +39,7 @@ PRIVATE_NAMESPACE_BEGIN struct QbfSolutionType { std::vector stdout; + std::map hole_to_value; bool sat; bool unknown; //true if neither 'sat' nor 'unsat' bool success; //true if exit code 0 @@ -56,8 +57,34 @@ struct QbfSolveOptions { nocleanup(false), dump_final_smt2(false), timeout_sec(-1) {}; }; -QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { +void recover_solution(RTLIL::Module *mod, QbfSolutionType &sol) { + YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED"); + YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available"); + YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)"); + YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+"); + YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+"); + YS_REGEX_MATCH_TYPE m; + bool sat_regex_found = false; + bool unsat_regex_found = false; + std::map hole_value_recovered; + for (const std::string &x : sol.stdout) { + if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) { + std::string loc = m[1].str(); + std::string val = m[2].str(); + log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex)); + log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex)); + sol.hole_to_value[loc] = val; + } + else if (YS_REGEX_NS::regex_search(x, sat_regex)) + sat_regex_found = true; + else if (YS_REGEX_NS::regex_search(x, unsat_regex)) + unsat_regex_found = true; + } + log_assert(!sol.unknown && sol.sat? sat_regex_found : true); + log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true); +} +QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { QbfSolutionType ret; std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; std::string smtbmc_warning = "z3: WARNING:"; @@ -127,22 +154,12 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { if(!opt.nocleanup) remove_directory(tempdir_name); - YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED"); - bool sat_regex_found = false; - YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available"); - bool unsat_regex_found = false; - for (auto &x : ret.stdout) { - //TODO: recover values here for later specialization? - if (YS_REGEX_NS::regex_search(x, sat_regex)) - sat_regex_found = true; - if (YS_REGEX_NS::regex_search(x, unsat_regex)) - unsat_regex_found = true; - } - log_assert(ret.sat? sat_regex_found : true); - log_assert(!ret.unknown && !ret.sat? unsat_regex_found : true); + recover_solution(mod, ret); + return ret; } + void print_proof_failed() { log("\n"); @@ -294,10 +311,9 @@ struct QbfSatPass : public Pass { if (!found_1bit_output) log_cmd_error("Did not find any single-bit outputs, assert()s, or assume()s. Is this a miter circuit?\n"); - //Do not modify the current design. Operate on a clone of the selected module. - RTLIL::Design *new_design = new Design(); - module = module->clone(); - new_design->add(module); + //Save the design to restore after modiyfing the current module. + std::string module_name = module->name.str(); + Pass::call(design, "design -save _qbfsat_tmp"); //Replace input wires with wires assigned $allconst cells. for(auto &n : input_wires) { @@ -314,6 +330,8 @@ struct QbfSatPass : public Pass { module->fixup_ports(); QbfSolutionType ret = qbf_solve(module, opt); + Pass::call(design, "design -load _qbfsat_tmp"); + module = design->module(module_name); if (ret.unknown) log_warning("solver did not give an answer\n"); @@ -322,9 +340,34 @@ struct QbfSatPass : public Pass { else print_proof_failed(); - //TODO specialize etc. + if (opt.specialize) { + std::map hole_loc_to_name; + for (auto cell : module->cells()) { + std::string cell_src = cell->get_src_attribute(); + auto pos = ret.hole_to_value.find(cell_src); + if (pos != ret.hole_to_value.end()) { + log_assert(cell->type.in("$anyconst", "$anyseq")); + log_assert(cell->hasPort(ID::Y)); + log_assert(cell->getPort(ID::Y).is_wire()); + hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str(); + } + } + for (auto &it : ret.hole_to_value) { + std::string hole_loc = it.first; + std::string hole_value = it.second; + + auto pos = hole_loc_to_name.find(hole_loc); + log_assert(pos != hole_loc_to_name.end()); - delete new_design; + std::string hole_name = hole_loc_to_name[hole_loc]; + RTLIL::Wire *wire = module->wire(hole_name); + log_assert(wire != nullptr); + + log("Specializing %s with %s = %s.\n", module->name.c_str(), hole_name.c_str(), hole_value.c_str()); + module->connect(wire, hole_value); + } + Pass::call(design, "opt_clean"); + } } } QbfSatPass; -- 2.30.2