mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 19:52:31 +00:00
Merge pull request #5023 from jix/restrict_share_activiation_patterns
share: Restrict activation patterns to potentially relevant signals
This commit is contained in:
Jannis Harder
GitHub
commit
ecf9c9f0cf
3 changed files with 121 additions and 23 deletions
|
|
@ -1000,6 +1000,61 @@ struct ShareWorker
|
|||
}
|
||||
}
|
||||
|
||||
pool<std::pair<SigBit, State>> pattern_bits(const pool<ssc_pair_t> &activation_patterns)
|
||||
{
|
||||
pool<std::pair<SigBit, State>> 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<ssc_pair_t> &activation_patterns, const pool<std::pair<SigBit, State>> &other_bits)
|
||||
{
|
||||
pool<ssc_pair_t> 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<ssc_pair_t> &activation_patterns, pool<ssc_pair_t> &other_activation_patterns)
|
||||
{
|
||||
pool<std::pair<SigBit, State>> bits = pattern_bits(activation_patterns);
|
||||
pool<std::pair<SigBit, State>> 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<ssc_pair_t> &activation_patterns, pool<RTLIL::Cell*> &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<ssc_pair_t> optimized_cell_activation_patterns = filtered_cell_activation_patterns;
|
||||
pool<ssc_pair_t> optimized_other_cell_activation_patterns = filtered_other_cell_activation_patterns;
|
||||
|
||||
all_ctrl_signals.sort_and_unify();
|
||||
std::vector<int> sat_model = qcsat.importSig(all_ctrl_signals);
|
||||
std::vector<bool> 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<int> sat_model = qcsat.importSig(all_ctrl_signals);
|
||||
std::vector<bool> 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<RTLIL::Cell*> 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));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue