aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat/freduce.cc
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat/freduce.cc')
-rw-r--r--passes/sat/freduce.cc85
1 files changed, 48 insertions, 37 deletions
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index fbca35861..77263f6a2 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -2,11 +2,11 @@
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
@@ -73,7 +73,7 @@ struct FindReducedInputs
SigMap &sigmap;
drivers_t &drivers;
- ezDefaultSAT ez;
+ ezSatPtr ez;
std::set<RTLIL::Cell*> ez_cells;
SatGen satgen;
@@ -81,7 +81,7 @@ struct FindReducedInputs
std::vector<int> sat_pi_uniq_bitvec;
FindReducedInputs(SigMap &sigmap, drivers_t &drivers) :
- sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap)
+ sigmap(sigmap), drivers(drivers), satgen(ez.get(), &sigmap)
{
satgen.model_undef = true;
}
@@ -104,30 +104,30 @@ struct FindReducedInputs
satgen.setContext(&sigmap, "A");
int sat_a = satgen.importSigSpec(bit).front();
- ez.assume(ez.NOT(satgen.importUndefSigSpec(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()));
+ 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.frozen_literal(stringf("uniq_%d", int(idx_bits)-1)));
+ sat_pi_uniq_bitvec.push_back(ez->frozen_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())));
+ 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.frozen_literal(stringf("p, falsei_%s", log_signal(bit)));
- ez.assume(ez.IFF(ez.XOR(sat_a, sat_b), sat_pi[bit]));
+ sat_pi[bit] = ez->frozen_literal(stringf("p, falsei_%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])));
+ 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]));
+ 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)
@@ -201,7 +201,7 @@ struct FindReducedInputs
model_expr.push_back(sat_pi.at(pi[i]));
}
- 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)))
+ 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)))
break;
int found_count = 0;
@@ -229,8 +229,9 @@ struct PerformReduction
SigMap &sigmap;
drivers_t &drivers;
std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs;
+ pool<SigBit> recursion_guard;
- ezDefaultSAT ez;
+ ezSatPtr ez;
SatGen satgen;
std::vector<int> sat_pi, sat_out, sat_def;
@@ -246,6 +247,15 @@ struct PerformReduction
if (sigdepth.count(out) != 0)
return sigdepth.at(out);
+ if (recursion_guard.count(out)) {
+ string loop_signals;
+ for (auto loop_bit : recursion_guard)
+ loop_signals += string(" ") + log_signal(loop_bit);
+ log_error("Found logic loop:%s\n", loop_signals.c_str());
+ }
+
+ recursion_guard.insert(out);
+
if (drivers.count(out) != 0) {
std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
if (celldone.count(drv.first) == 0) {
@@ -255,20 +265,21 @@ struct PerformReduction
}
int max_child_depth = 0;
for (auto &bit : drv.second)
- max_child_depth = std::max(register_cone_worker(celldone, sigdepth, bit), max_child_depth);
+ max_child_depth = max(register_cone_worker(celldone, sigdepth, bit), max_child_depth);
sigdepth[out] = max_child_depth + 1;
} else {
pi_bits.push_back(out);
sat_pi.push_back(satgen.importSigSpec(out).front());
- ez.assume(ez.NOT(satgen.importUndefSigSpec(out).front()));
+ ez->assume(ez->NOT(satgen.importUndefSigSpec(out).front()));
sigdepth[out] = 0;
}
+ recursion_guard.erase(out);
return sigdepth.at(out);
}
PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs, std::vector<RTLIL::SigBit> &bits, int cone_size) :
- sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(&ez, &sigmap), out_bits(bits), cone_size(cone_size)
+ sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(ez.get(), &sigmap), out_bits(bits), cone_size(cone_size)
{
satgen.model_undef = true;
@@ -278,15 +289,15 @@ struct PerformReduction
for (auto &bit : bits) {
out_depth.push_back(register_cone_worker(celldone, sigdepth, bit));
sat_out.push_back(satgen.importSigSpec(bit).front());
- sat_def.push_back(ez.NOT(satgen.importUndefSigSpec(bit).front()));
+ sat_def.push_back(ez->NOT(satgen.importUndefSigSpec(bit).front()));
}
if (inv_mode && cone_size > 0) {
- if (!ez.solve(sat_out, out_inverted, ez.expression(ezSAT::OpAnd, sat_def)))
+ if (!ez->solve(sat_out, out_inverted, ez->expression(ezSAT::OpAnd, sat_def)))
log_error("Solving for initial model failed!\n");
for (size_t i = 0; i < sat_out.size(); i++)
if (out_inverted.at(i))
- sat_out[i] = ez.NOT(sat_out[i]);
+ sat_out[i] = ez->NOT(sat_out[i]);
} else
out_inverted = std::vector<bool>(sat_out.size(), false);
}
@@ -296,8 +307,8 @@ struct PerformReduction
if (verbose_level == 1)
log(" Finding const value for %s.\n", log_signal(out_bits[idx]));
- bool can_be_set = ez.solve(ez.AND(sat_out[idx], sat_def[idx]));
- bool can_be_clr = ez.solve(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
+ bool can_be_set = ez->solve(ez->AND(sat_out[idx], sat_def[idx]));
+ bool can_be_clr = ez->solve(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx]));
log_assert(!can_be_set || !can_be_clr);
RTLIL::SigBit value(RTLIL::State::Sx);
@@ -355,8 +366,8 @@ struct PerformReduction
std::vector<int> sat_set_list, sat_clr_list;
for (int idx : bucket) {
- sat_set_list.push_back(ez.AND(sat_out[idx], sat_def[idx]));
- sat_clr_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
+ sat_set_list.push_back(ez->AND(sat_out[idx], sat_def[idx]));
+ sat_clr_list.push_back(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx]));
}
std::vector<int> modelVars = sat_out;
@@ -366,7 +377,7 @@ struct PerformReduction
if (verbose_level >= 2)
modelVars.insert(modelVars.end(), sat_pi.begin(), sat_pi.end());
- if (ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_set_list), ez.expression(ezSAT::OpOr, sat_clr_list)))
+ if (ez->solve(modelVars, model, ez->expression(ezSAT::OpOr, sat_set_list), ez->expression(ezSAT::OpOr, sat_clr_list)))
{
int iter_count = 1;
@@ -379,13 +390,13 @@ struct PerformReduction
for (int idx : bucket)
if (!model[sat_out.size() + idx]) {
- sat_set_list.push_back(ez.AND(sat_out[idx], sat_def[idx]));
- sat_clr_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
+ sat_set_list.push_back(ez->AND(sat_out[idx], sat_def[idx]));
+ sat_clr_list.push_back(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx]));
} else {
sat_def_list.push_back(sat_def[idx]);
}
- if (!ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_set_list), ez.expression(ezSAT::OpOr, sat_clr_list), ez.expression(ezSAT::OpAnd, sat_def_list)))
+ if (!ez->solve(modelVars, model, ez->expression(ezSAT::OpOr, sat_set_list), ez->expression(ezSAT::OpOr, sat_clr_list), ez->expression(ezSAT::OpAnd, sat_def_list)))
break;
iter_count++;
}
@@ -431,7 +442,7 @@ struct PerformReduction
for (int idx2 : bucket)
if (idx != idx2)
sat_def_list.push_back(sat_def[idx2]);
- if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list)))
+ if (ez->solve(ez->NOT(sat_def[idx]), ez->expression(ezSAT::OpOr, sat_def_list)))
undef_slaves.push_back(idx);
}
@@ -446,7 +457,7 @@ struct PerformReduction
out_depth[idx] = std::numeric_limits<int>::max();
if (verbose_level >= 1) {
- log("%s Found %d equivialent signals:", indt, int(bucket.size()));
+ log("%s Found %d equivalent signals:", indt, int(bucket.size()));
for (int idx : bucket)
log("%s%s%s", idx == bucket.front() ? " " : ", ", out_inverted[idx] ? "~" : "", log_signal(out_bits[idx]));
log("\n");
@@ -495,7 +506,7 @@ struct PerformReduction
std::vector<RTLIL::SigBit> r_sigbits;
for (int idx : r)
r_sigbits.push_back(out_bits[idx]);
- log(" Found group of %d equivialent signals: %s\n", int(r.size()), log_signal(r_sigbits));
+ log(" Found group of %d equivalent signals: %s\n", int(r.size()), log_signal(r_sigbits));
}
std::vector<int> undef_slaves;
@@ -505,7 +516,7 @@ struct PerformReduction
for (int idx2 : r)
if (idx != idx2)
sat_def_list.push_back(sat_def[idx2]);
- if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list)))
+ if (ez->solve(ez->NOT(sat_def[idx]), ez->expression(ezSAT::OpOr, sat_def_list)))
undef_slaves.push_back(idx);
}
@@ -681,7 +692,7 @@ struct FreduceWorker
if (!dump_prefix.empty())
dump();
- log(" Rewiring %d equivialent groups:\n", int(equiv.size()));
+ log(" Rewiring %d equivalent groups:\n", int(equiv.size()));
int rewired_sigbits = 0;
for (auto &grp : equiv)
{
@@ -755,7 +766,7 @@ struct FreducePass : public Pass {
log(" freduce [options] [selection]\n");
log("\n");
log("This pass performs functional reduction in the circuit. I.e. if two nodes are\n");
- log("equivialent, they are merged to one node and one of the redundant drivers is\n");
+ log("equivalent, they are merged to one node and one of the redundant drivers is\n");
log("disconnected. A subsequent call to 'clean' will remove the redundant drivers.\n");
log("\n");
log(" -v, -vv\n");
@@ -773,7 +784,7 @@ struct FreducePass : public Pass {
log(" operation. this is mostly used for debugging the freduce command.\n");
log("\n");
log("This pass is undef-aware, i.e. it considers don't-care values for detecting\n");
- log("equivialent nodes.\n");
+ log("equivalent nodes.\n");
log("\n");
log("All selected wires are considered for rewiring. The selected cells cover the\n");
log("circuit that is analyzed.\n");
@@ -787,7 +798,7 @@ struct FreducePass : public Pass {
inv_mode = false;
dump_prefix = std::string();
- log_header("Executing FREDUCE pass (perform functional reduction).\n");
+ log_header(design, "Executing FREDUCE pass (perform functional reduction).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
@@ -825,5 +836,5 @@ struct FreducePass : public Pass {
log("Rewired a total of %d signal bits.\n", bitcount);
}
} FreducePass;
-
+
PRIVATE_NAMESPACE_END
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-05 14:36:15 +0000