diff options
| author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-03-27 23:25:24 +0000 |
|---|---|---|
| committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-04-04 22:13:26 +0000 |
| commit | d311a8022292a9934c11ff9124a53932469974e6 (patch) | |
| tree | ceaf58260e5292accd676dc5362f56eb671142a9 /passes/sat/qbfsat.cc | |
| parent | 125a583c575747e07530b214c922ff6a17c5bb34 (diff) | |
| download | yosys-d311a8022292a9934c11ff9124a53932469974e6.tar.gz yosys-d311a8022292a9934c11ff9124a53932469974e6.tar.bz2 yosys-d311a8022292a9934c11ff9124a53932469974e6.zip | |
Clean up `qbfsat` command and fix AND-reduction of miter outputs.
Diffstat (limited to 'passes/sat/qbfsat.cc')
| -rw-r--r-- | passes/sat/qbfsat.cc | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 3db84a579..2861ae452 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -198,10 +198,9 @@ void allconstify_inputs(RTLIL::Module *module, const std::set<std::string> &inpu void assume_miter_outputs(RTLIL::Module *module) { std::vector<RTLIL::Wire *> wires_to_assume; for (auto w : module->wires()) - if (w->port_output) { - if (w->width == 1) - wires_to_assume.push_back(w); - } + if (w->port_output && w->width == 1) + wires_to_assume.push_back(w); + if (wires_to_assume.size() == 0) return; else { @@ -211,16 +210,19 @@ void assume_miter_outputs(RTLIL::Module *module) { log("\n"); } - std::vector<RTLIL::Wire *>::size_type i; + unsigned long i = 0; while (wires_to_assume.size() > 1) { std::vector<RTLIL::Wire *> buf; - for (i = 0; i + 1 < wires_to_assume.size(); i += 2) { - std::stringstream strstr; strstr << i; + for (auto j = 0; j + 1 < GetSize(wires_to_assume); j += 2) { + std::stringstream strstr; strstr << i << "_" << j; RTLIL::Wire *and_wire = module->addWire("\\_qbfsat_and_" + strstr.str(), 1); - module->addLogicAnd("$_qbfsat_and_" + strstr.str(), wires_to_assume[i], wires_to_assume[i+1], and_wire, false, wires_to_assume[i]->get_src_attribute()); + module->addLogicAnd("$_qbfsat_and_" + strstr.str(), wires_to_assume[j], wires_to_assume[j+1], and_wire, false, wires_to_assume[j]->get_src_attribute()); buf.push_back(and_wire); } + if (wires_to_assume.size() % 2 == 1) + buf.push_back(wires_to_assume[wires_to_assume.size() - 1]); wires_to_assume.swap(buf); + ++i; } #ifndef NDEBUG |