aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/opt/opt.cc8
-rw-r--r--passes/opt/opt_rmdff.cc109
-rw-r--r--passes/techmap/abc9.cc30
3 files changed, 123 insertions, 24 deletions
diff --git a/passes/opt/opt.cc b/passes/opt/opt.cc
index a4aca2fee..e9a43e0f3 100644
--- a/passes/opt/opt.cc
+++ b/passes/opt/opt.cc
@@ -44,7 +44,7 @@ struct OptPass : public Pass {
log(" opt_muxtree\n");
log(" opt_reduce [-fine] [-full]\n");
log(" opt_merge [-share_all]\n");
- log(" opt_rmdff [-keepdc]\n");
+ log(" opt_rmdff [-keepdc] [-sat]\n");
log(" opt_clean [-purge]\n");
log(" opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
log(" while <changed design>\n");
@@ -54,7 +54,7 @@ struct OptPass : public Pass {
log(" do\n");
log(" opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
log(" opt_merge [-share_all]\n");
- log(" opt_rmdff [-keepdc]\n");
+ log(" opt_rmdff [-keepdc] [-sat]\n");
log(" opt_clean [-purge]\n");
log(" while <changed design in opt_rmdff>\n");
log("\n");
@@ -112,6 +112,10 @@ struct OptPass : public Pass {
opt_rmdff_args += " -keepdc";
continue;
}
+ if (args[argidx] == "-sat") {
+ opt_rmdff_args += " -sat";
+ continue;
+ }
if (args[argidx] == "-share_all") {
opt_merge_args += " -share_all";
continue;
diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index eeb992a3e..be6ac2d30 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -17,19 +17,24 @@
*
*/
+#include "kernel/log.h"
#include "kernel/register.h"
+#include "kernel/rtlil.h"
+#include "kernel/satgen.h"
#include "kernel/sigtools.h"
-#include "kernel/log.h"
-#include <stdlib.h>
#include <stdio.h>
+#include <stdlib.h>
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
SigMap assign_map, dff_init_map;
SigSet<RTLIL::Cell*> mux_drivers;
+dict<SigBit, RTLIL::Cell*> bit2driver;
dict<SigBit, pool<SigBit>> init_attributes;
+
bool keepdc;
+bool sat;
void remove_init_attr(SigSpec sig)
{
@@ -452,12 +457,84 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
dff->unsetPort("\\E");
}
+ if (sat && has_init && (!sig_r.size() || val_init == val_rv))
+ {
+ bool removed_sigbits = false;
+
+ ezSatPtr ez;
+ SatGen satgen(ez.get(), &assign_map);
+ pool<Cell*> sat_cells;
+
+ 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 : assign_map(conn.second))
+ if (bit2driver.count(bit))
+ sat_import_cell(bit2driver.at(bit));
+ }
+ };
+
+ // For each register bit, try to prove that it cannot change from the initial value. If so, remove it
+ for (int position = 0; position < GetSize(sig_d); position += 1) {
+ RTLIL::SigBit q_sigbit = sig_q[position];
+ RTLIL::SigBit d_sigbit = sig_d[position];
+
+ if ((!q_sigbit.wire) || (!d_sigbit.wire))
+ continue;
+
+ if (!bit2driver.count(d_sigbit))
+ continue;
+
+ sat_import_cell(bit2driver.at(d_sigbit));
+
+ RTLIL::State sigbit_init_val = val_init[position];
+ if (sigbit_init_val != State::S0 && sigbit_init_val != State::S1)
+ continue;
+
+ int init_sat_pi = satgen.importSigSpec(sigbit_init_val).front();
+ int q_sat_pi = satgen.importSigBit(q_sigbit);
+ int d_sat_pi = satgen.importSigBit(d_sigbit);
+
+ // 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)));
+
+ // If the register bit cannot change, we can replace it with a constant
+ if (!counter_example_found)
+ {
+ log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n", sigbit_init_val ? 1 : 0,
+ position, log_id(dff), log_id(dff->type), log_id(mod));
+
+ SigSpec tmp = dff->getPort("\\D");
+ tmp[position] = sigbit_init_val;
+ dff->setPort("\\D", tmp);
+
+ removed_sigbits = true;
+ }
+ }
+
+ if (removed_sigbits) {
+ handle_dff(mod, dff);
+ return true;
+ }
+ }
+
+
return false;
delete_dff:
log("Removing %s (%s) from module %s.\n", log_id(dff), log_id(dff->type), log_id(mod));
remove_init_attr(dff->getPort("\\Q"));
mod->remove(dff);
+
+ for (auto &entry : bit2driver)
+ if (entry.second == dff)
+ bit2driver.erase(entry.first);
+
return true;
}
@@ -467,11 +544,15 @@ struct OptRmdffPass : public Pass {
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
- log(" opt_rmdff [-keepdc] [selection]\n");
+ log(" opt_rmdff [-keepdc] [-sat] [selection]\n");
log("\n");
log("This pass identifies flip-flops with constant inputs and replaces them with\n");
log("a constant driver.\n");
log("\n");
+ log(" -sat\n");
+ log(" additionally invoke SAT solver to detect and remove flip-flops (with \n");
+ log(" non-constant inputs) that can also be replaced with a constant driver\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
@@ -479,6 +560,7 @@ struct OptRmdffPass : public Pass {
log_header(design, "Executing OPT_RMDFF pass (remove dff with constant values).\n");
keepdc = false;
+ sat = false;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
@@ -486,18 +568,22 @@ struct OptRmdffPass : public Pass {
keepdc = true;
continue;
}
+ if (args[argidx] == "-sat") {
+ sat = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
- for (auto module : design->selected_modules())
- {
+ for (auto module : design->selected_modules()) {
pool<SigBit> driven_bits;
dict<SigBit, State> init_bits;
assign_map.set(module);
dff_init_map.set(module);
mux_drivers.clear();
+ bit2driver.clear();
init_attributes.clear();
for (auto wire : module->wires())
@@ -522,17 +608,21 @@ struct OptRmdffPass : public Pass {
driven_bits.insert(bit);
}
}
- mux_drivers.clear();
std::vector<RTLIL::IdString> dff_list;
std::vector<RTLIL::IdString> dffsr_list;
std::vector<RTLIL::IdString> dlatch_list;
for (auto cell : module->cells())
{
- for (auto &conn : cell->connections())
- if (cell->output(conn.first) || !cell->known())
- for (auto bit : assign_map(conn.second))
+ for (auto &conn : cell->connections()) {
+ bool is_output = cell->output(conn.first);
+ if (is_output || !cell->known())
+ for (auto bit : assign_map(conn.second)) {
+ if (is_output)
+ bit2driver[bit] = cell;
driven_bits.insert(bit);
+ }
+ }
if (cell->type == "$mux" || cell->type == "$pmux") {
if (cell->getPort("\\A").size() == cell->getPort("\\B").size())
@@ -604,6 +694,7 @@ struct OptRmdffPass : public Pass {
assign_map.clear();
mux_drivers.clear();
+ bit2driver.clear();
init_attributes.clear();
if (total_count || total_initdrv)
diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc
index dbdd775f8..f107f9947 100644
--- a/passes/techmap/abc9.cc
+++ b/passes/techmap/abc9.cc
@@ -33,7 +33,7 @@
#endif
-#define ABC_FAST_COMMAND_LUT "&st; &retime; &if {W}"
+#define ABC_FAST_COMMAND_LUT "&st; &if {W} {D}"
#include "kernel/register.h"
#include "kernel/sigtools.h"
@@ -80,7 +80,7 @@ void handle_loops(RTLIL::Design *design)
{
Pass::call(design, "scc -set_attr abc_scc_id {}");
- dict<IdString, vector<IdString>> module_break;
+ dict<IdString, vector<IdString>> abc_scc_break;
// For every unique SCC found, (arbitrarily) find the first
// cell in the component, and select (and mark) all its output
@@ -116,12 +116,11 @@ void handle_loops(RTLIL::Design *design)
cell->attributes.erase(it);
}
- auto jt = module_break.find(cell->type);
- if (jt == module_break.end()) {
+ auto jt = abc_scc_break.find(cell->type);
+ if (jt == abc_scc_break.end()) {
std::vector<IdString> ports;
- if (!yosys_celltypes.cell_known(cell->type)) {
- RTLIL::Module* box_module = design->module(cell->type);
- log_assert(box_module);
+ RTLIL::Module* box_module = design->module(cell->type);
+ if (box_module) {
auto ports_csv = box_module->attributes.at("\\abc_scc_break", RTLIL::Const::from_string("")).decode_string();
for (const auto &port_name : split_tokens(ports_csv, ",")) {
auto port_id = RTLIL::escape_id(port_name);
@@ -131,7 +130,7 @@ void handle_loops(RTLIL::Design *design)
ports.push_back(port_id);
}
}
- jt = module_break.insert(std::make_pair(cell->type, std::move(ports))).first;
+ jt = abc_scc_break.insert(std::make_pair(cell->type, std::move(ports))).first;
}
for (auto port_name : jt->second) {
@@ -554,15 +553,20 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
signal = std::move(bits);
}
+ dict<IdString, bool> abc_box;
vector<RTLIL::Cell*> boxes;
- for (auto it = module->cells_.begin(); it != module->cells_.end(); ++it) {
- RTLIL::Cell *cell = it->second;
- if (cell->type.in("$_AND_", "$_NOT_", "$__ABC_FF_")) {
+ for (const auto &it : module->cells_) {
+ auto cell = it.second;
+ if (cell->type.in("$_AND_", "$_NOT_")) {
module->remove(cell);
continue;
}
- RTLIL::Module* box_module = design->module(cell->type);
- if (box_module && box_module->attributes.count("\\abc_box_id"))
+ auto jt = abc_box.find(cell->type);
+ if (jt == abc_box.end()) {
+ RTLIL::Module* box_module = design->module(cell->type);
+ jt = abc_box.insert(std::make_pair(cell->type, box_module && box_module->attributes.count("\\abc_box_id"))).first;
+ }
+ if (jt->second)
boxes.emplace_back(cell);
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 17:49:32 +0000