mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 04:28:18 +00:00
Code Activity

Clean up qbfsat command and fix AND-reduction of miter outputs.

Browse source
This commit is contained in:
Alberto Gonzalez 2020-03-27 23:25:24 +00:00
parent 125a583c57
commit d311a80222
No known key found for this signature in database
GPG key ID: 8395A8BA109708B2
1 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
passes/sat/qbfsat.cc
View file

@ -198,10 +198,9 @@ void allconstify_inputs(RTLIL::Module *module, const std::set<std::string> &inpu
void assume_miter_outputs(RTLIL::Module *module) { void assume_miter_outputs(RTLIL::Module *module) {
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) { if (w->port_output && w->width == 1)
if (w->width == 1) wires_to_assume.push_back(w);
wires_to_assume.push_back(w);
}
if (wires_to_assume.size() == 0) if (wires_to_assume.size() == 0)
return; return;
else { else {
@ -211,16 +210,19 @@ void assume_miter_outputs(RTLIL::Module *module) {
log("\n"); log("\n");
} }
std::vector<RTLIL::Wire *>::size_type i; unsigned long i = 0;
while (wires_to_assume.size() > 1) { while (wires_to_assume.size() > 1) {
std::vector<RTLIL::Wire *> buf; std::vector<RTLIL::Wire *> buf;
for (i = 0; i + 1 < wires_to_assume.size(); i += 2) { for (auto j = 0; j + 1 < GetSize(wires_to_assume); j += 2) {
std::stringstream strstr; strstr << i; std::stringstream strstr; strstr << i << "_" << j;
RTLIL::Wire *and_wire = module->addWire("\\_qbfsat_and_" + strstr.str(), 1); 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); 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); wires_to_assume.swap(buf);
++i;
} }
#ifndef NDEBUG #ifndef NDEBUG