summaryrefslogtreecommitdiff
path: root/passes/sat
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-01-04 00:06:36 +0100
committerClifford Wolf <clifford@clifford.at>2014-01-04 00:06:36 +0100
commitb791af174eb468c983d2b7912a9ed51054d44514 (patch)
tree83cc85b32942826c3f458dab29d0c8d838286fff /passes/sat
parent10f45b8c8ebe612b5bd489cbecb7e778e63580de (diff)
Improved freduce performance on const signals
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/freduce.cc76
1 files changed, 63 insertions, 13 deletions
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index 5ff4311f..9ccce167 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -180,6 +180,7 @@ struct PerformReduction
std::vector<RTLIL::SigBit> out_bits, pi_bits;
std::vector<bool> out_inverted;
std::vector<int> out_depth;
+ int cone_size;
int register_cone_worker(std::set<RTLIL::Cell*> &celldone, std::map<RTLIL::SigBit, int> &sigdepth, RTLIL::SigBit out)
{
@@ -209,8 +210,8 @@ struct PerformReduction
return sigdepth[out];
}
- PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs, std::vector<RTLIL::SigBit> &bits) :
- sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(&ez, &sigmap), out_bits(bits)
+ 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)
{
satgen.model_undef = true;
@@ -223,7 +224,7 @@ struct PerformReduction
sat_def.push_back(ez.NOT(satgen.importUndefSigSpec(bit).front()));
}
- if (inv_mode) {
+ if (inv_mode && cone_size > 0) {
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++)
@@ -233,6 +234,50 @@ struct PerformReduction
out_inverted = std::vector<bool>(sat_out.size(), false);
}
+ void analyze_const(std::vector<std::vector<equiv_bit_t>> &results, int idx)
+ {
+ 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]));
+ log_assert(!can_be_set || !can_be_clr);
+
+ RTLIL::SigBit value(RTLIL::State::Sx);
+ if (can_be_set)
+ value = RTLIL::State::S1;
+ if (can_be_clr)
+ value = RTLIL::State::S0;
+ if (verbose_level == 1)
+ log(" Constant value for this signal: %s\n", log_signal(value));
+
+ int result_idx = -1;
+ for (size_t i = 0; i < results.size(); i++) {
+ if (results[i].front().bit == value) {
+ result_idx = i;
+ break;
+ }
+ }
+
+ if (result_idx == -1) {
+ result_idx = results.size();
+ results.push_back(std::vector<equiv_bit_t>());
+ equiv_bit_t bit;
+ bit.depth = 0;
+ bit.inverted = false;
+ bit.drv = NULL;
+ bit.bit = value;
+ results.back().push_back(bit);
+ }
+
+ equiv_bit_t bit;
+ bit.depth = 1;
+ bit.inverted = false;
+ bit.drv = drivers.count(out_bits[idx]) ? drivers.at(out_bits[idx]).first : NULL;
+ bit.bit = out_bits[idx];
+ results[result_idx].push_back(bit);
+ }
+
void analyze(std::vector<std::set<int>> &results, std::map<int, int> &results_map, std::vector<int> &bucket, std::string indent1, std::string indent2)
{
std::string indent = indent1 + indent2;
@@ -374,7 +419,7 @@ struct PerformReduction
}
}
- void analyze(std::vector<std::vector<equiv_bit_t>> &results)
+ void analyze(std::vector<std::vector<equiv_bit_t>> &results, int perc)
{
std::vector<int> bucket;
for (size_t i = 0; i < sat_out.size(); i++)
@@ -382,7 +427,7 @@ struct PerformReduction
std::vector<std::set<int>> results_buf;
std::map<int, int> results_map;
- analyze(results_buf, results_map, bucket, "", "");
+ analyze(results_buf, results_map, bucket, stringf("[%2d%%] %d ", perc, cone_size), "");
for (auto &r : results_buf)
{
@@ -520,20 +565,25 @@ struct FreduceWorker
}
log(" Sorted %d signal bits into %d buckets.\n", bits_count, int(buckets.size()));
- if (buckets.count(std::vector<RTLIL::SigBit>()) != 0) {
- buckets[std::vector<RTLIL::SigBit>()].push_back(RTLIL::SigBit(RTLIL::State::S0));
- buckets[std::vector<RTLIL::SigBit>()].push_back(RTLIL::SigBit(RTLIL::State::S1));
- }
-
+ int bucket_count = 0;
std::vector<std::vector<equiv_bit_t>> equiv;
for (auto &bucket : buckets)
{
+ bucket_count++;
+
if (bucket.second.size() == 1)
continue;
- log(" Trying to shatter bucket %s%c\n", log_signal(RTLIL::SigSpec(bucket.second).optimized()), verbose_level ? ':' : '.');
- PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second);
- worker.analyze(equiv);
+ if (bucket.first.size() == 0) {
+ log(" Finding const values for bucket %s%c\n", log_signal(RTLIL::SigSpec(bucket.second).optimized()), verbose_level ? ':' : '.');
+ PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second, bucket.first.size());
+ for (size_t idx = 0; idx < bucket.second.size(); idx++)
+ worker.analyze_const(equiv, idx);
+ } else {
+ log(" Trying to shatter bucket %s%c\n", log_signal(RTLIL::SigSpec(bucket.second).optimized()), verbose_level ? ':' : '.');
+ PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second, bucket.first.size());
+ worker.analyze(equiv, 100 * bucket_count / (buckets.size() + 1));
+ }
}
std::map<RTLIL::SigBit, int> bitusage;