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

Implement `-write-solution` option for the `qbfsat` command.

This commit is contained in:
Alberto Gonzalez 2020-03-25 23:51:32 +00:00
parent d07ac2612b
commit b9e79e0bb7
No known key found for this signature in database
GPG Key ID: 8395A8BA109708B2
1 changed files with 28 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
passes/sat/qbfsat.cc
View File

@ -86,19 +86,35 @@ void recover_solution(QbfSolutionType &sol) {
log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true); log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true);
} }
void specialize(RTLIL::Module *module, const QbfSolutionType &ret) { std::map<std::string, std::string> get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) {
std::map<std::string, std::string> hole_loc_to_name; std::map<std::string, std::string> hole_loc_to_name;
for (auto cell : module->cells()) { for (auto cell : module->cells()) {
std::string cell_src = cell->get_src_attribute(); std::string cell_src = cell->get_src_attribute();
auto pos = ret.hole_to_value.find(cell_src); auto pos = sol.hole_to_value.find(cell_src);
if (pos != ret.hole_to_value.end()) { if (pos != sol.hole_to_value.end()) {
log_assert(cell->type.in("$anyconst", "$anyseq")); log_assert(cell->type.in("$anyconst", "$anyseq"));
log_assert(cell->hasPort(ID::Y)); log_assert(cell->hasPort(ID::Y));
log_assert(cell->getPort(ID::Y).is_wire()); log_assert(cell->getPort(ID::Y).is_wire());
hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str(); 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<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;
}
void specialize(RTLIL::Module *module, const QbfSolutionType &sol) {
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_loc = it.first;
std::string hole_value = it.second; std::string hole_value = it.second;
@ -389,9 +405,14 @@ struct QbfSatPass : public Pass {
else else
print_proof_failed(); print_proof_failed();
if (opt.specialize) { if(!ret.unknown && ret.sat) {
specialize(module, ret); if (opt.write_solution) {
Pass::call(design, "opt_clean"); write_solution(module, ret, opt.write_soln_soln_file);
}
if (opt.specialize) {
specialize(module, ret);
Pass::call(design, "opt_clean");
}
} }
} }
} QbfSatPass; } QbfSatPass;