From 9a468f81c412f8b63d25e739f28932815c6882fb Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Tue, 28 May 2019 08:48:21 +0200 Subject: [PATCH 01/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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