mirror of
https://github.com/YosysHQ/yosys
synced 2025-06-06 14:13:23 +00:00
Refactor common parts of SAT-using optimizations into a helper.
This also aligns the functionality: - in all cases, the onehot attribute is used to create appropriate constraints (previously, opt_dff didn't do it at all, and share created one-hot constraints based on $pmux presence alone, which is unsound) - in all cases, shift and mul/div/pow cells are now skipped when importing the SAT problem (previously only memory_share did this) — this avoids creating clauses for hard cells that are unlikely to help with proving the UNSATness needed for optimization
This commit is contained in:
Marcelina Kościelnicka
parent
d8fcf1ab25
commit
d25b9088c8
7 changed files with 224 additions and 153 deletions
|
|
@ -18,7 +18,7 @@
|
|||
*/
|
||||
|
||||
#include "kernel/yosys.h"
|
||||
#include "kernel/satgen.h"
|
||||
#include "kernel/qcsat.h"
|
||||
#include "kernel/sigtools.h"
|
||||
#include "kernel/modtools.h"
|
||||
#include "kernel/utils.h"
|
||||
|
|
@ -58,8 +58,6 @@ struct ShareWorker
|
|||
std::map<RTLIL::Cell*, std::set<RTLIL::Cell*, cell_ptr_cmp>, cell_ptr_cmp> topo_cell_drivers;
|
||||
std::map<RTLIL::SigBit, std::set<RTLIL::Cell*, cell_ptr_cmp>> topo_bit_drivers;
|
||||
|
||||
std::vector<std::pair<RTLIL::SigBit, RTLIL::SigBit>> exclusive_ctrls;
|
||||
|
||||
|
||||
// ------------------------------------------------------------------------------
|
||||
// Find terminal bits -- i.e. bits that do not (exclusively) feed into a mux tree
|
||||
|
|
@ -1156,7 +1154,6 @@ struct ShareWorker
|
|||
recursion_state.clear();
|
||||
topo_cell_drivers.clear();
|
||||
topo_bit_drivers.clear();
|
||||
exclusive_ctrls.clear();
|
||||
terminal_bits.clear();
|
||||
shareable_cells.clear();
|
||||
forbidden_controls_cache.clear();
|
||||
|
|
@ -1171,13 +1168,6 @@ struct ShareWorker
|
|||
log("Found %d cells in module %s that may be considered for resource sharing.\n",
|
||||
GetSize(shareable_cells), log_id(module));
|
||||
|
||||
for (auto cell : module->cells())
|
||||
if (cell->type == ID($pmux))
|
||||
for (auto bit : cell->getPort(ID::S))
|
||||
for (auto other_bit : cell->getPort(ID::S))
|
||||
if (bit < other_bit)
|
||||
exclusive_ctrls.push_back(std::pair<RTLIL::SigBit, RTLIL::SigBit>(bit, other_bit));
|
||||
|
||||
while (!shareable_cells.empty() && config.limit != 0)
|
||||
{
|
||||
RTLIL::Cell *cell = *shareable_cells.begin();
|
||||
|
|
@ -1256,8 +1246,11 @@ struct ShareWorker
|
|||
optimize_activation_patterns(filtered_cell_activation_patterns);
|
||||
optimize_activation_patterns(filtered_other_cell_activation_patterns);
|
||||
|
||||
ezSatPtr ez;
|
||||
SatGen satgen(ez.get(), &modwalker.sigmap);
|
||||
QuickConeSat qcsat(modwalker);
|
||||
if (config.opt_fast) {
|
||||
qcsat.max_cell_outs = 3;
|
||||
qcsat.max_cell_count = 100;
|
||||
}
|
||||
|
||||
pool<RTLIL::Cell*> sat_cells;
|
||||
std::set<RTLIL::SigBit> bits_queue;
|
||||
|
|
@ -1267,77 +1260,45 @@ struct ShareWorker
|
|||
|
||||
for (auto &p : filtered_cell_activation_patterns) {
|
||||
log(" Activation pattern for cell %s: %s = %s\n", log_id(cell), log_signal(p.first), log_signal(p.second));
|
||||
cell_active.push_back(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second)));
|
||||
cell_active.push_back(qcsat.ez->vec_eq(qcsat.importSig(p.first), qcsat.importSig(p.second)));
|
||||
all_ctrl_signals.append(p.first);
|
||||
}
|
||||
|
||||
for (auto &p : filtered_other_cell_activation_patterns) {
|
||||
log(" Activation pattern for cell %s: %s = %s\n", log_id(other_cell), log_signal(p.first), log_signal(p.second));
|
||||
other_cell_active.push_back(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second)));
|
||||
other_cell_active.push_back(qcsat.ez->vec_eq(qcsat.importSig(p.first), qcsat.importSig(p.second)));
|
||||
all_ctrl_signals.append(p.first);
|
||||
}
|
||||
|
||||
for (auto &bit : cell_activation_signals.to_sigbit_vector())
|
||||
bits_queue.insert(bit);
|
||||
qcsat.prepare();
|
||||
|
||||
for (auto &bit : other_cell_activation_signals.to_sigbit_vector())
|
||||
bits_queue.insert(bit);
|
||||
|
||||
while (!bits_queue.empty())
|
||||
{
|
||||
pool<ModWalker::PortBit> portbits;
|
||||
modwalker.get_drivers(portbits, bits_queue);
|
||||
bits_queue.clear();
|
||||
|
||||
for (auto &pbit : portbits)
|
||||
if (sat_cells.count(pbit.cell) == 0 && cone_ct.cell_known(pbit.cell->type)) {
|
||||
if (config.opt_fast && modwalker.cell_outputs[pbit.cell].size() >= 4)
|
||||
continue;
|
||||
// log(" Adding cell %s (%s) to SAT problem.\n", log_id(pbit.cell), log_id(pbit.cell->type));
|
||||
bits_queue.insert(modwalker.cell_inputs[pbit.cell].begin(), modwalker.cell_inputs[pbit.cell].end());
|
||||
satgen.importCell(pbit.cell);
|
||||
sat_cells.insert(pbit.cell);
|
||||
}
|
||||
|
||||
if (config.opt_fast && sat_cells.size() > 100)
|
||||
break;
|
||||
}
|
||||
|
||||
for (auto it : exclusive_ctrls)
|
||||
if (satgen.importedSigBit(it.first) && satgen.importedSigBit(it.second)) {
|
||||
log(" Adding exclusive control bits: %s vs. %s\n", log_signal(it.first), log_signal(it.second));
|
||||
int sub1 = satgen.importSigBit(it.first);
|
||||
int sub2 = satgen.importSigBit(it.second);
|
||||
ez->assume(ez->NOT(ez->AND(sub1, sub2)));
|
||||
}
|
||||
|
||||
if (!ez->solve(ez->expression(ez->OpOr, cell_active))) {
|
||||
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;
|
||||
}
|
||||
|
||||
if (!ez->solve(ez->expression(ez->OpOr, other_cell_active))) {
|
||||
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);
|
||||
shareable_cells.erase(other_cell);
|
||||
continue;
|
||||
}
|
||||
|
||||
ez->non_incremental();
|
||||
qcsat.ez->non_incremental();
|
||||
|
||||
all_ctrl_signals.sort_and_unify();
|
||||
std::vector<int> sat_model = satgen.importSigSpec(all_ctrl_signals);
|
||||
std::vector<int> sat_model = qcsat.importSig(all_ctrl_signals);
|
||||
std::vector<bool> sat_model_values;
|
||||
|
||||
int sub1 = ez->expression(ez->OpOr, cell_active);
|
||||
int sub2 = ez->expression(ez->OpOr, other_cell_active);
|
||||
ez->assume(ez->AND(sub1, sub2));
|
||||
qcsat.ez->assume(qcsat.ez->AND(sub1, sub2));
|
||||
|
||||
log(" Size of SAT problem: %d cells, %d variables, %d clauses\n",
|
||||
GetSize(sat_cells), ez->numCnfVariables(), ez->numCnfClauses());
|
||||
GetSize(sat_cells), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses());
|
||||
|
||||
if (ez->solve(sat_model, sat_model_values)) {
|
||||
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--)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue