diff --git a/passes/opt/share.cc b/passes/opt/share.cc index 0820bad12..1d7ba7d98 100644 --- a/passes/opt/share.cc +++ b/passes/opt/share.cc @@ -1000,6 +1000,61 @@ struct ShareWorker } } + pool> pattern_bits(const pool &activation_patterns) + { + pool> bits; + for (auto const &pattern : activation_patterns) { + for (int i = 0; i < GetSize(pattern.second); ++i) { + SigBit bit = pattern.first[i]; + State val = pattern.second[i]; + bits.emplace(bit, val); + } + } + return bits; + } + + bool onesided_restrict_activation_patterns( + pool &activation_patterns, const pool> &other_bits) + { + pool new_activation_patterns; + + bool simplified = false; + + for (auto const &pattern : activation_patterns) { + ssc_pair_t new_pair; + for (int i = 0; i < GetSize(pattern.second); ++i) { + SigBit bit = pattern.first[i]; + State val = pattern.second[i]; + if (other_bits.count({bit, val == State::S0 ? State::S1 : State::S0})) { + new_pair.first.append(bit); + new_pair.second.append(val); + } else { + simplified = true; + } + } + new_activation_patterns.emplace(std::move(new_pair)); + } + + activation_patterns = std::move(new_activation_patterns); + return simplified; + } + + // Only valid if the patterns on their own (i.e. without considering their input cone) are mutually exclusive! + bool restrict_activation_patterns(pool &activation_patterns, pool &other_activation_patterns) + { + pool> bits = pattern_bits(activation_patterns); + pool> other_bits = pattern_bits(other_activation_patterns); + + bool simplified = false; + simplified |= onesided_restrict_activation_patterns(activation_patterns, other_bits); + simplified |= onesided_restrict_activation_patterns(other_activation_patterns, bits); + + optimize_activation_patterns(activation_patterns); + optimize_activation_patterns(other_activation_patterns); + + return simplified; + } + RTLIL::SigSpec make_cell_activation_logic(const pool &activation_patterns, pool &supercell_aux) { RTLIL::Wire *all_cases_wire = module->addWire(NEW_ID, 0); @@ -1299,17 +1354,18 @@ struct ShareWorker other_cell_active.push_back(qcsat.ez->vec_eq(qcsat.importSig(p.first), qcsat.importSig(p.second))); all_ctrl_signals.append(p.first); } + int sub1 = qcsat.ez->expression(qcsat.ez->OpOr, cell_active); + int sub2 = qcsat.ez->expression(qcsat.ez->OpOr, other_cell_active); + bool pattern_only_solve = qcsat.ez->solve(qcsat.ez->AND(sub1, sub2)); qcsat.prepare(); - int sub1 = qcsat.ez->expression(qcsat.ez->OpOr, cell_active); if (!qcsat.ez->solve(sub1)) { log(" According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(cell)); cells_to_remove.insert(cell); break; } - int sub2 = qcsat.ez->expression(qcsat.ez->OpOr, other_cell_active); if (!qcsat.ez->solve(sub2)) { log(" According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(other_cell)); cells_to_remove.insert(other_cell); @@ -1317,28 +1373,43 @@ struct ShareWorker continue; } - qcsat.ez->non_incremental(); + pool optimized_cell_activation_patterns = filtered_cell_activation_patterns; + pool optimized_other_cell_activation_patterns = filtered_other_cell_activation_patterns; - all_ctrl_signals.sort_and_unify(); - std::vector sat_model = qcsat.importSig(all_ctrl_signals); - std::vector sat_model_values; + if (pattern_only_solve) { + qcsat.ez->non_incremental(); - qcsat.ez->assume(qcsat.ez->AND(sub1, sub2)); + all_ctrl_signals.sort_and_unify(); + std::vector sat_model = qcsat.importSig(all_ctrl_signals); + std::vector sat_model_values; - log(" Size of SAT problem: %zu cells, %d variables, %d clauses\n", - qcsat.imported_cells.size(), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses()); + qcsat.ez->assume(qcsat.ez->AND(sub1, sub2)); - if (qcsat.ez->solve(sat_model, sat_model_values)) { - log(" According to the SAT solver this pair of cells can not be shared.\n"); - log(" Model from SAT solver: %s = %d'", log_signal(all_ctrl_signals), GetSize(sat_model_values)); - for (int i = GetSize(sat_model_values)-1; i >= 0; i--) - log("%c", sat_model_values[i] ? '1' : '0'); - log("\n"); - continue; + log(" Size of SAT problem: %zu cells, %d variables, %d clauses\n", + qcsat.imported_cells.size(), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses()); + + if (qcsat.ez->solve(sat_model, sat_model_values)) { + log(" According to the SAT solver this pair of cells can not be shared.\n"); + log(" Model from SAT solver: %s = %d'", log_signal(all_ctrl_signals), GetSize(sat_model_values)); + for (int i = GetSize(sat_model_values)-1; i >= 0; i--) + log("%c", sat_model_values[i] ? '1' : '0'); + log("\n"); + continue; + } + + log(" According to the SAT solver this pair of cells can be shared.\n"); + } else { + log(" According to the SAT solver this pair of cells can be shared. (Pattern only case)\n"); + + if (restrict_activation_patterns(optimized_cell_activation_patterns, optimized_other_cell_activation_patterns)) { + for (auto &p : optimized_cell_activation_patterns) + log(" Simplified activation pattern for cell %s: %s = %s\n", log_id(cell), log_signal(p.first), log_signal(p.second)); + + for (auto &p : optimized_other_cell_activation_patterns) + log(" Simplified activation pattern for cell %s: %s = %s\n", log_id(other_cell), log_signal(p.first), log_signal(p.second)); + } } - log(" According to the SAT solver this pair of cells can be shared.\n"); - if (find_in_input_cone(cell, other_cell)) { log(" Sharing not possible: %s is in input cone of %s.\n", log_id(other_cell), log_id(cell)); continue; @@ -1354,20 +1425,20 @@ struct ShareWorker int cell_select_score = 0; int other_cell_select_score = 0; - for (auto &p : filtered_cell_activation_patterns) + for (auto &p : optimized_cell_activation_patterns) cell_select_score += p.first.size(); - for (auto &p : filtered_other_cell_activation_patterns) + for (auto &p : optimized_other_cell_activation_patterns) other_cell_select_score += p.first.size(); RTLIL::Cell *supercell; pool supercell_aux; if (cell_select_score <= other_cell_select_score) { - RTLIL::SigSpec act = make_cell_activation_logic(filtered_cell_activation_patterns, supercell_aux); + RTLIL::SigSpec act = make_cell_activation_logic(optimized_cell_activation_patterns, supercell_aux); supercell = make_supercell(cell, other_cell, act, supercell_aux); log(" Activation signal for %s: %s\n", log_id(cell), log_signal(act)); } else { - RTLIL::SigSpec act = make_cell_activation_logic(filtered_other_cell_activation_patterns, supercell_aux); + RTLIL::SigSpec act = make_cell_activation_logic(optimized_other_cell_activation_patterns, supercell_aux); supercell = make_supercell(other_cell, cell, act, supercell_aux); log(" Activation signal for %s: %s\n", log_id(other_cell), log_signal(act)); } diff --git a/tests/sat/share.v b/tests/sat/share.v index e06fc8f1e..29e423137 100644 --- a/tests/sat/share.v +++ b/tests/sat/share.v @@ -30,3 +30,26 @@ module test_2( end endmodule + +module test_3( + input [3:0] s, + input [7:0] a, b, c, + output reg [7:0] y0, + output reg [7:0] y1, + output reg [7:0] y2, + output reg [7:0] y3, +); + wire is_onehot = s & (s - 1); + + always @* begin + y0 <= 0; + y1 <= 0; + y2 <= 0; + y3 <= 0; + if (s < 3) y0 <= b / c; + if (3 <= s && s < 6) y1 <= c / b; + if (6 <= s && s < 9) y2 <= a / b; + if (9 <= s && s < 12) y3 <= b / a; + end +endmodule + diff --git a/tests/sat/share.ys b/tests/sat/share.ys index f2f5d649d..ef88d55c3 100644 --- a/tests/sat/share.ys +++ b/tests/sat/share.ys @@ -3,11 +3,13 @@ proc;; copy test_1 gold_1 copy test_2 gold_2 -share test_1 test_2;; +copy test_3 gold_3 +share test_1 test_2 test_3;; select -assert-count 1 test_1/t:$mul select -assert-count 1 test_2/t:$mul select -assert-count 1 test_2/t:$div +select -assert-count 1 test_3/t:$div miter -equiv -flatten -make_outputs -make_outcmp gold_1 test_1 miter_1 sat -verify -prove trigger 0 -show-inputs -show-outputs miter_1 @@ -15,3 +17,5 @@ sat -verify -prove trigger 0 -show-inputs -show-outputs miter_1 miter -equiv -flatten -make_outputs -make_outcmp gold_2 test_2 miter_2 sat -verify -prove trigger 0 -show-inputs -show-outputs miter_2 +miter -equiv -flatten -make_outputs -make_outcmp gold_3 test_3 miter_3 +sat -verify -prove trigger 0 -show-inputs -show-outputs miter_3