diff --git a/kernel/celltypes.h b/kernel/celltypes.h index 4e91eddda..758661c02 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -246,24 +246,24 @@ struct CellTypes cell_types.clear(); } - bool cell_known(RTLIL::IdString type) + bool cell_known(RTLIL::IdString type) const { return cell_types.count(type) != 0; } - bool cell_output(RTLIL::IdString type, RTLIL::IdString port) + bool cell_output(RTLIL::IdString type, RTLIL::IdString port) const { auto it = cell_types.find(type); return it != cell_types.end() && it->second.outputs.count(port) != 0; } - bool cell_input(RTLIL::IdString type, RTLIL::IdString port) + bool cell_input(RTLIL::IdString type, RTLIL::IdString port) const { auto it = cell_types.find(type); return it != cell_types.end() && it->second.inputs.count(port) != 0; } - bool cell_evaluable(RTLIL::IdString type) + bool cell_evaluable(RTLIL::IdString type) const { auto it = cell_types.find(type); return it != cell_types.end() && it->second.is_evaluable; @@ -482,4 +482,3 @@ extern CellTypes yosys_celltypes; YOSYS_NAMESPACE_END #endif - 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 eeb992a3e..be6ac2d30 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -17,19 +17,24 @@ * */ -#include "kernel/register.h" -#include "kernel/sigtools.h" #include "kernel/log.h" -#include +#include "kernel/register.h" +#include "kernel/rtlil.h" +#include "kernel/satgen.h" +#include "kernel/sigtools.h" #include +#include USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN SigMap assign_map, dff_init_map; SigSet mux_drivers; +dict bit2driver; dict> 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 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)) + 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 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 driven_bits; dict 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 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()) @@ -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/tests/opt/opt_ff_sat.v b/tests/opt/opt_ff_sat.v new file mode 100644 index 000000000..5a0a6fe37 --- /dev/null +++ b/tests/opt/opt_ff_sat.v @@ -0,0 +1,12 @@ +module top ( + input clk, + output reg [7:0] cnt +); + initial cnt = 0; + always @(posedge clk) begin + if (cnt < 20) + cnt <= cnt + 1; + else + cnt <= 0; + end +endmodule diff --git a/tests/opt/opt_ff_sat.ys b/tests/opt/opt_ff_sat.ys new file mode 100644 index 000000000..4e7cc6ca4 --- /dev/null +++ b/tests/opt/opt_ff_sat.ys @@ -0,0 +1,5 @@ +read_verilog opt_ff_sat.v +prep -flatten +opt_rmdff -sat +synth +select -assert-count 5 t:$_DFF_P_