From 8a8d444648bd1744c2598854367fd14d143aeb78 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 3 Jan 2014 16:54:59 +0100 Subject: [PATCH 01/10] Tiny cleanup in proc_mux.cc --- passes/proc/proc_mux.cc | 3 --- 1 file changed, 3 deletions(-) diff --git a/passes/proc/proc_mux.cc b/passes/proc/proc_mux.cc index c7121959a..9b2f83885 100644 --- a/passes/proc/proc_mux.cc +++ b/passes/proc/proc_mux.cc @@ -186,9 +186,6 @@ static void append_pmux(RTLIL::Module *mod, const RTLIL::SigSpec &signal, const assert(last_mux_cell != NULL); assert(when_signal.width == last_mux_cell->connections["\\A"].width); - std::stringstream sstr; - sstr << "$procmux$" << (RTLIL::autoidx++); - RTLIL::SigSpec ctrl_sig = gen_cmp(mod, signal, compare, sw); assert(ctrl_sig.width == 1); last_mux_cell->type = "$pmux"; From 7354a1718e2e3f2eec4843a56410743af0ff7a83 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 3 Jan 2014 17:30:50 +0100 Subject: [PATCH 02/10] Fixed SAT and ConstEval undef handling for $pmux and $safe_pmux --- kernel/consteval.h | 10 ++++++---- kernel/satgen.h | 43 +++++++++++++++++++++++++++++++++++++------ 2 files changed, 43 insertions(+), 10 deletions(-) diff --git a/kernel/consteval.h b/kernel/consteval.h index a424007ef..10116ccfe 100644 --- a/kernel/consteval.h +++ b/kernel/consteval.h @@ -110,6 +110,7 @@ struct ConstEval if (cell->type == "$mux" || cell->type == "$pmux" || cell->type == "$safe_pmux" || cell->type == "$_MUX_") { std::vector y_candidates; + int count_maybe_set_s_bits = 0; int count_set_s_bits = 0; for (int i = 0; i < sig_s.width; i++) @@ -120,16 +121,17 @@ struct ConstEval if (s_bit == RTLIL::State::Sx || s_bit == RTLIL::State::S1) y_candidates.push_back(b_slice); + if (s_bit == RTLIL::State::S1 || s_bit == RTLIL::State::Sx) + count_maybe_set_s_bits++; + if (s_bit == RTLIL::State::S1) count_set_s_bits++; } - if (cell->type == "$safe_pmux" && count_set_s_bits > 1) { + if (cell->type == "$safe_pmux" && count_set_s_bits > 1) y_candidates.clear(); - count_set_s_bits = 0; - } - if (count_set_s_bits == 0) + if ((cell->type == "$safe_pmux" && count_maybe_set_s_bits > 1) || count_set_s_bits == 0) y_candidates.push_back(sig_a); std::vector y_values; diff --git a/kernel/satgen.h b/kernel/satgen.h index 208ae1658..a668c73a4 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -318,14 +318,45 @@ struct SatGen std::vector undef_s = importUndefSigSpec(cell->connections.at("\\S"), timestep); std::vector undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep); - tmp = a; - for (size_t i = 0; i < s.size(); i++) { + int maybe_one_hot = ez->FALSE; + int maybe_many_hot = ez->FALSE; + + int sure_one_hot = ez->FALSE; + int sure_many_hot = ez->FALSE; + + std::vector bits_set = std::vector(undef_y.size(), ez->FALSE); + std::vector bits_clr = std::vector(undef_y.size(), ez->FALSE); + + for (size_t i = 0; i < s.size(); i++) + { + std::vector part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size()); std::vector part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size()); - tmp = ez->vec_ite(s.at(i), part_of_undef_b, tmp); + + int maybe_s = ez->OR(s.at(i), undef_s.at(i)); + int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i))); + + maybe_one_hot = ez->OR(maybe_one_hot, maybe_s); + maybe_many_hot = ez->OR(maybe_many_hot, ez->AND(maybe_one_hot, maybe_s)); + + sure_one_hot = ez->OR(sure_one_hot, sure_s); + sure_many_hot = ez->OR(sure_many_hot, ez->AND(sure_one_hot, sure_s)); + + bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b))), bits_set); + bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b))), bits_clr); } - tmp = ez->vec_ite(ez->onehot(s, true), tmp, cell->type == "$safe_pmux" ? a : std::vector(tmp.size(), ez->TRUE)); - tmp = ez->vec_ite(ez->expression(ezSAT::OpOr, undef_s), std::vector(tmp.size(), ez->TRUE), tmp); - ez->assume(ez->vec_eq(tmp, undef_y)); + + int maybe_a = ez->NOT(maybe_one_hot); + + if (cell->type == "$safe_pmux") { + maybe_a = ez->OR(maybe_a, maybe_many_hot); + bits_set = ez->vec_ite(sure_many_hot, ez->vec_or(a, undef_a), bits_set); + bits_clr = ez->vec_ite(sure_many_hot, ez->vec_or(ez->vec_not(a), undef_a), bits_clr); + } + + bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set); + bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr); + + ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y)); undefGating(y, yy, undef_y); } return true; From 03f0ab9de29aa3e396c1b1b3e62e6676de3946a3 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 3 Jan 2014 17:50:39 +0100 Subject: [PATCH 03/10] Cleanups in freduce command --- passes/sat/freduce.cc | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc index 893fe5167..23ab8a04a 100644 --- a/passes/sat/freduce.cc +++ b/passes/sat/freduce.cc @@ -441,8 +441,6 @@ struct FreduceWorker int bits_count = 0; std::map, std::vector> buckets; - buckets[std::vector()].push_back(RTLIL::SigBit(RTLIL::State::S0)); - buckets[std::vector()].push_back(RTLIL::SigBit(RTLIL::State::S1)); for (auto &batch : batches) { for (auto &bit : batch) @@ -464,6 +462,11 @@ struct FreduceWorker } log(" Sorted %d signal bits into %d buckets.\n", bits_count, int(buckets.size())); + if (buckets.count(std::vector()) != 0) { + buckets[std::vector()].push_back(RTLIL::SigBit(RTLIL::State::S0)); + buckets[std::vector()].push_back(RTLIL::SigBit(RTLIL::State::S1)); + } + std::vector> equiv; for (auto &bucket : buckets) { From 8f11eaaca6259e817df47d47df4acd8e77948d7f Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 3 Jan 2014 17:51:05 +0100 Subject: [PATCH 04/10] Added updating of RTLIL::autoidx to ilang frontend --- frontends/ilang/lexer.l | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/frontends/ilang/lexer.l b/frontends/ilang/lexer.l index d582d0413..fd842b3dc 100644 --- a/frontends/ilang/lexer.l +++ b/frontends/ilang/lexer.l @@ -25,6 +25,7 @@ %{ #include "kernel/rtlil.h" #include "parser.tab.h" +void update_autoidx(const char *p); %} %option yylineno @@ -68,7 +69,7 @@ [a-z]+ { return TOK_INVALID; } "\\"[^ \t\r\n]+ { rtlil_frontend_ilang_yylval.string = strdup(yytext); return TOK_ID; } -"$"[^ \t\r\n]+ { rtlil_frontend_ilang_yylval.string = strdup(yytext); return TOK_ID; } +"$"[^ \t\r\n]+ { rtlil_frontend_ilang_yylval.string = strdup(yytext); update_autoidx(yytext); return TOK_ID; } "."[0-9]+ { rtlil_frontend_ilang_yylval.string = strdup(yytext); return TOK_ID; } [0-9]+'[01xzm-]* { rtlil_frontend_ilang_yylval.string = strdup(yytext); return TOK_VALUE; } @@ -116,6 +117,27 @@ %% +void update_autoidx(const char *p) +{ + if (*p != '$') + return; + + while (*p) { + if (*(p++) != '$') + continue; + if ('0' <= *p && *p <= '9') { + const char *q = p; + while ('0' <= *q && *q <= '9') + q++; + if ((q - p) < 10) { + int idx = atoi(p); + if (idx > RTLIL::autoidx) + RTLIL::autoidx = idx; + } + } + } +} + // this is a hack to avoid the 'yyinput defined but not used' error msgs void *rtlil_frontend_ilang_avoid_input_warnings() { return (void*)&yyinput; From c44e1bec6d2a549abb9d56c98e41c23bc698e12d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 3 Jan 2014 18:17:28 +0100 Subject: [PATCH 05/10] More freduce cleanups --- passes/sat/freduce.cc | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc index 23ab8a04a..44c095d28 100644 --- a/passes/sat/freduce.cc +++ b/passes/sat/freduce.cc @@ -52,6 +52,22 @@ struct equiv_bit_t } }; +struct CountBitUsage +{ + SigMap &sigmap; + std::map &cache; + + CountBitUsage(SigMap &sigmap, std::map &cache) : sigmap(sigmap), cache(cache) { } + + void operator()(RTLIL::SigSpec &sig) + { + std::vector vec = sigmap(sig).to_sigbit_vector(); + for (auto &bit : vec) { + log("%s %d\n", log_signal(bit), cache[bit]++); + } + } +}; + struct FindReducedInputs { SigMap &sigmap; @@ -478,6 +494,9 @@ struct FreduceWorker worker.analyze(equiv); } + std::map bitusage; + module->rewrite_sigspecs(CountBitUsage(sigmap, bitusage)); + log(" Rewiring %d equivialent groups:\n", int(equiv.size())); int rewired_sigbits = 0; for (auto &grp : equiv) @@ -492,6 +511,11 @@ struct FreduceWorker continue; } + if (grp[i].bit.wire->port_id == 0 && bitusage[grp[i].bit] <= 1) { + log(" Skipping unused slave: %s\n", log_signal(grp[i].bit)); + continue; + } + log(" Connect slave%s: %s\n", grp[i].inverted ? " using inverter" : "", log_signal(grp[i].bit)); RTLIL::Cell *drv = drivers.at(grp[i].bit).first; From 10f45b8c8ebe612b5bd489cbecb7e778e63580de Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 3 Jan 2014 21:29:28 +0100 Subject: [PATCH 06/10] Performance improvements in freduce pass --- passes/sat/freduce.cc | 96 +++++++++++++++++++++++++++++++------------ 1 file changed, 69 insertions(+), 27 deletions(-) diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc index 44c095d28..5ff4311fb 100644 --- a/passes/sat/freduce.cc +++ b/passes/sat/freduce.cc @@ -59,12 +59,10 @@ struct CountBitUsage CountBitUsage(SigMap &sigmap, std::map &cache) : sigmap(sigmap), cache(cache) { } - void operator()(RTLIL::SigSpec &sig) - { + void operator()(RTLIL::SigSpec &sig) { std::vector vec = sigmap(sig).to_sigbit_vector(); - for (auto &bit : vec) { - log("%s %d\n", log_signal(bit), cache[bit]++); - } + for (auto &bit : vec) + cache[bit]++; } }; @@ -116,16 +114,16 @@ struct FindReducedInputs pi.insert(pi.end(), pi_set.begin(), pi_set.end()); } - void analyze(std::vector &reduced_inputs, RTLIL::SigBit output) + void analyze(std::vector &reduced_inputs, RTLIL::SigBit output, int prec) { if (verbose_level >= 1) - log(" Analyzing input cone for signal %s:\n", log_signal(output)); + log("[%2d%%] Analyzing input cone for signal %s:\n", prec, log_signal(output)); std::vector pi; register_cone(pi, output); if (verbose_level >= 1) - log(" Found %d input signals and %d cells.\n", int(pi.size()), int(ez_cells.size())); + log(" Found %d input signals and %d cells.\n", int(pi.size()), int(ez_cells.size())); satgen.setContext(&sigmap, "A"); int output_a = satgen.importSigSpec(output).front(); @@ -156,16 +154,16 @@ struct FindReducedInputs 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))) { if (verbose_level >= 2) - log(" Result for input %s: pass\n", log_signal(test_sig)); + log(" Result for input %s: pass\n", log_signal(test_sig)); reduced_inputs.push_back(pi[i]); } else { if (verbose_level >= 2) - log(" Result for input %s: strip\n", log_signal(test_sig)); + log(" Result for input %s: strip\n", log_signal(test_sig)); } } 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())); } }; @@ -235,25 +233,28 @@ struct PerformReduction out_inverted = std::vector(sat_out.size(), false); } - void analyze(std::vector> &results, std::map &results_map, std::vector &bucket, int level) + void analyze(std::vector> &results, std::map &results_map, std::vector &bucket, std::string indent1, std::string indent2) { + std::string indent = indent1 + indent2; + const char *indt = indent.c_str(); + if (bucket.size() <= 1) return; if (verbose_level == 1) - log("%*s Trying to shatter bucket with %d signals.\n", 2*level, "", int(bucket.size())); + log("%s Trying to shatter bucket with %d signals.\n", indt, int(bucket.size())); if (verbose_level > 1) { std::vector bucket_sigbits; for (int idx : bucket) bucket_sigbits.push_back(out_bits[idx]); - log("%*s Trying to shatter bucket with %d signals: %s\n", 2*level, "", int(bucket.size()), log_signal(RTLIL::SigSpec(bucket_sigbits).optimized())); + log("%s Trying to shatter bucket with %d signals: %s\n", indt, int(bucket.size()), log_signal(RTLIL::SigSpec(bucket_sigbits).optimized())); } - std::vector sat_list, sat_inv_list; + std::vector sat_set_list, sat_clr_list; for (int idx : bucket) { - sat_list.push_back(ez.AND(sat_out[idx], sat_def[idx])); - sat_inv_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 modelVars = sat_out; @@ -263,13 +264,47 @@ 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_list), ez.expression(ezSAT::OpOr, sat_inv_list))) + if (ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_set_list), ez.expression(ezSAT::OpOr, sat_clr_list))) { + int iter_count = 1; + + while (1) + { + sat_set_list.clear(); + sat_clr_list.clear(); + + std::vector sat_def_list; + + 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])); + } 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))) + break; + iter_count++; + } + + if (verbose_level >= 1) { + int count_set = 0, count_clr = 0, count_undef = 0; + for (int idx : bucket) + if (!model[sat_out.size() + idx]) + count_undef++; + else if (model[idx]) + count_set++; + else + count_clr++; + log("%s After %d iterations: %d set vs. %d clr vs %d undef\n", indt, iter_count, count_set, count_clr, count_undef); + } + if (verbose_level >= 2) { for (size_t i = 0; i < pi_bits.size(); i++) - log("%*s -> PI %c == %s\n", 2*level, "", model[2*sat_out.size() + i] ? '1' : '0', log_signal(pi_bits[i])); + log("%s -> PI %c == %s\n", indt, model[2*sat_out.size() + i] ? '1' : '0', log_signal(pi_bits[i])); for (int idx : bucket) - log("%*s -> OUT %c == %s%s\n", 2*level, "", model[sat_out.size() + idx] ? model[idx] ? '1' : '0' : 'x', + log("%s -> OUT %c == %s%s\n", indt, model[sat_out.size() + idx] ? model[idx] ? '1' : '0' : 'x', out_inverted.at(idx) ? "~" : "", log_signal(out_bits[idx])); } @@ -282,8 +317,8 @@ struct PerformReduction if (!model[sat_out.size() + idx] || !model[idx]) buckets_b.push_back(idx); } - analyze(results, results_map, buckets_a, level+1); - analyze(results, results_map, buckets_b, level+1); + analyze(results, results_map, buckets_a, indent1 + ".", indent2 + " "); + analyze(results, results_map, buckets_b, indent1 + "x", indent2 + " "); } else { @@ -300,7 +335,7 @@ struct PerformReduction if (undef_slaves.size() == bucket.size()) { if (verbose_level >= 1) - log("%*s Complex undef overlap. None of the signals covers the others.\n", 2*level, ""); + log("%s Complex undef overlap. None of the signals covers the others.\n", indt); // FIXME: We could try to further shatter a group with complex undef overlaps return; } @@ -309,7 +344,7 @@ struct PerformReduction out_depth[idx] = std::numeric_limits::max(); if (verbose_level >= 1) { - log("%*s Found %d equivialent signals:", 2*level, "", int(bucket.size())); + log("%s Found %d equivialent 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"); @@ -347,7 +382,7 @@ struct PerformReduction std::vector> results_buf; std::map results_map; - analyze(results_buf, results_map, bucket, 1); + analyze(results_buf, results_map, bucket, "", ""); for (auto &r : results_buf) { @@ -432,10 +467,13 @@ struct FreduceWorker ct.setup_internals(); ct.setup_stdcells(); + int bits_full_total = 0; std::vector> batches; for (auto &it : module->wires) - if (it.second->port_input) + if (it.second->port_input) { batches.push_back(sigmap(it.second).to_sigbit_set()); + bits_full_total += it.second->width; + } for (auto &it : module->cells) { if (ct.cell_known(it.second->type)) { std::set inputs, outputs; @@ -450,18 +488,21 @@ struct FreduceWorker for (auto &bit : outputs) drivers[bit] = drv; batches.push_back(outputs); + bits_full_total += outputs.size(); } if (inv_mode && it.second->type == "$_INV_") inv_pairs.insert(std::pair(sigmap(it.second->connections.at("\\A")), sigmap(it.second->connections.at("\\Y")))); } int bits_count = 0; + int bits_full_count = 0; std::map, std::vector> buckets; for (auto &batch : batches) { for (auto &bit : batch) if (bit.wire != NULL && design->selected(module, bit.wire)) goto found_selected_wire; + bits_full_count += batch.size(); continue; found_selected_wire: @@ -471,8 +512,9 @@ struct FreduceWorker FindReducedInputs infinder(sigmap, drivers); for (auto &bit : batch) { std::vector inputs; - infinder.analyze(inputs, bit); + infinder.analyze(inputs, bit, 100 * bits_full_count / bits_full_total); buckets[inputs].push_back(bit); + bits_full_count++; bits_count++; } } From b791af174eb468c983d2b7912a9ed51054d44514 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 4 Jan 2014 00:06:36 +0100 Subject: [PATCH 07/10] Improved freduce performance on const signals --- passes/sat/freduce.cc | 76 +++++++++++++++++++++++++++++++++++-------- 1 file 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 out_bits, pi_bits; std::vector out_inverted; std::vector out_depth; + int cone_size; int register_cone_worker(std::set &celldone, std::map &sigdepth, RTLIL::SigBit out) { @@ -209,8 +210,8 @@ struct PerformReduction return sigdepth[out]; } - PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set> &inv_pairs, std::vector &bits) : - sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(&ez, &sigmap), out_bits(bits) + PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set> &inv_pairs, std::vector &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(sat_out.size(), false); } + void analyze_const(std::vector> &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 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> &results, std::map &results_map, std::vector &bucket, std::string indent1, std::string indent2) { std::string indent = indent1 + indent2; @@ -374,7 +419,7 @@ struct PerformReduction } } - void analyze(std::vector> &results) + void analyze(std::vector> &results, int perc) { std::vector bucket; for (size_t i = 0; i < sat_out.size(); i++) @@ -382,7 +427,7 @@ struct PerformReduction std::vector> results_buf; std::map 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()) != 0) { - buckets[std::vector()].push_back(RTLIL::SigBit(RTLIL::State::S0)); - buckets[std::vector()].push_back(RTLIL::SigBit(RTLIL::State::S1)); - } - + int bucket_count = 0; std::vector> 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 bitusage; From bc541b47ea0ceb2556b54bd5310d11c1d77a5d3d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 4 Jan 2014 13:10:51 +0100 Subject: [PATCH 08/10] Improved performance of freduce input cone reduction --- passes/sat/freduce.cc | 101 ++++++++++++++++++++++++++++++++---------- 1 file changed, 78 insertions(+), 23 deletions(-) diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc index 9ccce167a..81250b000 100644 --- a/passes/sat/freduce.cc +++ b/passes/sat/freduce.cc @@ -75,12 +75,59 @@ struct FindReducedInputs std::set ez_cells; SatGen satgen; + std::map sat_pi; + std::vector sat_pi_uniq_bitvec; + FindReducedInputs(SigMap &sigmap, drivers_t &drivers) : sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap) { 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 &pi, std::set &sigdone, RTLIL::SigBit out) { if (out.wire == NULL) @@ -102,8 +149,10 @@ struct FindReducedInputs } for (auto &bit : drv.second) register_cone_worker(pi, sigdone, bit); - } else + } else { + register_pi_bit(out); pi.insert(out); + } } void register_cone(std::vector &pi, RTLIL::SigBit out) @@ -128,40 +177,46 @@ struct FindReducedInputs satgen.setContext(&sigmap, "A"); int output_a = satgen.importSigSpec(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"); int output_b = satgen.importSigSpec(output).front(); int output_undef_b = satgen.importUndefSigSpec(output).front(); - ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, satgen.importUndefSigSpec(pi)))); + + std::set unused_pi_idx; for (size_t i = 0; i < pi.size(); i++) + unused_pi_idx.insert(i); + + while (1) { - RTLIL::SigSpec test_sig(pi[i]); - RTLIL::SigSpec rest_sig(pi); - rest_sig.remove(i, 1); + std::vector model_pi_idx; + std::vector model_expr; + std::vector model; - int test_sig_a, test_sig_b; - std::vector rest_sig_a, rest_sig_b; + for (size_t i = 0; i < pi.size(); i++) + 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"); - test_sig_a = satgen.importSigSpec(test_sig).front(); - rest_sig_a = satgen.importSigSpec(rest_sig); + 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; - satgen.setContext(&sigmap, "B"); - test_sig_b = satgen.importSigSpec(test_sig).front(); - rest_sig_b = satgen.importSigSpec(rest_sig); - - 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))) { - if (verbose_level >= 2) - log(" Result for input %s: pass\n", log_signal(test_sig)); - reduced_inputs.push_back(pi[i]); - } else { - if (verbose_level >= 2) - log(" Result for input %s: strip\n", log_signal(test_sig)); - } + int found_count = 0; + for (size_t i = 0; i < model_pi_idx.size(); i++) + if (model[i]) { + if (verbose_level >= 2) + log(" Found relevant input: %s\n", log_signal(pi[model_pi_idx[i]])); + unused_pi_idx.erase(model_pi_idx[i]); + found_count++; + } + log_assert(found_count == 1); } + 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) log(" Reduced input cone contains %d inputs.\n", int(reduced_inputs.size())); } From a3d94bf88819ce3f0ffa161137a5549fc6d8490b Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 12 Jan 2014 21:04:42 +0100 Subject: [PATCH 09/10] Fixed typo in frontends/ast/simplify.cc --- frontends/ast/simplify.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 9b8ed7603..bc5dec7b9 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -1065,7 +1065,7 @@ skip_dynamic_range_lvalue_expansion:; { AstNode *buf = children[0]->clone(); while (buf->simplify(true, false, false, stage, width_hint, sign_hint)) { } - if (!buf->type == AST_CONSTANT) + if (buf->type != AST_CONSTANT) log_error("Failed to evaluate system function `%s' with non-constant value at %s:%d.\n", str.c_str(), filename.c_str(), linenum); RTLIL::Const arg_value = buf->bitsAsConst(); From 54275c61ee863ff2bb5fb20baae72fcce69b4bbf Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 14 Jan 2014 11:10:29 +0100 Subject: [PATCH 10/10] Added "opt_const -mux_undef" --- passes/opt/opt_const.cc | 76 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 71 insertions(+), 5 deletions(-) diff --git a/passes/opt/opt_const.cc b/passes/opt/opt_const.cc index 0ead97b4e..c5c159ae2 100644 --- a/passes/opt/opt_const.cc +++ b/passes/opt/opt_const.cc @@ -42,7 +42,7 @@ void replace_cell(RTLIL::Module *module, RTLIL::Cell *cell, std::string info, st did_something = true; } -void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool consume_x) +void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool consume_x, bool mux_undef) { if (!design->selected(module)) return; @@ -139,8 +139,16 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons cell->connections.erase("\\S"); goto next_cell; } + if (input.match("11 ")) ACTION_DO_Y(1); + if (input.match("00 ")) ACTION_DO_Y(0); + if (input.match("** ")) ACTION_DO_Y(x); if (input.match("01*")) ACTION_DO_Y(x); if (input.match("10*")) ACTION_DO_Y(x); + if (mux_undef) { + if (input.match("* ")) ACTION_DO("\\Y", input.extract(1, 1)); + if (input.match(" * ")) ACTION_DO("\\Y", input.extract(2, 1)); + if (input.match(" *")) ACTION_DO("\\Y", input.extract(2, 1)); + } } if (cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex") @@ -216,6 +224,51 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons } } + if (mux_undef && (cell->type == "$mux" || cell->type == "$pmux")) { + RTLIL::SigSpec new_a, new_b, new_s; + int width = cell->connections.at("\\A").width; + if ((cell->connections.at("\\A").is_fully_undef() && cell->connections.at("\\B").is_fully_undef()) || + cell->connections.at("\\S").is_fully_undef()) { + replace_cell(module, cell, "mux undef", "\\Y", cell->connections.at("\\A")); + goto next_cell; + } + for (int i = 0; i < cell->connections.at("\\S").width; i++) { + RTLIL::SigSpec old_b = cell->connections.at("\\B").extract(i*width, width); + RTLIL::SigSpec old_s = cell->connections.at("\\S").extract(i, 1); + if (old_b.is_fully_undef() || old_s.is_fully_undef()) + continue; + new_b.append(old_b); + new_s.append(old_s); + } + new_a = cell->connections.at("\\A"); + if (new_a.is_fully_undef() && new_s.width > 0) { + new_a = new_b.extract((new_s.width-1)*width, width); + new_b = new_b.extract(0, (new_s.width-1)*width); + new_s = new_s.extract(0, new_s.width-1); + } + if (new_s.width == 0) { + replace_cell(module, cell, "mux undef", "\\Y", new_a); + goto next_cell; + } + if (new_a == RTLIL::SigSpec(RTLIL::State::S0) && new_b == RTLIL::SigSpec(RTLIL::State::S1)) { + replace_cell(module, cell, "mux undef", "\\Y", new_s); + goto next_cell; + } + if (cell->connections.at("\\S").width != new_s.width) { + cell->connections.at("\\A") = new_a; + cell->connections.at("\\B") = new_b; + cell->connections.at("\\S") = new_s; + if (new_s.width > 1) { + cell->type = "$pmux"; + cell->parameters["\\S_WIDTH"] = new_s.width; + } else { + cell->type = "$mux"; + cell->parameters.erase("\\S_WIDTH"); + } + did_something = true; + } + } + #define FOLD_1ARG_CELL(_t) \ if (cell->type == "$" #_t) { \ RTLIL::SigSpec a = cell->connections["\\A"]; \ @@ -312,25 +365,38 @@ struct OptConstPass : public Pass { { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" opt_const [selection]\n"); + log(" opt_const [options] [selection]\n"); log("\n"); log("This pass performs const folding on internal cell types with constant inputs.\n"); log("\n"); + log(" -mux_undef\n"); + log(" remove 'undef' inputs from $mux, $pmux and $_MUX_ cells\n"); + log("\n"); } virtual void execute(std::vector args, RTLIL::Design *design) { + bool mux_undef = false; + log_header("Executing OPT_CONST pass (perform const folding).\n"); log_push(); - extra_args(args, 1, design); + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-mux_undef") { + mux_undef = true; + continue; + } + break; + } + extra_args(args, argidx, design); for (auto &mod_it : design->modules) do { do { did_something = false; - replace_const_cells(design, mod_it.second, false); + replace_const_cells(design, mod_it.second, false, mux_undef); } while (did_something); - replace_const_cells(design, mod_it.second, true); + replace_const_cells(design, mod_it.second, true, mux_undef); } while (did_something); log_pop();