From 9a468f81c412f8b63d25e739f28932815c6882fb Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Tue, 28 May 2019 08:48:21 +0200 Subject: [PATCH 01/13] 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 +++ tests/opt/opt_ff_sat.v | 15 +++++++++++ tests/opt/opt_ff_sat.ys | 4 +++ 4 files changed, 78 insertions(+), 3 deletions(-) create mode 100644 tests/opt/opt_ff_sat.v create mode 100644 tests/opt/opt_ff_sat.ys 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) diff --git a/tests/opt/opt_ff_sat.v b/tests/opt/opt_ff_sat.v new file mode 100644 index 000000000..fc1e61980 --- /dev/null +++ b/tests/opt/opt_ff_sat.v @@ -0,0 +1,15 @@ +module top( + input clk, + input a, + output b + ); + reg b_reg; + initial begin + b_reg <= 0; + end + + assign b = b_reg; + always @(posedge clk) begin + b_reg <= a && b_reg; + end +endmodule diff --git a/tests/opt/opt_ff_sat.ys b/tests/opt/opt_ff_sat.ys new file mode 100644 index 000000000..13e4ad29b --- /dev/null +++ b/tests/opt/opt_ff_sat.ys @@ -0,0 +1,4 @@ +read_verilog opt_ff_sat.v +prep -flatten +opt_rmdff -sat +synth From 29a78267d7c84699bdcebfa87719b31d9b65909b Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Tue, 28 May 2019 15:45:04 +0200 Subject: [PATCH 02/13] Fix the regression --- passes/sat/sat.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 { From d097f423d1b30a3936388bb93a0a88fd3527ad49 Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Mon, 10 Jun 2019 21:42:35 +0200 Subject: [PATCH 03/13] Refactor driver map generation - Implement iterators over the driver map that enumerate signals and cells within the cones of the signal --- kernel/satgen_algo.h | 158 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 158 insertions(+) create mode 100644 kernel/satgen_algo.h diff --git a/kernel/satgen_algo.h b/kernel/satgen_algo.h new file mode 100644 index 000000000..483dfad5c --- /dev/null +++ b/kernel/satgen_algo.h @@ -0,0 +1,158 @@ +/* -*- 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 + +struct DriverMap : public std::map>> { + RTLIL::Module *module; + SigMap sigmap; + + using map_t = std::map>>; + + struct DriverMapConeWireIterator : public std::iterator { + using set_iter_t = std::set::iterator; + + DriverMap *drvmap; + const RTLIL::SigBit *sig; + std::stack> dfs; + + DriverMapConeWireIterator(DriverMap *drvmap) : DriverMapConeWireIterator(drvmap, NULL) {} + + DriverMapConeWireIterator(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {} + + inline const RTLIL::SigBit &operator*() const { return *sig; }; + inline bool operator!=(const DriverMapConeWireIterator &other) const { return sig != other.sig; } + inline bool operator==(const DriverMapConeWireIterator &other) const { return sig == other.sig; } + inline void operator++() + { + if (drvmap->count(*sig)) { + std::pair> &drv = drvmap->at(*sig); + dfs.push(std::make_pair(drv.second.begin(), drv.second.end())); + sig = &(*dfs.top().first); + } else { + while (1) { + auto &inputs_iter = dfs.top(); + + inputs_iter.first++; + if (inputs_iter.first != inputs_iter.second) { + sig = &(*inputs_iter.first); + return; + } else { + dfs.pop(); + if (dfs.empty()) { + sig = NULL; + return; + } + } + } + } + } + }; + + struct DriverMapConeWireIterable { + DriverMap *drvmap; + const RTLIL::SigBit *sig; + + DriverMapConeWireIterable(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {} + + inline DriverMapConeWireIterator begin() { return DriverMapConeWireIterator(drvmap, sig); } + inline DriverMapConeWireIterator end() { return DriverMapConeWireIterator(drvmap); } + }; + + struct DriverMapConeCellIterator : public std::iterator { + DriverMap *drvmap; + const RTLIL::SigBit *sig; + + DriverMapConeWireIterator sig_iter; + + DriverMapConeCellIterator(DriverMap *drvmap) : DriverMapConeCellIterator(drvmap, NULL) {} + + DriverMapConeCellIterator(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig), sig_iter(drvmap, sig) + { + if ((sig != NULL) && (!drvmap->count(*sig_iter))) { + ++(*this); + } + } + + inline RTLIL::Cell *operator*() const + { + std::pair> &drv = drvmap->at(*sig); + return drv.first; + }; + inline bool operator!=(const DriverMapConeCellIterator &other) const { return sig_iter != other.sig_iter; } + inline bool operator==(const DriverMapConeCellIterator &other) const { return sig_iter == other.sig_iter; } + inline void operator++() + { + do { + ++sig_iter; + if (sig_iter.sig == NULL) { + return; + } + } while (!drvmap->count(*sig_iter)); + } + }; + + struct DriverMapConeCellIterable { + DriverMap *drvmap; + const RTLIL::SigBit *sig; + + DriverMapConeCellIterable(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {} + + inline DriverMapConeCellIterator begin() { return DriverMapConeCellIterator(drvmap, sig); } + inline DriverMapConeCellIterator end() { return DriverMapConeCellIterator(drvmap); } + }; + + DriverMap(RTLIL::Module *module) : module(module), sigmap(module) + { + CellTypes ct; + ct.setup_internals(); + ct.setup_stdcells(); + + for (auto &it : module->cells_) { + if (ct.cell_known(it.second->type)) { + std::set inputs, outputs; + for (auto &port : it.second->connections()) { + std::vector bits = sigmap(port.second).to_sigbit_vector(); + if (ct.cell_output(it.second->type, port.first)) + outputs.insert(bits.begin(), bits.end()); + else + inputs.insert(bits.begin(), bits.end()); + } + std::pair> drv(it.second, inputs); + for (auto &bit : outputs) + (*this)[bit] = drv; + } + } + } + + DriverMapConeWireIterable cone(const RTLIL::SigBit &sig) { return DriverMapConeWireIterable(this, &sig); } + DriverMapConeCellIterable cell_cone(const RTLIL::SigBit &sig) { return DriverMapConeCellIterable(this, &sig); } +}; + +YOSYS_NAMESPACE_END + +#endif From 9892df17efadd0eafe5217e812fb4cec2bfdf6e5 Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Tue, 11 Jun 2019 11:47:13 +0200 Subject: [PATCH 04/13] Generate satgen instance instead of calling sat pass --- kernel/satgen_algo.h | 45 ++++++++++++++++- passes/opt/opt_rmdff.cc | 106 +++++++++++++++++++++++++++++++--------- 2 files changed, 128 insertions(+), 23 deletions(-) diff --git a/kernel/satgen_algo.h b/kernel/satgen_algo.h index 483dfad5c..d475d7d64 100644 --- a/kernel/satgen_algo.h +++ b/kernel/satgen_algo.h @@ -100,7 +100,7 @@ struct DriverMap : public std::map> &drv = drvmap->at(*sig); + std::pair> &drv = drvmap->at(*sig_iter); return drv.first; }; inline bool operator!=(const DriverMapConeCellIterator &other) const { return sig_iter != other.sig_iter; } @@ -126,6 +126,48 @@ struct DriverMap : public std::map { + DriverMap *drvmap; + const RTLIL::SigBit *sig; + + DriverMapConeWireIterator sig_iter; + + DriverMapConeInputsIterator(DriverMap *drvmap) : DriverMapConeInputsIterator(drvmap, NULL) {} + + DriverMapConeInputsIterator(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig), sig_iter(drvmap, sig) + { + if ((sig != NULL) && (drvmap->count(*sig_iter))) { + ++(*this); + } + } + + inline const RTLIL::SigBit& operator*() const + { + return *sig_iter; + }; + inline bool operator!=(const DriverMapConeInputsIterator &other) const { return sig_iter != other.sig_iter; } + inline bool operator==(const DriverMapConeInputsIterator &other) const { return sig_iter == other.sig_iter; } + inline void operator++() + { + do { + ++sig_iter; + if (sig_iter.sig == NULL) { + return; + } + } while (drvmap->count(*sig_iter)); + } + }; + + struct DriverMapConeInputsIterable { + DriverMap *drvmap; + const RTLIL::SigBit *sig; + + DriverMapConeInputsIterable(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {} + + inline DriverMapConeInputsIterator begin() { return DriverMapConeInputsIterator(drvmap, sig); } + inline DriverMapConeInputsIterator end() { return DriverMapConeInputsIterator(drvmap); } + }; + DriverMap(RTLIL::Module *module) : module(module), sigmap(module) { CellTypes ct; @@ -150,6 +192,7 @@ struct DriverMap : public std::map +#include "kernel/register.h" +#include "kernel/rtlil.h" +#include "kernel/satgen.h" +#include "kernel/satgen_algo.h" +#include "kernel/sigtools.h" #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); + // 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(); + // 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() - ); + // 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); From d69989b8d27eea16d793600b1779661f31161c6c Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Wed, 12 Jun 2019 19:35:05 +0200 Subject: [PATCH 05/13] Rename satgen_algo.h -> algo.h, code cleanup and refactoring --- kernel/algo.h | 239 ++++++++++++++++++++++++++++++++++++++++ kernel/celltypes.h | 9 +- kernel/satgen_algo.h | 201 --------------------------------- passes/opt/opt_rmdff.cc | 93 ++++------------ 4 files changed, 264 insertions(+), 278 deletions(-) create mode 100644 kernel/algo.h delete mode 100644 kernel/satgen_algo.h diff --git a/kernel/algo.h b/kernel/algo.h new file mode 100644 index 000000000..6ab96a875 --- /dev/null +++ b/kernel/algo.h @@ -0,0 +1,239 @@ +/* -*- 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; + dict sigbit_driver_map; + dict> cell_inputs_map; + + Netlist(RTLIL::Module *module) : module(module), sigmap(module) + { + CellTypes ct(module->design); + setup_netlist(module, ct); + } + + Netlist(RTLIL::Module *module, const CellTypes &ct) : module(module), sigmap(module) { setup_netlist(module, ct); } + + 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; + const RTLIL::SigBit *p_sig; + std::stack> dfs_path_stack; + std::set cells_visited; + + NetlistConeWireIter(const Netlist &net, const RTLIL::SigBit *p_sig = NULL) : net(net), p_sig(p_sig) {} + + const RTLIL::SigBit &operator*() const { return *p_sig; }; + bool operator!=(const NetlistConeWireIter &other) const { return p_sig != other.p_sig; } + bool operator==(const NetlistConeWireIter &other) const { return p_sig == other.p_sig; } + + void next_sig_in_dag() + { + while (1) { + if (dfs_path_stack.empty()) { + p_sig = NULL; + 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) { + p_sig = &(*cell_inputs_iter); + return; + } else { + dfs_path_stack.pop(); + } + } + } + + NetlistConeWireIter &operator++() + { + if (net.sigbit_driver_map.count(*p_sig)) { + auto drv = net.sigbit_driver_map.at(*p_sig); + + if (!cells_visited.count(drv)) { + auto &inputs = net.cell_inputs_map.at(drv); + dfs_path_stack.push(std::make_pair(inputs.begin(), inputs.end())); + cells_visited.insert(drv); + p_sig = &(*dfs_path_stack.top().first); + } else { + next_sig_in_dag(); + } + } else { + next_sig_in_dag(); + } + return *this; + } +}; + +struct NetlistConeWireIterable { + const Netlist &net; + const RTLIL::SigBit *p_sig; + + NetlistConeWireIterable(const Netlist &net, const RTLIL::SigBit *p_sig) : net(net), p_sig(p_sig) {} + + NetlistConeWireIter begin() { return NetlistConeWireIter(net, p_sig); } + NetlistConeWireIter end() { return NetlistConeWireIter(net); } +}; + +struct NetlistConeCellIter : public std::iterator { + const Netlist &net; + const RTLIL::SigBit *p_sig; + + NetlistConeWireIter sig_iter; + + NetlistConeCellIter(const Netlist &net, const RTLIL::SigBit *p_sig = NULL) : net(net), p_sig(p_sig), sig_iter(net, p_sig) + { + if ((p_sig != NULL) && (!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.p_sig == NULL) { + return *this; + } + + if (has_driver_cell(*sig_iter)) { + auto cell = net.sigbit_driver_map.at(*sig_iter); + + if (!sig_iter.cells_visited.count(cell)) { + return *this; + } + } + }; + } +}; + +struct NetlistConeCellIterable { + const Netlist &net; + const RTLIL::SigBit *p_sig; + + NetlistConeCellIterable(const Netlist &net, const RTLIL::SigBit *p_sig) : net(net), p_sig(p_sig) {} + + NetlistConeCellIter begin() { return NetlistConeCellIter(net, p_sig); } + NetlistConeCellIter end() { return NetlistConeCellIter(net); } +}; + +struct NetlistConeInputsIter : public std::iterator { + const Netlist &net; + const RTLIL::SigBit *p_sig; + + NetlistConeWireIter sig_iter; + + bool has_driver_cell(const RTLIL::SigBit &s) { return net.sigbit_driver_map.count(s); } + + NetlistConeInputsIter(const Netlist &net, const RTLIL::SigBit *p_sig = NULL) : net(net), p_sig(p_sig), sig_iter(net, p_sig) + { + if ((p_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.p_sig == NULL) { + return *this; + } + } while (has_driver_cell(*sig_iter)); + + return *this; + } +}; + +struct NetlistConeInputsIterable { + const Netlist &net; + const RTLIL::SigBit *p_sig; + + NetlistConeInputsIterable(const Netlist &net, const RTLIL::SigBit *p_sig) : net(net), p_sig(p_sig) {} + + NetlistConeInputsIter begin() { return NetlistConeInputsIter(net, p_sig); } + NetlistConeInputsIter end() { return NetlistConeInputsIter(net); } +}; +} // namespace detail + +detail::NetlistConeWireIterable cone(const Netlist &net, const RTLIL::SigBit &sig) { return detail::NetlistConeWireIterable(net, &sig); } + +// detail::NetlistConeInputsIterable cone_inputs(const RTLIL::SigBit &sig) { return NetlistConeInputsIterable(this, &sig); } +detail::NetlistConeCellIterable cell_cone(const Netlist &net, const RTLIL::SigBit &sig) { return detail::NetlistConeCellIterable(net, &sig); } + +YOSYS_NAMESPACE_END + +#endif 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/kernel/satgen_algo.h b/kernel/satgen_algo.h deleted file mode 100644 index d475d7d64..000000000 --- a/kernel/satgen_algo.h +++ /dev/null @@ -1,201 +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 - -struct DriverMap : public std::map>> { - RTLIL::Module *module; - SigMap sigmap; - - using map_t = std::map>>; - - struct DriverMapConeWireIterator : public std::iterator { - using set_iter_t = std::set::iterator; - - DriverMap *drvmap; - const RTLIL::SigBit *sig; - std::stack> dfs; - - DriverMapConeWireIterator(DriverMap *drvmap) : DriverMapConeWireIterator(drvmap, NULL) {} - - DriverMapConeWireIterator(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {} - - inline const RTLIL::SigBit &operator*() const { return *sig; }; - inline bool operator!=(const DriverMapConeWireIterator &other) const { return sig != other.sig; } - inline bool operator==(const DriverMapConeWireIterator &other) const { return sig == other.sig; } - inline void operator++() - { - if (drvmap->count(*sig)) { - std::pair> &drv = drvmap->at(*sig); - dfs.push(std::make_pair(drv.second.begin(), drv.second.end())); - sig = &(*dfs.top().first); - } else { - while (1) { - auto &inputs_iter = dfs.top(); - - inputs_iter.first++; - if (inputs_iter.first != inputs_iter.second) { - sig = &(*inputs_iter.first); - return; - } else { - dfs.pop(); - if (dfs.empty()) { - sig = NULL; - return; - } - } - } - } - } - }; - - struct DriverMapConeWireIterable { - DriverMap *drvmap; - const RTLIL::SigBit *sig; - - DriverMapConeWireIterable(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {} - - inline DriverMapConeWireIterator begin() { return DriverMapConeWireIterator(drvmap, sig); } - inline DriverMapConeWireIterator end() { return DriverMapConeWireIterator(drvmap); } - }; - - struct DriverMapConeCellIterator : public std::iterator { - DriverMap *drvmap; - const RTLIL::SigBit *sig; - - DriverMapConeWireIterator sig_iter; - - DriverMapConeCellIterator(DriverMap *drvmap) : DriverMapConeCellIterator(drvmap, NULL) {} - - DriverMapConeCellIterator(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig), sig_iter(drvmap, sig) - { - if ((sig != NULL) && (!drvmap->count(*sig_iter))) { - ++(*this); - } - } - - inline RTLIL::Cell *operator*() const - { - std::pair> &drv = drvmap->at(*sig_iter); - return drv.first; - }; - inline bool operator!=(const DriverMapConeCellIterator &other) const { return sig_iter != other.sig_iter; } - inline bool operator==(const DriverMapConeCellIterator &other) const { return sig_iter == other.sig_iter; } - inline void operator++() - { - do { - ++sig_iter; - if (sig_iter.sig == NULL) { - return; - } - } while (!drvmap->count(*sig_iter)); - } - }; - - struct DriverMapConeCellIterable { - DriverMap *drvmap; - const RTLIL::SigBit *sig; - - DriverMapConeCellIterable(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {} - - inline DriverMapConeCellIterator begin() { return DriverMapConeCellIterator(drvmap, sig); } - inline DriverMapConeCellIterator end() { return DriverMapConeCellIterator(drvmap); } - }; - - struct DriverMapConeInputsIterator : public std::iterator { - DriverMap *drvmap; - const RTLIL::SigBit *sig; - - DriverMapConeWireIterator sig_iter; - - DriverMapConeInputsIterator(DriverMap *drvmap) : DriverMapConeInputsIterator(drvmap, NULL) {} - - DriverMapConeInputsIterator(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig), sig_iter(drvmap, sig) - { - if ((sig != NULL) && (drvmap->count(*sig_iter))) { - ++(*this); - } - } - - inline const RTLIL::SigBit& operator*() const - { - return *sig_iter; - }; - inline bool operator!=(const DriverMapConeInputsIterator &other) const { return sig_iter != other.sig_iter; } - inline bool operator==(const DriverMapConeInputsIterator &other) const { return sig_iter == other.sig_iter; } - inline void operator++() - { - do { - ++sig_iter; - if (sig_iter.sig == NULL) { - return; - } - } while (drvmap->count(*sig_iter)); - } - }; - - struct DriverMapConeInputsIterable { - DriverMap *drvmap; - const RTLIL::SigBit *sig; - - DriverMapConeInputsIterable(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {} - - inline DriverMapConeInputsIterator begin() { return DriverMapConeInputsIterator(drvmap, sig); } - inline DriverMapConeInputsIterator end() { return DriverMapConeInputsIterator(drvmap); } - }; - - DriverMap(RTLIL::Module *module) : module(module), sigmap(module) - { - CellTypes ct; - ct.setup_internals(); - ct.setup_stdcells(); - - for (auto &it : module->cells_) { - if (ct.cell_known(it.second->type)) { - std::set inputs, outputs; - for (auto &port : it.second->connections()) { - std::vector bits = sigmap(port.second).to_sigbit_vector(); - if (ct.cell_output(it.second->type, port.first)) - outputs.insert(bits.begin(), bits.end()); - else - inputs.insert(bits.begin(), bits.end()); - } - std::pair> drv(it.second, inputs); - for (auto &bit : outputs) - (*this)[bit] = drv; - } - } - } - - DriverMapConeWireIterable cone(const RTLIL::SigBit &sig) { return DriverMapConeWireIterable(this, &sig); } - DriverMapConeInputsIterable cone_inputs(const RTLIL::SigBit &sig) { return DriverMapConeInputsIterable(this, &sig); } - DriverMapConeCellIterable cell_cone(const RTLIL::SigBit &sig) { return DriverMapConeCellIterable(this, &sig); } -}; - -YOSYS_NAMESPACE_END - -#endif 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; + SatGen satgen(ez.get(), &net.sigmap); - 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); - } + 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)); } RTLIL::Const sigbit_init_val = val_init.extract(position); - int reg_init = satgen.importSigSpec(sigbit_init_val).front(); + int init_sat_pi = satgen.importSigSpec(sigbit_init_val).front(); - int output_a = satgen.importSigSpec(d_sigbit).front(); - modelExpressions.push_back(output_a); + int q_sat_pi = satgen.importSigBit(q_sigbit); + int d_sat_pi = satgen.importSigBit(d_sigbit); - 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)); - // } - // } + // 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; From 4912567cbff3c24e9cddea0b59287ec53321af7a Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Thu, 13 Jun 2019 15:42:45 +0200 Subject: [PATCH 06/13] Pass SigBit by value to Netlist algorithms --- kernel/algo.h | 133 ++++++++++++++++++++++++++++---------------------- 1 file changed, 76 insertions(+), 57 deletions(-) diff --git a/kernel/algo.h b/kernel/algo.h index 6ab96a875..05467c60a 100644 --- a/kernel/algo.h +++ b/kernel/algo.h @@ -74,25 +74,43 @@ struct Netlist { namespace detail { -struct NetlistConeWireIter : public std::iterator { +struct NetlistConeWireIter : public std::iterator { using set_iter_t = std::set::iterator; const Netlist &net; - const RTLIL::SigBit *p_sig; + RTLIL::SigBit sig; + bool sentinel; + std::stack> dfs_path_stack; std::set cells_visited; - NetlistConeWireIter(const Netlist &net, const RTLIL::SigBit *p_sig = NULL) : net(net), p_sig(p_sig) {} + NetlistConeWireIter(const Netlist &net) : net(net), sentinel(true) {} - const RTLIL::SigBit &operator*() const { return *p_sig; }; - bool operator!=(const NetlistConeWireIter &other) const { return p_sig != other.p_sig; } - bool operator==(const NetlistConeWireIter &other) const { return p_sig == other.p_sig; } + NetlistConeWireIter(const Netlist &net, RTLIL::SigBit sig) : net(net), sig(sig), sentinel(false) {} + + 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()) { - p_sig = NULL; + sentinel = true; return; } @@ -101,7 +119,7 @@ struct NetlistConeWireIter : public std::iterator { +struct NetlistConeCellIter : public std::iterator { const Netlist &net; - const RTLIL::SigBit *p_sig; NetlistConeWireIter sig_iter; - NetlistConeCellIter(const Netlist &net, const RTLIL::SigBit *p_sig = NULL) : net(net), p_sig(p_sig), sig_iter(net, p_sig) + NetlistConeCellIter(const Netlist &net) : net(net), sig_iter(net) {} + + NetlistConeCellIter(const Netlist &net, RTLIL::SigBit sig) : net(net), sig_iter(net, sig) { - if ((p_sig != NULL) && (!has_driver_cell(*sig_iter))) { + if ((!sig_iter.sentinel) && (!has_driver_cell(*sig_iter))) { ++(*this); } } @@ -162,7 +181,7 @@ struct NetlistConeCellIter : public std::iterator { - const Netlist &net; - const RTLIL::SigBit *p_sig; +// struct NetlistConeInputsIter : public std::iterator { +// const Netlist &net; +// RTLIL::SigBit sig; - NetlistConeWireIter sig_iter; +// NetlistConeWireIter sig_iter; - bool has_driver_cell(const RTLIL::SigBit &s) { return net.sigbit_driver_map.count(s); } +// bool has_driver_cell(const RTLIL::SigBit &s) { return net.sigbit_driver_map.count(s); } - NetlistConeInputsIter(const Netlist &net, const RTLIL::SigBit *p_sig = NULL) : net(net), p_sig(p_sig), sig_iter(net, p_sig) - { - if ((p_sig != NULL) && (has_driver_cell(*sig_iter))) { - ++(*this); - } - } +// 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.p_sig == NULL) { - return *this; - } - } while (has_driver_cell(*sig_iter)); +// 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; - } -}; +// return *this; +// } +// }; -struct NetlistConeInputsIterable { - const Netlist &net; - const RTLIL::SigBit *p_sig; +// struct NetlistConeInputsIterable { +// const Netlist &net; +// RTLIL::SigBit sig; - NetlistConeInputsIterable(const Netlist &net, const RTLIL::SigBit *p_sig) : net(net), p_sig(p_sig) {} +// NetlistConeInputsIterable(const Netlist &net, RTLIL::SigBit sig) : net(net), sig(sig) {} - NetlistConeInputsIter begin() { return NetlistConeInputsIter(net, p_sig); } - NetlistConeInputsIter end() { return NetlistConeInputsIter(net); } -}; +// NetlistConeInputsIter begin() { return NetlistConeInputsIter(net, sig); } +// NetlistConeInputsIter end() { return NetlistConeInputsIter(net); } +// }; } // namespace detail -detail::NetlistConeWireIterable cone(const Netlist &net, const RTLIL::SigBit &sig) { return detail::NetlistConeWireIterable(net, &sig); } +detail::NetlistConeWireIterable cone(const Netlist &net, RTLIL::SigBit sig) { return detail::NetlistConeWireIterable(net, net.sigmap(sig)); } -// detail::NetlistConeInputsIterable cone_inputs(const RTLIL::SigBit &sig) { return NetlistConeInputsIterable(this, &sig); } -detail::NetlistConeCellIterable cell_cone(const Netlist &net, const RTLIL::SigBit &sig) { return detail::NetlistConeCellIterable(net, &sig); } +// detail::NetlistConeInputsIterable cone_inputs(RTLIL::SigBit sig) { return NetlistConeInputsIterable(this, &sig); } +detail::NetlistConeCellIterable cell_cone(const Netlist &net, RTLIL::SigBit sig) { return detail::NetlistConeCellIterable(net, net.sigmap(sig)); } YOSYS_NAMESPACE_END From 8665f48879526f8f3ed79629f28a8686ed78a8ad Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Thu, 13 Jun 2019 19:35:37 +0200 Subject: [PATCH 07/13] Implement disconnection of constant register bits --- kernel/algo.h | 115 +++++++++++++++++++++++++++++----------- passes/opt/opt_rmdff.cc | 36 ++++++++----- 2 files changed, 108 insertions(+), 43 deletions(-) diff --git a/kernel/algo.h b/kernel/algo.h index 05467c60a..9626c780e 100644 --- a/kernel/algo.h +++ b/kernel/algo.h @@ -40,16 +40,39 @@ CellTypes comb_cells_filt() 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) + 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 { - CellTypes ct(module->design); - setup_netlist(module, ct); + sig = sigmap(sig); + if (!sigbit_driver_map.count(sig)) { + return NULL; + } + + return sigbit_driver_map.at(sig); } - Netlist(RTLIL::Module *module, const CellTypes &ct) : module(module), sigmap(module) { setup_netlist(module, ct); } + RTLIL::SigBit& driver_port(RTLIL::SigBit sig) + { + RTLIL::Cell *cell = driver_cell(sig); + + 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]; + } + } + } + } + } void setup_netlist(RTLIL::Module *module, const CellTypes &ct) { @@ -80,13 +103,17 @@ struct NetlistConeWireIter : public std::iterator> dfs_path_stack; std::set cells_visited; - NetlistConeWireIter(const Netlist &net) : net(net), sentinel(true) {} + NetlistConeWireIter(const Netlist &net) : net(net), sentinel(true), cell_filter(NULL) {} - NetlistConeWireIter(const Netlist &net, RTLIL::SigBit sig) : net(net), sig(sig), sentinel(false) {} + 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 @@ -98,7 +125,8 @@ struct NetlistConeWireIter : public std::iteratorcell_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; } }; @@ -150,10 +185,13 @@ struct NetlistConeWireIter : public std::iteratorcell_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) : net(net), sig(sig) {} + 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); } + NetlistConeCellIter begin() { return NetlistConeCellIter(net, sig, cell_filter); } NetlistConeCellIter end() { return NetlistConeCellIter(net); } }; @@ -248,10 +295,16 @@ struct NetlistConeCellIterable { // }; } // namespace detail -detail::NetlistConeWireIterable cone(const Netlist &net, RTLIL::SigBit sig) { return detail::NetlistConeWireIterable(net, net.sigmap(sig)); } +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) { return detail::NetlistConeCellIterable(net, net.sigmap(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 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++; } From 291b36afeb1075b7c6329d1e57594ed3e6b71581 Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Fri, 14 Jun 2019 11:35:45 +0200 Subject: [PATCH 08/13] Some cleanup, revert sat.cc --- passes/opt/opt_rmdff.cc | 17 ++++++++++------- passes/sat/sat.cc | 7 +------ 2 files changed, 11 insertions(+), 13 deletions(-) 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) From 53695e6729e8ae603be7e7cd9bc8b29758d61a11 Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Fri, 14 Jun 2019 11:39:24 +0200 Subject: [PATCH 09/13] Prepare for situation when port of the signal cannot be found --- kernel/algo.h | 8 +++++++- passes/opt/opt_rmdff.cc | 2 +- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/kernel/algo.h b/kernel/algo.h index 9626c780e..f029ad6ab 100644 --- a/kernel/algo.h +++ b/kernel/algo.h @@ -58,10 +58,14 @@ struct Netlist { return sigbit_driver_map.at(sig); } - RTLIL::SigBit& driver_port(RTLIL::SigBit 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); @@ -72,6 +76,8 @@ struct Netlist { } } } + + return RTLIL::SigSpec(); } void setup_netlist(RTLIL::Module *module, const CellTypes &ct) 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_) From 8451cbea896d2b441b5c78eb2813790616d10b84 Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Fri, 14 Jun 2019 12:14:02 +0200 Subject: [PATCH 10/13] Move netlist helper module to passes/opt for the time being --- kernel/algo.h => passes/opt/netlist.h | 0 passes/opt/opt_rmdff.cc | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) rename kernel/algo.h => passes/opt/netlist.h (100%) diff --git a/kernel/algo.h b/passes/opt/netlist.h similarity index 100% rename from kernel/algo.h rename to passes/opt/netlist.h 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 From 2454ad99bf49afe752d6fd1c1567f59ee9e26736 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 20 Jun 2019 13:44:21 +0200 Subject: [PATCH 11/13] Refactor "opt_rmdff -sat" Signed-off-by: Clifford Wolf --- passes/opt/netlist.h | 317 ---------------------------------------- passes/opt/opt_rmdff.cc | 86 +++++------ tests/opt/opt_ff_sat.v | 25 ++-- tests/opt/opt_ff_sat.ys | 1 + 4 files changed, 57 insertions(+), 372 deletions(-) delete mode 100644 passes/opt/netlist.h 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::State sigbit_init_val = val_init[position]; + if (sigbit_init_val != State::S0 && sigbit_init_val != State::S1) + continue; - RTLIL::Const sigbit_init_val = val_init.extract(position); 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) { + 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)); - 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; - - 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) diff --git a/tests/opt/opt_ff_sat.v b/tests/opt/opt_ff_sat.v index fc1e61980..5a0a6fe37 100644 --- a/tests/opt/opt_ff_sat.v +++ b/tests/opt/opt_ff_sat.v @@ -1,15 +1,12 @@ -module top( - input clk, - input a, - output b - ); - reg b_reg; - initial begin - b_reg <= 0; - end - - assign b = b_reg; - always @(posedge clk) begin - b_reg <= a && b_reg; - end +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 index 13e4ad29b..4e7cc6ca4 100644 --- a/tests/opt/opt_ff_sat.ys +++ b/tests/opt/opt_ff_sat.ys @@ -2,3 +2,4 @@ read_verilog opt_ff_sat.v prep -flatten opt_rmdff -sat synth +select -assert-count 5 t:$_DFF_P_ From 35fa7b30574244e4f99373f2a790f004b4a1dbbb Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Thu, 27 Jun 2019 22:02:12 +0200 Subject: [PATCH 12/13] 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(+) 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; } From 3225bfb98403271bbe8a56418ccd027b42eabda1 Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Thu, 27 Jun 2019 22:06:23 +0200 Subject: [PATCH 13/13] 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(-) 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 {