mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 05:19:11 +00:00
Code Activity

Improved performance of freduce input cone reduction

Browse source
This commit is contained in:
Clifford Wolf 2014-01-04 13:10:51 +01:00
parent b791af174e
commit bc541b47ea
1 changed files with 78 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

101
passes/sat/freduce.cc
View file

@ -75,12 +75,59 @@ struct FindReducedInputs
std::set<RTLIL::Cell*> ez_cells; std::set<RTLIL::Cell*> ez_cells;
SatGen satgen; SatGen satgen;
std::map<RTLIL::SigBit, int> sat_pi;
std::vector<int> sat_pi_uniq_bitvec;
FindReducedInputs(SigMap &sigmap, drivers_t &drivers) : FindReducedInputs(SigMap &sigmap, drivers_t &drivers) :
sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap) sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap)
{ {
satgen.model_undef = true; satgen.model_undef = true;
} }
int get_bits(int val)
{
int bits = 0;
for (int i = 8*sizeof(int); val; i = i >> 1)
if (val >> (i-1)) {
bits += i;
val = val >> i;
}
return bits;
}
void register_pi_bit(RTLIL::SigBit bit)
{
if (sat_pi.count(bit) != 0)
return;
satgen.setContext(&sigmap, "A");
int sat_a = satgen.importSigSpec(bit).front();
ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front()));
satgen.setContext(&sigmap, "B");
int sat_b = satgen.importSigSpec(bit).front();
ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front()));
int idx = sat_pi.size();
size_t idx_bits = get_bits(idx);
if (sat_pi_uniq_bitvec.size() != idx_bits) {
sat_pi_uniq_bitvec.push_back(ez.literal(stringf("uniq_%d", int(idx_bits)-1)));
for (auto &it : sat_pi)
ez.assume(ez.OR(ez.NOT(it.second), ez.NOT(sat_pi_uniq_bitvec.back())));
}
log_assert(sat_pi_uniq_bitvec.size() == idx_bits);
sat_pi[bit] = ez.literal(stringf("pi_%s", log_signal(bit)));
ez.assume(ez.IFF(ez.XOR(sat_a, sat_b), sat_pi[bit]));
for (size_t i = 0; i < idx_bits; i++)
if ((idx & (1 << i)) == 0)
ez.assume(ez.OR(ez.NOT(sat_pi[bit]), ez.NOT(sat_pi_uniq_bitvec[i])));
else
ez.assume(ez.OR(ez.NOT(sat_pi[bit]), sat_pi_uniq_bitvec[i]));
}
void register_cone_worker(std::set<RTLIL::SigBit> &pi, std::set<RTLIL::SigBit> &sigdone, RTLIL::SigBit out) void register_cone_worker(std::set<RTLIL::SigBit> &pi, std::set<RTLIL::SigBit> &sigdone, RTLIL::SigBit out)
{ {
if (out.wire == NULL) if (out.wire == NULL)
@ -102,8 +149,10 @@ struct FindReducedInputs
} }
for (auto &bit : drv.second) for (auto &bit : drv.second)
register_cone_worker(pi, sigdone, bit); register_cone_worker(pi, sigdone, bit);
} else } else {
register_pi_bit(out);
pi.insert(out); pi.insert(out);
}
} }
void register_cone(std::vector<RTLIL::SigBit> &pi, RTLIL::SigBit out) void register_cone(std::vector<RTLIL::SigBit> &pi, RTLIL::SigBit out)
@ -128,40 +177,46 @@ struct FindReducedInputs
satgen.setContext(&sigmap, "A"); satgen.setContext(&sigmap, "A");
int output_a = satgen.importSigSpec(output).front(); int output_a = satgen.importSigSpec(output).front();
int output_undef_a = satgen.importUndefSigSpec(output).front(); int output_undef_a = satgen.importUndefSigSpec(output).front();
ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, satgen.importUndefSigSpec(pi))));
satgen.setContext(&sigmap, "B"); satgen.setContext(&sigmap, "B");
int output_b = satgen.importSigSpec(output).front(); int output_b = satgen.importSigSpec(output).front();
int output_undef_b = satgen.importUndefSigSpec(output).front(); int output_undef_b = satgen.importUndefSigSpec(output).front();
ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, satgen.importUndefSigSpec(pi))));
std::set<int> unused_pi_idx;
for (size_t i = 0; i < pi.size(); i++) for (size_t i = 0; i < pi.size(); i++)
unused_pi_idx.insert(i);
while (1)
{ {
RTLIL::SigSpec test_sig(pi[i]); std::vector<int> model_pi_idx;
RTLIL::SigSpec rest_sig(pi); std::vector<int> model_expr;
rest_sig.remove(i, 1); std::vector<bool> model;
int test_sig_a, test_sig_b; for (size_t i = 0; i < pi.size(); i++)
std::vector<int> rest_sig_a, rest_sig_b; if (unused_pi_idx.count(i) != 0) {
model_pi_idx.push_back(i);
model_expr.push_back(sat_pi.at(pi[i]));
}
satgen.setContext(&sigmap, "A"); if (!ez.solve(model_expr, model, ez.expression(ezSAT::OpOr, model_expr), ez.XOR(output_a, output_b), ez.NOT(output_undef_a), ez.NOT(output_undef_b)))
test_sig_a = satgen.importSigSpec(test_sig).front(); break;
rest_sig_a = satgen.importSigSpec(rest_sig);
satgen.setContext(&sigmap, "B"); int found_count = 0;
test_sig_b = satgen.importSigSpec(test_sig).front(); for (size_t i = 0; i < model_pi_idx.size(); i++)
rest_sig_b = satgen.importSigSpec(rest_sig); if (model[i]) {
if (verbose_level >= 2)
if (ez.solve(ez.vec_eq(rest_sig_a, rest_sig_b), ez.XOR(output_a, output_b), ez.XOR(test_sig_a, test_sig_b), ez.NOT(output_undef_a), ez.NOT(output_undef_b))) { log(" Found relevant input: %s\n", log_signal(pi[model_pi_idx[i]]));
if (verbose_level >= 2) unused_pi_idx.erase(model_pi_idx[i]);
log(" Result for input %s: pass\n", log_signal(test_sig)); found_count++;
reduced_inputs.push_back(pi[i]); }
} else { log_assert(found_count == 1);
if (verbose_level >= 2)
log(" Result for input %s: strip\n", log_signal(test_sig));
}
} }
for (size_t i = 0; i < pi.size(); i++)
if (unused_pi_idx.count(i) == 0)
reduced_inputs.push_back(pi[i]);
if (verbose_level >= 1) if (verbose_level >= 1)
log(" Reduced input cone contains %d inputs.\n", int(reduced_inputs.size())); log(" Reduced input cone contains %d inputs.\n", int(reduced_inputs.size()));
} }