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

Merge pull request #1988 from boqwxp/qbfsat 

qbfsat: Add `-assume-negative-polarity` option.
This commit is contained in:
Claire Wolf 2020-04-23 11:33:54 +02:00 committed by GitHub
parent ca31027fe1 7369e6b26b
commit 1797c574da
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 22 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
passes/sat/qbfsat.cc
View File

@ -49,15 +49,15 @@ struct QbfSolutionType {
}; };
struct QbfSolveOptions { struct QbfSolveOptions {
bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs; bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg;
bool sat, unsat, show_smtbmc; bool sat, unsat, show_smtbmc;
std::string specialize_soln_file; std::string specialize_soln_file;
std::string write_soln_soln_file; std::string write_soln_soln_file;
std::string dump_final_smt2_file; std::string dump_final_smt2_file;
size_t argidx; size_t argidx;
QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false), QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
nocleanup(false), dump_final_smt2(false), assume_outputs(false), sat(false), unsat(false), nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false),
show_smtbmc(false), argidx(0) {}; sat(false), unsat(false), show_smtbmc(false), argidx(0) {};
}; };
void recover_solution(QbfSolutionType &sol) { void recover_solution(QbfSolutionType &sol) {
@ -242,7 +242,7 @@ void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wi
module->fixup_ports(); module->fixup_ports();
} }
void assume_miter_outputs(RTLIL::Module *module) { void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
std::vector<RTLIL::Wire *> wires_to_assume; std::vector<RTLIL::Wire *> wires_to_assume;
for (auto w : module->wires()) for (auto w : module->wires())
if (w->port_output && w->width == 1) if (w->port_output && w->width == 1)
@ -257,7 +257,14 @@ void assume_miter_outputs(RTLIL::Module *module) {
log("\n"); log("\n");
} }
for(auto i = 0; wires_to_assume.size() > 1; ++i) { if (opt.assume_neg) {
for (unsigned int i = 0; i < wires_to_assume.size(); ++i) {
RTLIL::SigSpec n_wire = module->LogicNot(wires_to_assume[i]->name.str() + "__n__qbfsat", wires_to_assume[i], false, wires_to_assume[i]->get_src_attribute());
wires_to_assume[i] = n_wire.as_wire();
}
}
for (auto i = 0; wires_to_assume.size() > 1; ++i) {
std::vector<RTLIL::Wire *> buf; std::vector<RTLIL::Wire *> buf;
for (auto j = 0; j + 1 < GetSize(wires_to_assume); j += 2) { for (auto j = 0; j + 1 < GetSize(wires_to_assume); j += 2) {
std::stringstream strstr; strstr << i << "_" << j; std::stringstream strstr; strstr << i << "_" << j;
@ -371,6 +378,10 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
opt.assume_outputs = true; opt.assume_outputs = true;
continue; continue;
} }
else if (args[opt.argidx] == "-assume-negative-polarity") {
opt.assume_neg = true;
continue;
}
else if (args[opt.argidx] == "-sat") { else if (args[opt.argidx] == "-sat") {
opt.sat = true; opt.sat = true;
continue; continue;
@ -464,6 +475,11 @@ struct QbfSatPass : public Pass {
log(" -assume-outputs\n"); log(" -assume-outputs\n");
log(" Add an $assume cell for the conjunction of all one-bit module output wires.\n"); log(" Add an $assume cell for the conjunction of all one-bit module output wires.\n");
log("\n"); log("\n");
log(" -assume-negative-polarity\n");
log(" When adding $assume cells for one-bit module output wires, assume they are\n");
log(" negative polarity signals and should always be low, for example like the\n");
log(" miters created with the `miter` command.\n");
log("\n");
log(" -sat\n"); log(" -sat\n");
log(" Generate an error if the solver does not return \"sat\".\n"); log(" Generate an error if the solver does not return \"sat\".\n");
log("\n"); log("\n");
@ -512,7 +528,7 @@ struct QbfSatPass : public Pass {
pool<std::string> input_wires = validate_design_and_get_inputs(module, opt); pool<std::string> input_wires = validate_design_and_get_inputs(module, opt);
allconstify_inputs(module, input_wires); allconstify_inputs(module, input_wires);
if (opt.assume_outputs) if (opt.assume_outputs)
assume_miter_outputs(module); assume_miter_outputs(module, opt);
QbfSolutionType ret = qbf_solve(module, opt); QbfSolutionType ret = qbf_solve(module, opt);
Pass::call(design, "design -pop"); Pass::call(design, "design -pop");