aboutsummaryrefslogtreecommitdiffstats
path: root/passes/opt
diff options
context:
space:
mode:
Diffstat (limited to 'passes/opt')
-rw-r--r--passes/opt/opt_dff.cc44
-rw-r--r--passes/opt/share.cc75
2 files changed, 30 insertions, 89 deletions
diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc
index 94d6d5443..ddf08392b 100644
--- a/passes/opt/opt_dff.cc
+++ b/passes/opt/opt_dff.cc
@@ -21,7 +21,8 @@
#include "kernel/log.h"
#include "kernel/register.h"
#include "kernel/rtlil.h"
-#include "kernel/satgen.h"
+#include "kernel/qcsat.h"
+#include "kernel/modtools.h"
#include "kernel/sigtools.h"
#include "kernel/ffinit.h"
#include "kernel/ff.h"
@@ -51,26 +52,23 @@ struct OptDffWorker
FfInitVals initvals;
dict<SigBit, int> bitusers;
dict<SigBit, cell_int_t> bit2mux;
- dict<SigBit, RTLIL::Cell*> bit2driver;
typedef std::map<RTLIL::SigBit, bool> pattern_t;
typedef std::set<pattern_t> patterns_t;
typedef std::pair<RTLIL::SigBit, bool> ctrl_t;
typedef std::set<ctrl_t> ctrls_t;
- ezSatPtr ez;
- SatGen satgen;
- pool<Cell*> sat_cells;
+ ModWalker modwalker;
+ QuickConeSat qcsat;
// Used as a queue.
std::vector<Cell *> dff_cells;
- OptDffWorker(const OptDffOptions &opt, Module *mod) : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod), ez(), satgen(ez.get(), &sigmap) {
- // Gathering three kinds of information here for every sigmapped SigBit:
+ OptDffWorker(const OptDffOptions &opt, Module *mod) : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod), modwalker(module->design, module), qcsat(modwalker) {
+ // Gathering two kinds of information here for every sigmapped SigBit:
//
// - bitusers: how many users it has (muxes will only be merged into FFs if this is 1, making the FF the only user)
// - bit2mux: the mux cell and bit index that drives it, if any
- // - bit2driver: the cell driving it, if any
for (auto wire : module->wires())
{
@@ -88,10 +86,6 @@ struct OptDffWorker
for (auto conn : cell->connections()) {
bool is_output = cell->output(conn.first);
- if (is_output) {
- for (auto bit : sigmap(conn.second))
- bit2driver[bit] = cell;
- }
if (!is_output || !cell->known()) {
for (auto bit : sigmap(conn.second))
bitusers[bit]++;
@@ -104,20 +98,6 @@ struct OptDffWorker
}
- std::function<void(Cell*)> sat_import_cell = [&](Cell *c) {
- if (!sat_cells.insert(c).second)
- return;
- if (!satgen.importCell(c))
- return;
- for (auto &conn : c->connections()) {
- if (!c->input(conn.first))
- continue;
- for (auto bit : sigmap(conn.second))
- if (bit2driver.count(bit))
- sat_import_cell(bit2driver.at(bit));
- }
- };
-
State combine_const(State a, State b) {
if (a == State::Sx && !opt.keepdc)
return b;
@@ -594,19 +574,19 @@ struct OptDffWorker
if (!opt.sat)
continue;
// For each register bit, try to prove that it cannot change from the initial value. If so, remove it
- if (!bit2driver.count(ff.sig_d[i]))
+ if (!modwalker.has_drivers(ff.sig_d.extract(i)))
continue;
if (val != State::S0 && val != State::S1)
continue;
- sat_import_cell(bit2driver.at(ff.sig_d[i]));
+ int init_sat_pi = qcsat.importSigBit(val);
+ int q_sat_pi = qcsat.importSigBit(ff.sig_q[i]);
+ int d_sat_pi = qcsat.importSigBit(ff.sig_d[i]);
- int init_sat_pi = satgen.importSigSpec(val).front();
- int q_sat_pi = satgen.importSigBit(ff.sig_q[i]);
- int d_sat_pi = satgen.importSigBit(ff.sig_d[i]);
+ qcsat.prepare();
// Try to find out whether the register bit can change under some circumstances
- bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi)));
+ bool counter_example_found = qcsat.ez->solve(qcsat.ez->IFF(q_sat_pi, init_sat_pi), qcsat.ez->NOT(qcsat.ez->IFF(d_sat_pi, init_sat_pi)));
// If the register bit cannot change, we can replace it with a constant
if (counter_example_found)
diff --git a/passes/opt/share.cc b/passes/opt/share.cc
index 88c4dee8b..ee1acfb7f 100644
--- a/passes/opt/share.cc
+++ b/passes/opt/share.cc
@@ -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);
-
- 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)));
- }
+ qcsat.prepare();
- 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--)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 14:41:18 +0000