From 6dff9e778744ad538c55946eb7b5ab97ee99d5fd Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 14 Apr 2025 15:41:30 +0200 Subject: [PATCH 1/4] share: Restrict activation patterns to potentially relevant signals In case the two sets of activation patterns are mutually exclusive without considering the logic feeding into the activation signals, an activation condition can only be relevant if present in both sets with opposite polarity. This detects pattern-only mutual exclusion by running an additional SAT query before importing the input cone logic. If that is already UNSAT, we remove all non-relevant condition and re-simplify the remaining patterns. In cases of pattern-only mutual exclusion, this will often produce much smaller selection logic and avoid the more costly SAT query that includes the input cones. --- passes/opt/share.cc | 95 ++++++++++++++++++++++++++++++++++++--------- 1 file changed, 77 insertions(+), 18 deletions(-) diff --git a/passes/opt/share.cc b/passes/opt/share.cc index 0820bad12..7ffe26b2b 100644 --- a/passes/opt/share.cc +++ b/passes/opt/share.cc @@ -1000,6 +1000,53 @@ 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; + } + + void onesided_restrict_activiation_patterns( + pool &activation_patterns, const pool> &other_bits) + { + pool new_activiation_patterns; + + 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); + } + } + new_activiation_patterns.emplace(std::move(new_pair)); + } + + activation_patterns = std::move(new_activiation_patterns); + } + + // Only valid if the patterns on their own (i.e. without considering their input cone) are mutually exclusive! + void restrict_activiation_patterns(pool &activation_patterns, pool &other_activation_patterns) + { + pool> bits = pattern_bits(activation_patterns); + pool> other_bits = pattern_bits(other_activation_patterns); + + onesided_restrict_activiation_patterns(activation_patterns, other_bits); + onesided_restrict_activiation_patterns(other_activation_patterns, bits); + + optimize_activation_patterns(activation_patterns); + optimize_activation_patterns(other_activation_patterns); + } + 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 +1346,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 +1365,39 @@ struct ShareWorker continue; } - qcsat.ez->non_incremental(); + if (pattern_only_solve) { + qcsat.ez->non_incremental(); - all_ctrl_signals.sort_and_unify(); - std::vector sat_model = qcsat.importSig(all_ctrl_signals); - std::vector sat_model_values; + all_ctrl_signals.sort_and_unify(); + std::vector sat_model = qcsat.importSig(all_ctrl_signals); + std::vector sat_model_values; - qcsat.ez->assume(qcsat.ez->AND(sub1, sub2)); + qcsat.ez->assume(qcsat.ez->AND(sub1, sub2)); - log(" Size of SAT problem: %zu cells, %d variables, %d clauses\n", - qcsat.imported_cells.size(), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses()); + 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; + 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"); + restrict_activiation_patterns(filtered_cell_activation_patterns, filtered_other_cell_activation_patterns); + + for (auto &p : filtered_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 : filtered_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; From 27ed77ea2428433e4efc1ff29d0ebc36753f9458 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 15 Apr 2025 10:25:39 +0200 Subject: [PATCH 2/4] share: Keep filtered activation patterns for the supercell The previous commit introduced code that optimizes the activation patterns to be able to generate smaller activation logic. The resulting supercell was then enqueued as shareable using those optimized activation patterns. The condition represented by the optimized patterns is an over-approximation of the actual activiation condition. This means using it as activiation for the supercell loses precision and pessimises sharing of the supercell with further cells, breaking the sat/share test. This commit fixes that by using the optimized activiation patterns only for the generation of activation logic and using the original patterns for enqueuing the supercell. --- passes/opt/share.cc | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/passes/opt/share.cc b/passes/opt/share.cc index 7ffe26b2b..eb6476d57 100644 --- a/passes/opt/share.cc +++ b/passes/opt/share.cc @@ -1365,6 +1365,9 @@ struct ShareWorker continue; } + pool optimized_cell_activation_patterns = filtered_cell_activation_patterns; + pool optimized_other_cell_activation_patterns = filtered_other_cell_activation_patterns; + if (pattern_only_solve) { qcsat.ez->non_incremental(); @@ -1389,12 +1392,12 @@ struct ShareWorker 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"); - restrict_activiation_patterns(filtered_cell_activation_patterns, filtered_other_cell_activation_patterns); + restrict_activiation_patterns(optimized_cell_activation_patterns, optimized_other_cell_activation_patterns); - for (auto &p : filtered_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 : filtered_other_cell_activation_patterns) + 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)); } @@ -1413,20 +1416,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)); } From 7593b5b224e54c871d5c48484eceac315b82ea9b Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 15 Apr 2025 12:02:09 +0200 Subject: [PATCH 3/4] share: Only print optimized activation patterns when different This removes redundant information from the log and makes it easier to spot where the new optimization had an effect. --- passes/opt/share.cc | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/passes/opt/share.cc b/passes/opt/share.cc index eb6476d57..580549e4d 100644 --- a/passes/opt/share.cc +++ b/passes/opt/share.cc @@ -1013,11 +1013,13 @@ struct ShareWorker return bits; } - void onesided_restrict_activiation_patterns( + bool onesided_restrict_activiation_patterns( pool &activation_patterns, const pool> &other_bits) { pool new_activiation_patterns; + bool simplified = false; + for (auto const &pattern : activation_patterns) { ssc_pair_t new_pair; for (int i = 0; i < GetSize(pattern.second); ++i) { @@ -1026,25 +1028,31 @@ struct ShareWorker 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_activiation_patterns.emplace(std::move(new_pair)); } activation_patterns = std::move(new_activiation_patterns); + return simplified; } // Only valid if the patterns on their own (i.e. without considering their input cone) are mutually exclusive! - void restrict_activiation_patterns(pool &activation_patterns, pool &other_activation_patterns) + bool restrict_activiation_patterns(pool &activation_patterns, pool &other_activation_patterns) { pool> bits = pattern_bits(activation_patterns); pool> other_bits = pattern_bits(other_activation_patterns); - onesided_restrict_activiation_patterns(activation_patterns, other_bits); - onesided_restrict_activiation_patterns(other_activation_patterns, bits); + bool simplified = false; + simplified |= onesided_restrict_activiation_patterns(activation_patterns, other_bits); + simplified |= onesided_restrict_activiation_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) @@ -1392,13 +1400,14 @@ struct ShareWorker 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"); - restrict_activiation_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)); + if (restrict_activiation_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)); + 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)); + } } if (find_in_input_cone(cell, other_cell)) { From 4b273a4ae9e4fc43b9580de82015a56d4095c85b Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 15 Apr 2025 12:04:09 +0200 Subject: [PATCH 4/4] share: Cleanup and additional testing Fixes a typo and adds another test case that triggers the fallback behavior as the existing tests all trigger the new optimization. --- passes/opt/share.cc | 16 ++++++++-------- tests/sat/share.v | 23 +++++++++++++++++++++++ tests/sat/share.ys | 6 +++++- 3 files changed, 36 insertions(+), 9 deletions(-) diff --git a/passes/opt/share.cc b/passes/opt/share.cc index 580549e4d..1d7ba7d98 100644 --- a/passes/opt/share.cc +++ b/passes/opt/share.cc @@ -1013,10 +1013,10 @@ struct ShareWorker return bits; } - bool onesided_restrict_activiation_patterns( + bool onesided_restrict_activation_patterns( pool &activation_patterns, const pool> &other_bits) { - pool new_activiation_patterns; + pool new_activation_patterns; bool simplified = false; @@ -1032,22 +1032,22 @@ struct ShareWorker simplified = true; } } - new_activiation_patterns.emplace(std::move(new_pair)); + new_activation_patterns.emplace(std::move(new_pair)); } - activation_patterns = std::move(new_activiation_patterns); + 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_activiation_patterns(pool &activation_patterns, pool &other_activation_patterns) + 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_activiation_patterns(activation_patterns, other_bits); - simplified |= onesided_restrict_activiation_patterns(other_activation_patterns, bits); + 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); @@ -1401,7 +1401,7 @@ struct ShareWorker } else { log(" According to the SAT solver this pair of cells can be shared. (Pattern only case)\n"); - if (restrict_activiation_patterns(optimized_cell_activation_patterns, optimized_other_cell_activation_patterns)) { + 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)); 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