diff options
author | Clifford Wolf <clifford@clifford.at> | 2014-01-04 00:06:36 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2014-01-04 00:06:36 +0100 |
commit | b791af174eb468c983d2b7912a9ed51054d44514 (patch) | |
tree | 83cc85b32942826c3f458dab29d0c8d838286fff /passes/sat | |
parent | 10f45b8c8ebe612b5bd489cbecb7e778e63580de (diff) | |
download | yosys-b791af174eb468c983d2b7912a9ed51054d44514.tar.gz yosys-b791af174eb468c983d2b7912a9ed51054d44514.tar.bz2 yosys-b791af174eb468c983d2b7912a9ed51054d44514.zip |
Improved freduce performance on const signals
Diffstat (limited to 'passes/sat')
-rw-r--r-- | passes/sat/freduce.cc | 76 |
1 files changed, 63 insertions, 13 deletions
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc index 5ff4311fb..9ccce167a 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; |