From b9e79e0bb76e0b45650005914ebf21c77e0242d1 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 25 Mar 2020 23:51:32 +0000 Subject: [PATCH] Implement `-write-solution` option for the `qbfsat` command. --- passes/sat/qbfsat.cc | 35 ++++++++++++++++++++++++++++------- 1 file changed, 28 insertions(+), 7 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index b95c81501..6ac952ea4 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -86,19 +86,35 @@ void recover_solution(QbfSolutionType &sol) { log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true); } -void specialize(RTLIL::Module *module, const QbfSolutionType &ret) { +std::map get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) { 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()) { + auto pos = sol.hole_to_value.find(cell_src); + if (pos != sol.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) { + + return hole_loc_to_name; +} + +void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) { + std::ofstream fout(file.c_str()); + if (!fout) + log_cmd_error("could not open solution file for writing.\n"); + + std::map 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; +} + +void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { + std::map hole_loc_to_name = get_hole_loc_name_map(module, sol); + for (auto &it : sol.hole_to_value) { std::string hole_loc = it.first; std::string hole_value = it.second; @@ -389,9 +405,14 @@ struct QbfSatPass : public Pass { else print_proof_failed(); - if (opt.specialize) { - specialize(module, ret); - Pass::call(design, "opt_clean"); + if(!ret.unknown && ret.sat) { + if (opt.write_solution) { + write_solution(module, ret, opt.write_soln_soln_file); + } + if (opt.specialize) { + specialize(module, ret); + Pass::call(design, "opt_clean"); + } } } } QbfSatPass; -- 2.30.2