From 9a468f81c412f8b63d25e739f28932815c6882fb Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Tue, 28 May 2019 08:48:21 +0200 Subject: Optimizing DFFs whose initial value prevents their value from changing This is a proof of concept implementation that invokes SAT solver via Pass::call method. --- passes/opt/opt_rmdff.cc | 58 ++++++++++++++++++++++++++++++++++++++++++++++--- passes/sat/sat.cc | 4 ++++ 2 files changed, 59 insertions(+), 3 deletions(-) (limited to 'passes') diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index 2abffa2a9..72eac9111 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -30,6 +30,7 @@ SigMap assign_map, dff_init_map; SigSet mux_drivers; dict> init_attributes; bool keepdc; +bool sat; void remove_init_attr(SigSpec sig) { @@ -258,7 +259,7 @@ delete_dlatch: return true; } -bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) +bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass) { RTLIL::SigSpec sig_d, sig_q, sig_c, sig_r, sig_e; RTLIL::Const val_cp, val_rp, val_rv, val_ep; @@ -452,6 +453,52 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) dff->unsetPort("\\E"); } + if (sat && has_init) { + std::vector removed_sigbits; + + // for (auto &sigbit : sig_q.bits()) { + for (int position =0; position < GetSize(sig_d); position += 1) { + RTLIL::SigBit q_sigbit = sig_q[position]; + RTLIL::SigBit d_sigbit = sig_d[position]; + RTLIL::Const sigbit_init_val = val_init.extract(position); + + if ((!q_sigbit.wire) || (!d_sigbit.wire)) { + continue; + } + + char str[1024]; + sprintf(str, "sat -ignore_unknown_cells -prove %s[%d] %s -set %s[%d] %s", + log_id(d_sigbit.wire), + d_sigbit.offset, + sigbit_init_val.as_string().c_str(), + log_id(q_sigbit.wire), + q_sigbit.offset, + sigbit_init_val.as_string().c_str() + ); + log("Running: %s\n", str); + + log_flush(); + + pass->call(mod->design, str); + if (mod->design->scratchpad_get_bool("sat.success", false)) { + sprintf(str, "connect -set %s[%d] %s", + log_id(q_sigbit.wire), + q_sigbit.offset, + sigbit_init_val.as_string().c_str() + ); + log("Running: %s\n", str); + log_flush(); + pass->call(mod->design, str); + // mod->connect(q_sigbit, sigbit_init_val); + removed_sigbits.push_back(position); + } + } + + if (!removed_sigbits.empty()) { + return true; + } + } + return false; delete_dff: @@ -467,7 +514,7 @@ 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"); @@ -479,6 +526,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,6 +534,10 @@ struct OptRmdffPass : public Pass { keepdc = true; continue; } + if (args[argidx] == "-sat") { + sat = true; + continue; + } break; } extra_args(args, argidx, design); @@ -568,7 +620,7 @@ struct OptRmdffPass : public Pass { for (auto &id : dff_list) { if (module->cell(id) != nullptr && - handle_dff(module, module->cells_[id])) + handle_dff(module, module->cells_[id], this)) total_count++; } diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index cbba738f0..453ae8cca 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -1548,6 +1548,7 @@ struct SatPass : public Pass { print_proof_failed(); tip_failed: + design->scratchpad_set_bool("sat.success", false); if (verify) { log("\n"); log_error("Called with -verify and proof did fail!\n"); @@ -1555,6 +1556,7 @@ struct SatPass : public Pass { if (0) tip_success: + design->scratchpad_set_bool("sat.success", true); if (falsify) { log("\n"); log_error("Called with -falsify and proof did succeed!\n"); @@ -1628,6 +1630,7 @@ struct SatPass : public Pass { if (sathelper.solve()) { + design->scratchpad_set_bool("sat.success", false); if (max_undef) { log("SAT model found. maximizing number of undefs.\n"); sathelper.maximize_undefs(); @@ -1667,6 +1670,7 @@ struct SatPass : public Pass { } else { + design->scratchpad_set_bool("sat.success", true); if (sathelper.gotTimeout) goto timeout; if (rerun_counter) -- cgit v1.2.3 From 29a78267d7c84699bdcebfa87719b31d9b65909b Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Tue, 28 May 2019 15:45:04 +0200 Subject: Fix the regression --- passes/sat/sat.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'passes') diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 453ae8cca..4492fc2b7 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -1554,13 +1554,14 @@ struct SatPass : public Pass { log_error("Called with -verify and proof did fail!\n"); } - if (0) + if (0) { tip_success: design->scratchpad_set_bool("sat.success", true); if (falsify) { log("\n"); log_error("Called with -falsify and proof did succeed!\n"); } + } } else { -- cgit v1.2.3 From 9892df17efadd0eafe5217e812fb4cec2bfdf6e5 Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Tue, 11 Jun 2019 11:47:13 +0200 Subject: Generate satgen instance instead of calling sat pass --- passes/opt/opt_rmdff.cc | 108 +++++++++++++++++++++++++++++++++++++----------- 1 file changed, 85 insertions(+), 23 deletions(-) (limited to 'passes') diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index 72eac9111..4b9fe5823 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -17,11 +17,14 @@ * */ +#include "kernel/log.h" #include "kernel/register.h" +#include "kernel/rtlil.h" +#include "kernel/satgen.h" +#include "kernel/satgen_algo.h" #include "kernel/sigtools.h" -#include "kernel/log.h" -#include #include +#include USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -456,36 +459,95 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass) if (sat && has_init) { std::vector removed_sigbits; + DriverMap drvmap(mod); + // for (auto &sigbit : sig_q.bits()) { - for (int position =0; position < GetSize(sig_d); position += 1) { + for (int position = 0; position < GetSize(sig_d); position += 1) { RTLIL::SigBit q_sigbit = sig_q[position]; RTLIL::SigBit d_sigbit = sig_d[position]; - RTLIL::Const sigbit_init_val = val_init.extract(position); if ((!q_sigbit.wire) || (!d_sigbit.wire)) { continue; } + std::map sat_pi; + + ezSatPtr ez; + SatGen satgen(ez.get(), &drvmap.sigmap); + std::set ez_cells; + std::vector modelExpressions; + std::vector modelValues; + + log("Optimizing: %s\n", log_id(q_sigbit.wire)); + log(" Cells:"); + for (const auto &cell : drvmap.cell_cone(d_sigbit)) { + if (ez_cells.count(cell) == 0) { + log(" %s\n", log_id(cell)); + if (!satgen.importCell(cell)) + log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name), + RTLIL::id2cstr(cell->type)); + ez_cells.insert(cell); + } + } + + RTLIL::Const sigbit_init_val = val_init.extract(position); + int reg_init = satgen.importSigSpec(sigbit_init_val).front(); + + int output_a = satgen.importSigSpec(d_sigbit).front(); + modelExpressions.push_back(output_a); + + log(" Wires:"); + for (const auto &sig : drvmap.cone_inputs(d_sigbit)) { + if (sat_pi.count(sig) == 0) { + sat_pi[sig] = satgen.importSigSpec(sig).front(); + modelExpressions.push_back(sat_pi[sig]); + + if (sig == q_sigbit) { + ez->assume(ez->IFF(sat_pi[sig], reg_init)); + } + + if (sig.wire) { + log(" %s\n", log_id(sig.wire)); + } + } + } + + bool success = ez->solve(modelExpressions, modelValues, ez->IFF(output_a, reg_init)); + // bool success = ez->solve(modelExpressions, modelValues, ez->IFF(output_a, ez->NOT(reg_init))); + if (ez->getSolverTimoutStatus()) + log("Timeout\n"); + + log("Success: %d\n", success); + + // satgen.signals_eq(big_lhs, big_rhs, timestep); + + // auto iterable = drvmap.cone(d_sigbit); + + // // for (const auto &sig : drvmap.cone(d_sigbit)) + // for(auto begin=iterable.begin(); begin != iterable.end(); ++begin) + // { + // if (drvmap.count(*begin)) { + // if (drvmap.at(*begin).first) + // log("Running: %s\n", log_id(drvmap.at(*begin).first)); + // } + + // if ((*begin).wire) { + // log("Running: %s\n", log_id((*begin).wire)); + // } + // } + + char str[1024]; - sprintf(str, "sat -ignore_unknown_cells -prove %s[%d] %s -set %s[%d] %s", - log_id(d_sigbit.wire), - d_sigbit.offset, - sigbit_init_val.as_string().c_str(), - log_id(q_sigbit.wire), - q_sigbit.offset, - sigbit_init_val.as_string().c_str() - ); - log("Running: %s\n", str); - - log_flush(); - - pass->call(mod->design, str); - if (mod->design->scratchpad_get_bool("sat.success", false)) { - sprintf(str, "connect -set %s[%d] %s", - log_id(q_sigbit.wire), - q_sigbit.offset, - sigbit_init_val.as_string().c_str() - ); + // sprintf(str, "sat -ignore_unknown_cells -prove %s[%d] %s -set %s[%d] %s", log_id(d_sigbit.wire), d_sigbit.offset, + // sigbit_init_val.as_string().c_str(), log_id(q_sigbit.wire), q_sigbit.offset, sigbit_init_val.as_string().c_str()); + // log("Running: %s\n", str); + + // log_flush(); + + // pass->call(mod->design, str); + // if (mod->design->scratchpad_get_bool("sat.success", false)) { + if (success) { + sprintf(str, "connect -set %s[%d] %s", log_id(q_sigbit.wire), q_sigbit.offset, sigbit_init_val.as_string().c_str()); log("Running: %s\n", str); log_flush(); pass->call(mod->design, str); -- cgit v1.2.3 From d69989b8d27eea16d793600b1779661f31161c6c Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Wed, 12 Jun 2019 19:35:05 +0200 Subject: Rename satgen_algo.h -> algo.h, code cleanup and refactoring --- passes/opt/opt_rmdff.cc | 95 ++++++++++++------------------------------------- 1 file changed, 22 insertions(+), 73 deletions(-) (limited to 'passes') diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index 4b9fe5823..b5a5735e7 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -21,7 +21,7 @@ #include "kernel/register.h" #include "kernel/rtlil.h" #include "kernel/satgen.h" -#include "kernel/satgen_algo.h" +#include "kernel/algo.h" #include "kernel/sigtools.h" #include #include @@ -32,6 +32,7 @@ PRIVATE_NAMESPACE_BEGIN SigMap assign_map, dff_init_map; SigSet mux_drivers; dict> init_attributes; +std::map netlists; bool keepdc; bool sat; @@ -459,9 +460,12 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass) if (sat && has_init) { std::vector removed_sigbits; - DriverMap drvmap(mod); + if (!netlists.count(mod)) { + netlists.emplace(mod, Netlist(mod, comb_cells_filt())); + } + + Netlist &net = netlists.at(mod); - // for (auto &sigbit : sig_q.bits()) { for (int position = 0; position < GetSize(sig_d); position += 1) { RTLIL::SigBit q_sigbit = sig_q[position]; RTLIL::SigBit d_sigbit = sig_d[position]; @@ -470,83 +474,27 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass) continue; } - std::map sat_pi; - ezSatPtr ez; - SatGen satgen(ez.get(), &drvmap.sigmap); - std::set ez_cells; - std::vector modelExpressions; - std::vector modelValues; - - log("Optimizing: %s\n", log_id(q_sigbit.wire)); - log(" Cells:"); - for (const auto &cell : drvmap.cell_cone(d_sigbit)) { - if (ez_cells.count(cell) == 0) { - log(" %s\n", log_id(cell)); - if (!satgen.importCell(cell)) - log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name), - RTLIL::id2cstr(cell->type)); - ez_cells.insert(cell); - } - } - - RTLIL::Const sigbit_init_val = val_init.extract(position); - int reg_init = satgen.importSigSpec(sigbit_init_val).front(); - - int output_a = satgen.importSigSpec(d_sigbit).front(); - modelExpressions.push_back(output_a); - - log(" Wires:"); - for (const auto &sig : drvmap.cone_inputs(d_sigbit)) { - if (sat_pi.count(sig) == 0) { - sat_pi[sig] = satgen.importSigSpec(sig).front(); - modelExpressions.push_back(sat_pi[sig]); - - if (sig == q_sigbit) { - ez->assume(ez->IFF(sat_pi[sig], reg_init)); - } + SatGen satgen(ez.get(), &net.sigmap); - if (sig.wire) { - log(" %s\n", log_id(sig.wire)); - } - } + for (const auto &cell : cell_cone(net, d_sigbit)) { + if (!satgen.importCell(cell)) + log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name), + RTLIL::id2cstr(cell->type)); } - bool success = ez->solve(modelExpressions, modelValues, ez->IFF(output_a, reg_init)); - // bool success = ez->solve(modelExpressions, modelValues, ez->IFF(output_a, ez->NOT(reg_init))); - if (ez->getSolverTimoutStatus()) - log("Timeout\n"); - - log("Success: %d\n", success); - - // satgen.signals_eq(big_lhs, big_rhs, timestep); - - // auto iterable = drvmap.cone(d_sigbit); + RTLIL::Const sigbit_init_val = val_init.extract(position); + int init_sat_pi = satgen.importSigSpec(sigbit_init_val).front(); - // // for (const auto &sig : drvmap.cone(d_sigbit)) - // for(auto begin=iterable.begin(); begin != iterable.end(); ++begin) - // { - // if (drvmap.count(*begin)) { - // if (drvmap.at(*begin).first) - // log("Running: %s\n", log_id(drvmap.at(*begin).first)); - // } + int q_sat_pi = satgen.importSigBit(q_sigbit); + int d_sat_pi = satgen.importSigBit(d_sigbit); - // if ((*begin).wire) { - // log("Running: %s\n", log_id((*begin).wire)); - // } - // } + // log("DFF: %s", log_id(net.sigbit_driver_map[q_sigbit])); + bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi))); char str[1024]; - // sprintf(str, "sat -ignore_unknown_cells -prove %s[%d] %s -set %s[%d] %s", log_id(d_sigbit.wire), d_sigbit.offset, - // sigbit_init_val.as_string().c_str(), log_id(q_sigbit.wire), q_sigbit.offset, sigbit_init_val.as_string().c_str()); - // log("Running: %s\n", str); - - // log_flush(); - - // pass->call(mod->design, str); - // if (mod->design->scratchpad_get_bool("sat.success", false)) { - if (success) { + if (!counter_example_found) { sprintf(str, "connect -set %s[%d] %s", log_id(q_sigbit.wire), q_sigbit.offset, sigbit_init_val.as_string().c_str()); log("Running: %s\n", str); log_flush(); @@ -561,6 +509,7 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass) } } + return false; delete_dff: @@ -603,9 +552,9 @@ struct OptRmdffPass : public Pass { break; } extra_args(args, argidx, design); + netlists.clear(); - for (auto module : design->selected_modules()) - { + for (auto module : design->selected_modules()) { pool driven_bits; dict init_bits; -- cgit v1.2.3 From 8665f48879526f8f3ed79629f28a8686ed78a8ad Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Thu, 13 Jun 2019 19:35:37 +0200 Subject: Implement disconnection of constant register bits --- passes/opt/opt_rmdff.cc | 36 ++++++++++++++++++++++++------------ 1 file changed, 24 insertions(+), 12 deletions(-) (limited to 'passes') diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index b5a5735e7..c5db344e8 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -33,6 +33,8 @@ SigMap assign_map, dff_init_map; SigSet mux_drivers; dict> init_attributes; std::map netlists; +std::map comb_filters; + bool keepdc; bool sat; @@ -263,7 +265,7 @@ delete_dlatch: return true; } -bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass) +bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) { RTLIL::SigSpec sig_d, sig_q, sig_c, sig_r, sig_e; RTLIL::Const val_cp, val_rp, val_rv, val_ep; @@ -461,7 +463,8 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass) std::vector removed_sigbits; if (!netlists.count(mod)) { - netlists.emplace(mod, Netlist(mod, comb_cells_filt())); + netlists.emplace(mod, Netlist(mod)); + comb_filters.emplace(mod, comb_cells_filt()); } Netlist &net = netlists.at(mod); @@ -477,7 +480,7 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass) ezSatPtr ez; SatGen satgen(ez.get(), &net.sigmap); - for (const auto &cell : cell_cone(net, d_sigbit)) { + for (const auto &cell : cell_cone(net, d_sigbit, &comb_filters.at(mod))) { if (!satgen.importCell(cell)) log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type)); @@ -489,17 +492,25 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass) int q_sat_pi = satgen.importSigBit(q_sigbit); int d_sat_pi = satgen.importSigBit(d_sigbit); - // log("DFF: %s", log_id(net.sigbit_driver_map[q_sigbit])); - bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi))); - char str[1024]; + if (position == 14) { + counter_example_found = false; + } + if (!counter_example_found) { - sprintf(str, "connect -set %s[%d] %s", log_id(q_sigbit.wire), q_sigbit.offset, sigbit_init_val.as_string().c_str()); - log("Running: %s\n", str); - log_flush(); - pass->call(mod->design, str); - // mod->connect(q_sigbit, sigbit_init_val); + + RTLIL::SigBit &driver_port = net.driver_port(q_sigbit); + RTLIL::Wire *dummy_wire = mod->addWire(NEW_ID, 1); + + for (auto &conn : mod->connections_) + net.sigmap(conn.first).replace(driver_port, dummy_wire, &conn.first); + + remove_init_attr(driver_port); + driver_port = dummy_wire; + + mod->connect(RTLIL::SigSig(q_sigbit, sigbit_init_val)); + removed_sigbits.push_back(position); } } @@ -553,6 +564,7 @@ struct OptRmdffPass : public Pass { } extra_args(args, argidx, design); netlists.clear(); + comb_filters.clear(); for (auto module : design->selected_modules()) { pool driven_bits; @@ -631,7 +643,7 @@ struct OptRmdffPass : public Pass { for (auto &id : dff_list) { if (module->cell(id) != nullptr && - handle_dff(module, module->cells_[id], this)) + handle_dff(module, module->cells_[id])) total_count++; } -- cgit v1.2.3 From 291b36afeb1075b7c6329d1e57594ed3e6b71581 Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Fri, 14 Jun 2019 11:35:45 +0200 Subject: Some cleanup, revert sat.cc --- passes/opt/opt_rmdff.cc | 17 ++++++++++------- passes/sat/sat.cc | 7 +------ 2 files changed, 11 insertions(+), 13 deletions(-) (limited to 'passes') diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index c5db344e8..41bbdcd57 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -460,15 +460,19 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) } if (sat && has_init) { - std::vector removed_sigbits; + bool removed_sigbits = false; + // Create netlist for the module if not already available if (!netlists.count(mod)) { netlists.emplace(mod, Netlist(mod)); comb_filters.emplace(mod, comb_cells_filt()); } + // Load netlist for the module from the pool Netlist &net = netlists.at(mod); + + // 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]; @@ -480,6 +484,7 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) ezSatPtr ez; SatGen satgen(ez.get(), &net.sigmap); + // Create SAT instance only for the cells that influence the register bit combinatorially for (const auto &cell : cell_cone(net, d_sigbit, &comb_filters.at(mod))) { if (!satgen.importCell(cell)) log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name), @@ -492,12 +497,10 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) 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 (position == 14) { - counter_example_found = false; - } - + // If the register bit cannot change, we can replace it with a constant if (!counter_example_found) { RTLIL::SigBit &driver_port = net.driver_port(q_sigbit); @@ -511,11 +514,11 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) mod->connect(RTLIL::SigSig(q_sigbit, sigbit_init_val)); - removed_sigbits.push_back(position); + removed_sigbits = true; } } - if (!removed_sigbits.empty()) { + if (removed_sigbits) { return true; } } diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 4492fc2b7..cbba738f0 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -1548,20 +1548,17 @@ struct SatPass : public Pass { print_proof_failed(); tip_failed: - design->scratchpad_set_bool("sat.success", false); if (verify) { log("\n"); log_error("Called with -verify and proof did fail!\n"); } - if (0) { + if (0) tip_success: - design->scratchpad_set_bool("sat.success", true); if (falsify) { log("\n"); log_error("Called with -falsify and proof did succeed!\n"); } - } } else { @@ -1631,7 +1628,6 @@ struct SatPass : public Pass { if (sathelper.solve()) { - design->scratchpad_set_bool("sat.success", false); if (max_undef) { log("SAT model found. maximizing number of undefs.\n"); sathelper.maximize_undefs(); @@ -1671,7 +1667,6 @@ struct SatPass : public Pass { } else { - design->scratchpad_set_bool("sat.success", true); if (sathelper.gotTimeout) goto timeout; if (rerun_counter) -- cgit v1.2.3 From 53695e6729e8ae603be7e7cd9bc8b29758d61a11 Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Fri, 14 Jun 2019 11:39:24 +0200 Subject: Prepare for situation when port of the signal cannot be found --- passes/opt/opt_rmdff.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'passes') diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index 41bbdcd57..cf89ac096 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -503,7 +503,7 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) // If the register bit cannot change, we can replace it with a constant if (!counter_example_found) { - RTLIL::SigBit &driver_port = net.driver_port(q_sigbit); + RTLIL::SigSpec driver_port = net.driver_port(q_sigbit); RTLIL::Wire *dummy_wire = mod->addWire(NEW_ID, 1); for (auto &conn : mod->connections_) -- cgit v1.2.3 From 8451cbea896d2b441b5c78eb2813790616d10b84 Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Fri, 14 Jun 2019 12:14:02 +0200 Subject: Move netlist helper module to passes/opt for the time being --- passes/opt/netlist.h | 317 ++++++++++++++++++++++++++++++++++++++++++++++++ passes/opt/opt_rmdff.cc | 2 +- 2 files changed, 318 insertions(+), 1 deletion(-) create mode 100644 passes/opt/netlist.h (limited to 'passes') diff --git a/passes/opt/netlist.h b/passes/opt/netlist.h new file mode 100644 index 000000000..f029ad6ab --- /dev/null +++ b/passes/opt/netlist.h @@ -0,0 +1,317 @@ +/* -*- c++ -*- + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#ifndef SATGEN_ALGO_H +#define SATGEN_ALGO_H + +#include "kernel/celltypes.h" +#include "kernel/rtlil.h" +#include "kernel/sigtools.h" +#include + +YOSYS_NAMESPACE_BEGIN + +CellTypes comb_cells_filt() +{ + CellTypes ct; + + ct.setup_internals(); + ct.setup_stdcells(); + + return ct; +} + +struct Netlist { + RTLIL::Module *module; + SigMap sigmap; + CellTypes ct; + dict sigbit_driver_map; + dict> cell_inputs_map; + + Netlist(RTLIL::Module *module) : module(module), sigmap(module), ct(module->design) { setup_netlist(module, ct); } + + Netlist(RTLIL::Module *module, const CellTypes &ct) : module(module), sigmap(module), ct(ct) { setup_netlist(module, ct); } + + RTLIL::Cell *driver_cell(RTLIL::SigBit sig) const + { + sig = sigmap(sig); + if (!sigbit_driver_map.count(sig)) { + return NULL; + } + + return sigbit_driver_map.at(sig); + } + + RTLIL::SigSpec driver_port(RTLIL::SigBit sig) + { + RTLIL::Cell *cell = driver_cell(sig); + + if (!cell) { + return RTLIL::SigSpec(); + } + + for (auto &port : cell->connections_) { + if (ct.cell_output(cell->type, port.first)) { + RTLIL::SigSpec port_sig = sigmap(port.second); + for (int i = 0; i < GetSize(port_sig); i++) { + if (port_sig[i] == sig) { + return port.second[i]; + } + } + } + } + + return RTLIL::SigSpec(); + } + + void setup_netlist(RTLIL::Module *module, const CellTypes &ct) + { + for (auto cell : module->cells()) { + if (ct.cell_known(cell->type)) { + std::set inputs, outputs; + for (auto &port : cell->connections()) { + std::vector bits = sigmap(port.second).to_sigbit_vector(); + if (ct.cell_output(cell->type, port.first)) + outputs.insert(bits.begin(), bits.end()); + else + inputs.insert(bits.begin(), bits.end()); + } + cell_inputs_map[cell] = inputs; + for (auto &bit : outputs) { + sigbit_driver_map[bit] = cell; + }; + } + } + } +}; + +namespace detail +{ +struct NetlistConeWireIter : public std::iterator { + using set_iter_t = std::set::iterator; + + const Netlist &net; + RTLIL::SigBit sig; + bool sentinel; + CellTypes *cell_filter; + + std::stack> dfs_path_stack; + std::set cells_visited; + + NetlistConeWireIter(const Netlist &net) : net(net), sentinel(true), cell_filter(NULL) {} + + NetlistConeWireIter(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) + : net(net), sig(sig), sentinel(false), cell_filter(cell_filter) + { + } + + const RTLIL::SigBit &operator*() const { return sig; }; + bool operator!=(const NetlistConeWireIter &other) const + { + if (sentinel || other.sentinel) { + return sentinel != other.sentinel; + } else { + return sig != other.sig; + } + } + + bool operator==(const NetlistConeWireIter &other) const + { + if (sentinel || other.sentinel) { + return sentinel == other.sentinel; + } else { + return sig == other.sig; + } + } + + void next_sig_in_dag() + { + while (1) { + if (dfs_path_stack.empty()) { + sentinel = true; + return; + } + + auto &cell_inputs_iter = dfs_path_stack.top().first; + auto &cell_inputs_iter_guard = dfs_path_stack.top().second; + + cell_inputs_iter++; + if (cell_inputs_iter != cell_inputs_iter_guard) { + sig = *cell_inputs_iter; + return; + } else { + dfs_path_stack.pop(); + } + } + } + + NetlistConeWireIter &operator++() + { + RTLIL::Cell *cell = net.driver_cell(sig); + + if (!cell) { + next_sig_in_dag(); + return *this; + } + + if (cells_visited.count(cell)) { + next_sig_in_dag(); + return *this; + } + + if ((cell_filter) && (!cell_filter->cell_known(cell->type))) { + next_sig_in_dag(); + return *this; + } + + auto &inputs = net.cell_inputs_map.at(cell); + dfs_path_stack.push(std::make_pair(inputs.begin(), inputs.end())); + cells_visited.insert(cell); + sig = (*dfs_path_stack.top().first); + return *this; + } +}; + +struct NetlistConeWireIterable { + const Netlist &net; + RTLIL::SigBit sig; + CellTypes *cell_filter; + + NetlistConeWireIterable(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) : net(net), sig(sig), cell_filter(cell_filter) + { + } + + NetlistConeWireIter begin() { return NetlistConeWireIter(net, sig, cell_filter); } + NetlistConeWireIter end() { return NetlistConeWireIter(net); } +}; + +struct NetlistConeCellIter : public std::iterator { + const Netlist &net; + + NetlistConeWireIter sig_iter; + + NetlistConeCellIter(const Netlist &net) : net(net), sig_iter(net) {} + + NetlistConeCellIter(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) : net(net), sig_iter(net, sig, cell_filter) + { + if ((!sig_iter.sentinel) && (!has_driver_cell(*sig_iter))) { + ++(*this); + } + } + + bool has_driver_cell(const RTLIL::SigBit &s) { return net.sigbit_driver_map.count(s); } + + RTLIL::Cell *operator*() const { return net.sigbit_driver_map.at(*sig_iter); }; + + bool operator!=(const NetlistConeCellIter &other) const { return sig_iter != other.sig_iter; } + bool operator==(const NetlistConeCellIter &other) const { return sig_iter == other.sig_iter; } + NetlistConeCellIter &operator++() + { + while (true) { + ++sig_iter; + if (sig_iter.sentinel) { + return *this; + } + + RTLIL::Cell* cell = net.driver_cell(*sig_iter); + + if (!cell) { + continue; + } + + if ((sig_iter.cell_filter) && (!sig_iter.cell_filter->cell_known(cell->type))) { + continue; + } + + if (!sig_iter.cells_visited.count(cell)) { + return *this; + } + } + } +}; + +struct NetlistConeCellIterable { + const Netlist &net; + RTLIL::SigBit sig; + CellTypes *cell_filter; + + NetlistConeCellIterable(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) : net(net), sig(sig), cell_filter(cell_filter) + { + } + + NetlistConeCellIter begin() { return NetlistConeCellIter(net, sig, cell_filter); } + NetlistConeCellIter end() { return NetlistConeCellIter(net); } +}; + +// struct NetlistConeInputsIter : public std::iterator { +// const Netlist &net; +// RTLIL::SigBit sig; + +// NetlistConeWireIter sig_iter; + +// bool has_driver_cell(const RTLIL::SigBit &s) { return net.sigbit_driver_map.count(s); } + +// NetlistConeInputsIter(const Netlist &net, RTLIL::SigBit sig = NULL) : net(net), sig(sig), sig_iter(net, sig) +// { +// if ((sig != NULL) && (has_driver_cell(sig_iter))) { +// ++(*this); +// } +// } + +// const RTLIL::SigBit &operator*() const { return sig_iter; }; +// bool operator!=(const NetlistConeInputsIter &other) const { return sig_iter != other.sig_iter; } +// bool operator==(const NetlistConeInputsIter &other) const { return sig_iter == other.sig_iter; } +// NetlistConeInputsIter &operator++() +// { +// do { +// ++sig_iter; +// if (sig_iter->empty()) { +// return *this; +// } +// } while (has_driver_cell(sig_iter)); + +// return *this; +// } +// }; + +// struct NetlistConeInputsIterable { +// const Netlist &net; +// RTLIL::SigBit sig; + +// NetlistConeInputsIterable(const Netlist &net, RTLIL::SigBit sig) : net(net), sig(sig) {} + +// NetlistConeInputsIter begin() { return NetlistConeInputsIter(net, sig); } +// NetlistConeInputsIter end() { return NetlistConeInputsIter(net); } +// }; +} // namespace detail + +detail::NetlistConeWireIterable cone(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) +{ + return detail::NetlistConeWireIterable(net, net.sigmap(sig), cell_filter = cell_filter); +} + +// detail::NetlistConeInputsIterable cone_inputs(RTLIL::SigBit sig) { return NetlistConeInputsIterable(this, &sig); } +detail::NetlistConeCellIterable cell_cone(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) +{ + return detail::NetlistConeCellIterable(net, net.sigmap(sig), cell_filter); +} + +YOSYS_NAMESPACE_END + +#endif diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index f44e6e58c..0ab91ca9e 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -21,8 +21,8 @@ #include "kernel/register.h" #include "kernel/rtlil.h" #include "kernel/satgen.h" -#include "kernel/algo.h" #include "kernel/sigtools.h" +#include "netlist.h" #include #include -- cgit v1.2.3 From 2454ad99bf49afe752d6fd1c1567f59ee9e26736 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 20 Jun 2019 13:44:21 +0200 Subject: Refactor "opt_rmdff -sat" Signed-off-by: Clifford Wolf --- passes/opt/netlist.h | 317 ------------------------------------------------ passes/opt/opt_rmdff.cc | 88 +++++++------- 2 files changed, 46 insertions(+), 359 deletions(-) delete mode 100644 passes/opt/netlist.h (limited to 'passes') diff --git a/passes/opt/netlist.h b/passes/opt/netlist.h deleted file mode 100644 index f029ad6ab..000000000 --- a/passes/opt/netlist.h +++ /dev/null @@ -1,317 +0,0 @@ -/* -*- c++ -*- - * yosys -- Yosys Open SYnthesis Suite - * - * Copyright (C) 2012 Clifford Wolf - * - * Permission to use, copy, modify, and/or distribute this software for any - * purpose with or without fee is hereby granted, provided that the above - * copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES - * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF - * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR - * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES - * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN - * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF - * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. - * - */ - -#ifndef SATGEN_ALGO_H -#define SATGEN_ALGO_H - -#include "kernel/celltypes.h" -#include "kernel/rtlil.h" -#include "kernel/sigtools.h" -#include - -YOSYS_NAMESPACE_BEGIN - -CellTypes comb_cells_filt() -{ - CellTypes ct; - - ct.setup_internals(); - ct.setup_stdcells(); - - return ct; -} - -struct Netlist { - RTLIL::Module *module; - SigMap sigmap; - CellTypes ct; - dict sigbit_driver_map; - dict> cell_inputs_map; - - Netlist(RTLIL::Module *module) : module(module), sigmap(module), ct(module->design) { setup_netlist(module, ct); } - - Netlist(RTLIL::Module *module, const CellTypes &ct) : module(module), sigmap(module), ct(ct) { setup_netlist(module, ct); } - - RTLIL::Cell *driver_cell(RTLIL::SigBit sig) const - { - sig = sigmap(sig); - if (!sigbit_driver_map.count(sig)) { - return NULL; - } - - return sigbit_driver_map.at(sig); - } - - RTLIL::SigSpec driver_port(RTLIL::SigBit sig) - { - RTLIL::Cell *cell = driver_cell(sig); - - if (!cell) { - return RTLIL::SigSpec(); - } - - for (auto &port : cell->connections_) { - if (ct.cell_output(cell->type, port.first)) { - RTLIL::SigSpec port_sig = sigmap(port.second); - for (int i = 0; i < GetSize(port_sig); i++) { - if (port_sig[i] == sig) { - return port.second[i]; - } - } - } - } - - return RTLIL::SigSpec(); - } - - void setup_netlist(RTLIL::Module *module, const CellTypes &ct) - { - for (auto cell : module->cells()) { - if (ct.cell_known(cell->type)) { - std::set inputs, outputs; - for (auto &port : cell->connections()) { - std::vector bits = sigmap(port.second).to_sigbit_vector(); - if (ct.cell_output(cell->type, port.first)) - outputs.insert(bits.begin(), bits.end()); - else - inputs.insert(bits.begin(), bits.end()); - } - cell_inputs_map[cell] = inputs; - for (auto &bit : outputs) { - sigbit_driver_map[bit] = cell; - }; - } - } - } -}; - -namespace detail -{ -struct NetlistConeWireIter : public std::iterator { - using set_iter_t = std::set::iterator; - - const Netlist &net; - RTLIL::SigBit sig; - bool sentinel; - CellTypes *cell_filter; - - std::stack> dfs_path_stack; - std::set cells_visited; - - NetlistConeWireIter(const Netlist &net) : net(net), sentinel(true), cell_filter(NULL) {} - - NetlistConeWireIter(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) - : net(net), sig(sig), sentinel(false), cell_filter(cell_filter) - { - } - - const RTLIL::SigBit &operator*() const { return sig; }; - bool operator!=(const NetlistConeWireIter &other) const - { - if (sentinel || other.sentinel) { - return sentinel != other.sentinel; - } else { - return sig != other.sig; - } - } - - bool operator==(const NetlistConeWireIter &other) const - { - if (sentinel || other.sentinel) { - return sentinel == other.sentinel; - } else { - return sig == other.sig; - } - } - - void next_sig_in_dag() - { - while (1) { - if (dfs_path_stack.empty()) { - sentinel = true; - return; - } - - auto &cell_inputs_iter = dfs_path_stack.top().first; - auto &cell_inputs_iter_guard = dfs_path_stack.top().second; - - cell_inputs_iter++; - if (cell_inputs_iter != cell_inputs_iter_guard) { - sig = *cell_inputs_iter; - return; - } else { - dfs_path_stack.pop(); - } - } - } - - NetlistConeWireIter &operator++() - { - RTLIL::Cell *cell = net.driver_cell(sig); - - if (!cell) { - next_sig_in_dag(); - return *this; - } - - if (cells_visited.count(cell)) { - next_sig_in_dag(); - return *this; - } - - if ((cell_filter) && (!cell_filter->cell_known(cell->type))) { - next_sig_in_dag(); - return *this; - } - - auto &inputs = net.cell_inputs_map.at(cell); - dfs_path_stack.push(std::make_pair(inputs.begin(), inputs.end())); - cells_visited.insert(cell); - sig = (*dfs_path_stack.top().first); - return *this; - } -}; - -struct NetlistConeWireIterable { - const Netlist &net; - RTLIL::SigBit sig; - CellTypes *cell_filter; - - NetlistConeWireIterable(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) : net(net), sig(sig), cell_filter(cell_filter) - { - } - - NetlistConeWireIter begin() { return NetlistConeWireIter(net, sig, cell_filter); } - NetlistConeWireIter end() { return NetlistConeWireIter(net); } -}; - -struct NetlistConeCellIter : public std::iterator { - const Netlist &net; - - NetlistConeWireIter sig_iter; - - NetlistConeCellIter(const Netlist &net) : net(net), sig_iter(net) {} - - NetlistConeCellIter(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) : net(net), sig_iter(net, sig, cell_filter) - { - if ((!sig_iter.sentinel) && (!has_driver_cell(*sig_iter))) { - ++(*this); - } - } - - bool has_driver_cell(const RTLIL::SigBit &s) { return net.sigbit_driver_map.count(s); } - - RTLIL::Cell *operator*() const { return net.sigbit_driver_map.at(*sig_iter); }; - - bool operator!=(const NetlistConeCellIter &other) const { return sig_iter != other.sig_iter; } - bool operator==(const NetlistConeCellIter &other) const { return sig_iter == other.sig_iter; } - NetlistConeCellIter &operator++() - { - while (true) { - ++sig_iter; - if (sig_iter.sentinel) { - return *this; - } - - RTLIL::Cell* cell = net.driver_cell(*sig_iter); - - if (!cell) { - continue; - } - - if ((sig_iter.cell_filter) && (!sig_iter.cell_filter->cell_known(cell->type))) { - continue; - } - - if (!sig_iter.cells_visited.count(cell)) { - return *this; - } - } - } -}; - -struct NetlistConeCellIterable { - const Netlist &net; - RTLIL::SigBit sig; - CellTypes *cell_filter; - - NetlistConeCellIterable(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) : net(net), sig(sig), cell_filter(cell_filter) - { - } - - NetlistConeCellIter begin() { return NetlistConeCellIter(net, sig, cell_filter); } - NetlistConeCellIter end() { return NetlistConeCellIter(net); } -}; - -// struct NetlistConeInputsIter : public std::iterator { -// const Netlist &net; -// RTLIL::SigBit sig; - -// NetlistConeWireIter sig_iter; - -// bool has_driver_cell(const RTLIL::SigBit &s) { return net.sigbit_driver_map.count(s); } - -// NetlistConeInputsIter(const Netlist &net, RTLIL::SigBit sig = NULL) : net(net), sig(sig), sig_iter(net, sig) -// { -// if ((sig != NULL) && (has_driver_cell(sig_iter))) { -// ++(*this); -// } -// } - -// const RTLIL::SigBit &operator*() const { return sig_iter; }; -// bool operator!=(const NetlistConeInputsIter &other) const { return sig_iter != other.sig_iter; } -// bool operator==(const NetlistConeInputsIter &other) const { return sig_iter == other.sig_iter; } -// NetlistConeInputsIter &operator++() -// { -// do { -// ++sig_iter; -// if (sig_iter->empty()) { -// return *this; -// } -// } while (has_driver_cell(sig_iter)); - -// return *this; -// } -// }; - -// struct NetlistConeInputsIterable { -// const Netlist &net; -// RTLIL::SigBit sig; - -// NetlistConeInputsIterable(const Netlist &net, RTLIL::SigBit sig) : net(net), sig(sig) {} - -// NetlistConeInputsIter begin() { return NetlistConeInputsIter(net, sig); } -// NetlistConeInputsIter end() { return NetlistConeInputsIter(net); } -// }; -} // namespace detail - -detail::NetlistConeWireIterable cone(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) -{ - return detail::NetlistConeWireIterable(net, net.sigmap(sig), cell_filter = cell_filter); -} - -// detail::NetlistConeInputsIterable cone_inputs(RTLIL::SigBit sig) { return NetlistConeInputsIterable(this, &sig); } -detail::NetlistConeCellIterable cell_cone(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) -{ - return detail::NetlistConeCellIterable(net, net.sigmap(sig), cell_filter); -} - -YOSYS_NAMESPACE_END - -#endif diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index 0ab91ca9e..5fc28ae92 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -22,7 +22,6 @@ #include "kernel/rtlil.h" #include "kernel/satgen.h" #include "kernel/sigtools.h" -#include "netlist.h" #include #include @@ -31,9 +30,8 @@ PRIVATE_NAMESPACE_BEGIN SigMap assign_map, dff_init_map; SigSet mux_drivers; +dict bit2driver; dict> init_attributes; -std::map netlists; -std::map comb_filters; bool keepdc; bool sat; @@ -459,41 +457,46 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) dff->unsetPort("\\E"); } - if (sat && has_init) { + if (sat && has_init && (!sig_r.size() || val_init == val_rv)) + { bool removed_sigbits = false; - // Create netlist for the module if not already available - if (!netlists.count(mod)) { - netlists.emplace(mod, Netlist(mod)); - comb_filters.emplace(mod, comb_cells_filt()); - } - - // Load netlist for the module from the pool - Netlist &net = netlists.at(mod); - + ezSatPtr ez; + SatGen satgen(ez.get(), &assign_map); + pool sat_cells; + + std::function 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)) { + if ((!q_sigbit.wire) || (!d_sigbit.wire)) continue; - } - ezSatPtr ez; - SatGen satgen(ez.get(), &net.sigmap); + if (!bit2driver.count(d_sigbit)) + continue; - // Create SAT instance only for the cells that influence the register bit combinatorially - for (const auto &cell : cell_cone(net, d_sigbit, &comb_filters.at(mod))) { - if (!satgen.importCell(cell)) - log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name), - RTLIL::id2cstr(cell->type)); - } + sat_import_cell(bit2driver.at(d_sigbit)); - RTLIL::Const sigbit_init_val = val_init.extract(position); - int init_sat_pi = satgen.importSigSpec(sigbit_init_val).front(); + 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); @@ -501,24 +504,21 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff) 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) { - - RTLIL::SigSpec driver_port = net.driver_port(q_sigbit); - RTLIL::Wire *dummy_wire = mod->addWire(NEW_ID, 1); - - for (auto &conn : mod->connections_) - net.sigmap(conn.first).replace(driver_port, dummy_wire, &conn.first); - - remove_init_attr(driver_port); - driver_port = dummy_wire; + 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)); - mod->connect(RTLIL::SigSig(q_sigbit, sigbit_init_val)); + 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; } } @@ -566,8 +566,6 @@ struct OptRmdffPass : public Pass { break; } extra_args(args, argidx, design); - netlists.clear(); - comb_filters.clear(); for (auto module : design->selected_modules()) { pool driven_bits; @@ -576,6 +574,7 @@ struct OptRmdffPass : public Pass { assign_map.set(module); dff_init_map.set(module); mux_drivers.clear(); + bit2driver.clear(); init_attributes.clear(); for (auto wire : module->wires()) @@ -600,17 +599,21 @@ struct OptRmdffPass : public Pass { driven_bits.insert(bit); } } - mux_drivers.clear(); std::vector dff_list; std::vector dffsr_list; std::vector 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()) @@ -682,6 +685,7 @@ struct OptRmdffPass : public Pass { assign_map.clear(); mux_drivers.clear(); + bit2driver.clear(); init_attributes.clear(); if (total_count || total_initdrv) -- cgit v1.2.3 From 35fa7b30574244e4f99373f2a790f004b4a1dbbb Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Thu, 27 Jun 2019 22:02:12 +0200 Subject: Fix memory leak when one of multiple DFF cells is removed in opt_rmdff When there are multiple DFFs and one of them is removed, its reference lingers inside bit2driver dict. While invoking handle_dff() function for other DFFs, this broken reference is used isnside sat_import_cell() function. --- passes/opt/opt_rmdff.cc | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'passes') diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index 5fc28ae92..17e0d7cd4 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -530,6 +530,11 @@ 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; } -- cgit v1.2.3 From 3225bfb98403271bbe8a56418ccd027b42eabda1 Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Thu, 27 Jun 2019 22:06:23 +0200 Subject: Add help for "-sat" option inside opt_rmdff. "opt" can pass "-sat" too --- passes/opt/opt.cc | 8 ++++++-- passes/opt/opt_rmdff.cc | 4 ++++ 2 files changed, 10 insertions(+), 2 deletions(-) (limited to 'passes') 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 \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 \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 17e0d7cd4..be6ac2d30 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -549,6 +549,10 @@ struct OptRmdffPass : public Pass { 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 args, RTLIL::Design *design) YS_OVERRIDE { -- cgit v1.2.3 From 6bf73e3546450671660e793991c982eeadf1872e Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 15:15:56 -0700 Subject: Cleanup abc9.cc --- passes/techmap/abc9.cc | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) (limited to 'passes') diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index b4f15d6a1..f25b02a88 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -80,7 +80,7 @@ void handle_loops(RTLIL::Design *design) { Pass::call(design, "scc -set_attr abc_scc_id {}"); - dict> module_break; + dict> 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 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,17 +553,20 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri signal = std::move(bits); } + dict abc_box; vector boxes; - for (auto it = module->cells_.begin(); it != module->cells_.end(); ) { - RTLIL::Cell* cell = it->second; - if (cell->type.in("$_AND_", "$_NOT_", "$__ABC_FF_")) { - it = module->remove(it); + for (auto cell : module->cells()) { + 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")) - boxes.emplace_back(it->second); - ++it; + auto it = abc_box.find(cell->type); + if (it == abc_box.end()) { + RTLIL::Module* box_module = design->module(cell->type); + it = abc_box.insert(std::make_pair(cell->type, box_module && box_module->attributes.count("\\abc_box_id"))).first; + } + if (it->second) + boxes.emplace_back(cell); } std::map cell_stats; -- cgit v1.2.3 From 137c91d9a98e05199b7acfe1d63139b79d278277 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 15:17:39 -0700 Subject: Remove &retime when abc9 -fast --- passes/techmap/abc9.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'passes') diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index f25b02a88..e2a82f0c8 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" -- cgit v1.2.3 From a625854ac5e2ff3d6bf11e97b7ac676b362e7461 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 15:29:20 -0700 Subject: Do not use Module::remove() iterator version --- passes/techmap/abc9.cc | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'passes') diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index e2a82f0c8..3721b82b7 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -555,17 +555,18 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri dict abc_box; vector boxes; - for (auto cell : module->cells()) { + for (const auto &it : module->cells_) { + auto cell = it.second; if (cell->type.in("$_AND_", "$_NOT_")) { module->remove(cell); continue; } - auto it = abc_box.find(cell->type); - if (it == abc_box.end()) { + auto jt = abc_box.find(cell->type); + if (jt == abc_box.end()) { RTLIL::Module* box_module = design->module(cell->type); - it = abc_box.insert(std::make_pair(cell->type, box_module && box_module->attributes.count("\\abc_box_id"))).first; + jt = abc_box.insert(std::make_pair(cell->type, box_module && box_module->attributes.count("\\abc_box_id"))).first; } - if (it->second) + if (jt->second) boxes.emplace_back(cell); } -- cgit v1.2.3