riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Use `log_push()` and `log_pop()` and show the satisfiable model when `-specialize` is not specified. 

Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
This commit is contained in:
Alberto Gonzalez 2020-04-01 19:28:07 +00:00
parent d311a80222
commit 6af8b767b4
No known key found for this signature in database
GPG Key ID: 8395A8BA109708B2
1 changed files with 28 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
passes/sat/qbfsat.cc
View File

@ -178,6 +178,29 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) {
} }
} }
void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) {
log("Satisfiable model:\n");
std::map<std::string, std::string> 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;
#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];
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.push_back(c == '1'? RTLIL::S1 : RTLIL::S0);
std::reverse(value_bv.begin(), value_bv.end());
}
}
void allconstify_inputs(RTLIL::Module *module, const std::set<std::string> &input_wires) { void allconstify_inputs(RTLIL::Module *module, const std::set<std::string> &input_wires) {
for (auto &n : input_wires) { for (auto &n : input_wires) {
RTLIL::Wire *input = module->wire(n); RTLIL::Wire *input = module->wire(n);
@ -242,6 +265,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
log_assert(mod->design != nullptr); log_assert(mod->design != nullptr);
#endif #endif
Pass::call(mod->design, smt2_command); Pass::call(mod->design, smt2_command);
log_header(mod->design, "Solving QBF-SAT problem.\n");
//Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]` //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]`
{ {
@ -445,6 +469,7 @@ struct QbfSatPass : public Pass {
if (module == NULL) if (module == NULL)
log_cmd_error("Can't perform QBF-SAT on an empty selection!\n"); log_cmd_error("Can't perform QBF-SAT on an empty selection!\n");
log_push();
if (!opt.specialize_from_file) { if (!opt.specialize_from_file) {
//Save the design to restore after modiyfing the current module. //Save the design to restore after modiyfing the current module.
std::string module_name = module->name.str(); std::string module_name = module->name.str();
@ -474,6 +499,8 @@ struct QbfSatPass : public Pass {
if (opt.specialize) { if (opt.specialize) {
specialize(module, ret); specialize(module, ret);
Pass::call(design, "opt_clean"); Pass::call(design, "opt_clean");
} else {
dump_model(module, ret);
} }
if (opt.unsat) if (opt.unsat)
log_cmd_error("expected problem to be UNSAT\n"); log_cmd_error("expected problem to be UNSAT\n");
@ -484,6 +511,7 @@ struct QbfSatPass : public Pass {
specialize_from_file(module, opt.specialize_soln_file); specialize_from_file(module, opt.specialize_soln_file);
Pass::call(design, "opt_clean"); Pass::call(design, "opt_clean");
} }
log_pop();
} }
} QbfSatPass; } QbfSatPass;