From 9a468f81c412f8b63d25e739f28932815c6882fb Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Tue, 28 May 2019 08:48:21 +0200 Subject: [PATCH 01/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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/32] 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 71b046d63996a1813375e56f44543e58eb7e1b5e Mon Sep 17 00:00:00 2001 From: David Shah Date: Wed, 26 Jun 2019 18:17:52 +0100 Subject: [PATCH 12/32] tests: Check that Icarus can parse arch sim models Signed-off-by: David Shah --- Makefile | 1 + tests/arch/run-test.sh | 8 ++++++++ 2 files changed, 9 insertions(+) create mode 100755 tests/arch/run-test.sh diff --git a/Makefile b/Makefile index 76dac48a5..67bcb3d15 100644 --- a/Makefile +++ b/Makefile @@ -681,6 +681,7 @@ test: $(TARGETS) $(EXTRA_TARGETS) +cd tests/svinterfaces && bash run-test.sh $(SEEDOPT) +cd tests/opt && bash run-test.sh +cd tests/aiger && bash run-test.sh + +cd tests/arch && bash run-test.sh @echo "" @echo " Passed \"make test\"." @echo "" diff --git a/tests/arch/run-test.sh b/tests/arch/run-test.sh new file mode 100755 index 000000000..fc4175be8 --- /dev/null +++ b/tests/arch/run-test.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +set -e + +echo "Running syntax check on arch sim models" +for arch in ../../techlibs/*; do + find $arch -name cells_sim.v -print0 | xargs -0 -n1 -r iverilog -t null -I$arch +done From ab7c4319058bbae8758cda9f246c92c324dfafbf Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 11:13:49 -0700 Subject: [PATCH 13/32] Add simcells.v, simlib.v, and some output --- tests/arch/run-test.sh | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/tests/arch/run-test.sh b/tests/arch/run-test.sh index fc4175be8..5292d1615 100755 --- a/tests/arch/run-test.sh +++ b/tests/arch/run-test.sh @@ -4,5 +4,15 @@ set -e echo "Running syntax check on arch sim models" for arch in ../../techlibs/*; do - find $arch -name cells_sim.v -print0 | xargs -0 -n1 -r iverilog -t null -I$arch + find $arch -name cells_sim.v | while read path; do + echo -n "Test $path ->" + iverilog -t null -I$arch $path + echo " ok" + done +done + +for path in "../../techlibs/common/simcells.v" "../../techlibs/common/simlib.v"; do + echo -n "Test $path ->" + iverilog -t null $path + echo " ok" done From 35fa7b30574244e4f99373f2a790f004b4a1dbbb Mon Sep 17 00:00:00 2001 From: Bogdan Vukobratovic Date: Thu, 27 Jun 2019 22:02:12 +0200 Subject: [PATCH 14/32] 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 15/32] 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 { From fb30fcb7c582406f627ebb15833791411091f738 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 15:03:21 -0700 Subject: [PATCH 16/32] Undo iterator based Module::remove() for cells, as containers will not invalidate --- kernel/rtlil.cc | 12 ++---------- kernel/rtlil.h | 1 - 2 files changed, 2 insertions(+), 11 deletions(-) diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 502b45cfd..a09f4a0d1 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1592,21 +1592,13 @@ void RTLIL::Module::remove(const pool &wires) void RTLIL::Module::remove(RTLIL::Cell *cell) { - auto it = cells_.find(cell->name); - log_assert(it != cells_.end()); - remove(it); -} - -dict::iterator RTLIL::Module::remove(dict::iterator it) -{ - RTLIL::Cell *cell = it->second; while (!cell->connections_.empty()) cell->unsetPort(cell->connections_.begin()->first); + log_assert(cells_.count(cell->name) != 0); log_assert(refcount_cells_ == 0); - it = cells_.erase(it); + cells_.erase(cell->name); delete cell; - return it; } void RTLIL::Module::rename(RTLIL::Wire *wire, RTLIL::IdString new_name) diff --git a/kernel/rtlil.h b/kernel/rtlil.h index 4a0f8b4f8..f4fcf5dcf 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -1040,7 +1040,6 @@ public: // Removing wires is expensive. If you have to remove wires, remove them all at once. void remove(const pool &wires); void remove(RTLIL::Cell *cell); - dict::iterator remove(dict::iterator it); void rename(RTLIL::Wire *wire, RTLIL::IdString new_name); void rename(RTLIL::Cell *cell, RTLIL::IdString new_name); From 6bf73e3546450671660e793991c982eeadf1872e Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 15:15:56 -0700 Subject: [PATCH 17/32] Cleanup abc9.cc --- passes/techmap/abc9.cc | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index b4f15d6a1..f25b02a88 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -80,7 +80,7 @@ void handle_loops(RTLIL::Design *design) { Pass::call(design, "scc -set_attr abc_scc_id {}"); - dict> module_break; + dict> abc_scc_break; // For every unique SCC found, (arbitrarily) find the first // cell in the component, and select (and mark) all its output @@ -116,12 +116,11 @@ void handle_loops(RTLIL::Design *design) cell->attributes.erase(it); } - auto jt = module_break.find(cell->type); - if (jt == module_break.end()) { + auto jt = abc_scc_break.find(cell->type); + if (jt == abc_scc_break.end()) { std::vector ports; - if (!yosys_celltypes.cell_known(cell->type)) { - RTLIL::Module* box_module = design->module(cell->type); - log_assert(box_module); + RTLIL::Module* box_module = design->module(cell->type); + if (box_module) { auto ports_csv = box_module->attributes.at("\\abc_scc_break", RTLIL::Const::from_string("")).decode_string(); for (const auto &port_name : split_tokens(ports_csv, ",")) { auto port_id = RTLIL::escape_id(port_name); @@ -131,7 +130,7 @@ void handle_loops(RTLIL::Design *design) ports.push_back(port_id); } } - jt = module_break.insert(std::make_pair(cell->type, std::move(ports))).first; + jt = abc_scc_break.insert(std::make_pair(cell->type, std::move(ports))).first; } for (auto port_name : jt->second) { @@ -554,17 +553,20 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri signal = std::move(bits); } + dict abc_box; vector boxes; - for (auto it = module->cells_.begin(); it != module->cells_.end(); ) { - RTLIL::Cell* cell = it->second; - if (cell->type.in("$_AND_", "$_NOT_", "$__ABC_FF_")) { - it = module->remove(it); + for (auto cell : module->cells()) { + if (cell->type.in("$_AND_", "$_NOT_")) { + module->remove(cell); continue; } - RTLIL::Module* box_module = design->module(cell->type); - if (box_module && box_module->attributes.count("\\abc_box_id")) - boxes.emplace_back(it->second); - ++it; + auto it = abc_box.find(cell->type); + if (it == abc_box.end()) { + RTLIL::Module* box_module = design->module(cell->type); + it = abc_box.insert(std::make_pair(cell->type, box_module && box_module->attributes.count("\\abc_box_id"))).first; + } + if (it->second) + boxes.emplace_back(cell); } std::map cell_stats; From 137c91d9a98e05199b7acfe1d63139b79d278277 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 15:17:39 -0700 Subject: [PATCH 18/32] Remove &retime when abc9 -fast --- passes/techmap/abc9.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index f25b02a88..e2a82f0c8 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -33,7 +33,7 @@ #endif -#define ABC_FAST_COMMAND_LUT "&st; &retime; &if {W}" +#define ABC_FAST_COMMAND_LUT "&st; &if {W} {D}" #include "kernel/register.h" #include "kernel/sigtools.h" From 312c03e4ca71f1560a9f47dcd2e9d3de1202179e Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 15:28:55 -0700 Subject: [PATCH 19/32] Remove redundant doc --- techlibs/xilinx/synth_xilinx.cc | 3 --- 1 file changed, 3 deletions(-) diff --git a/techlibs/xilinx/synth_xilinx.cc b/techlibs/xilinx/synth_xilinx.cc index 7dbd98055..c24f66e52 100644 --- a/techlibs/xilinx/synth_xilinx.cc +++ b/techlibs/xilinx/synth_xilinx.cc @@ -62,9 +62,6 @@ struct SynthXilinxPass : public ScriptPass log(" generate an output netlist (and BLIF file) suitable for VPR\n"); log(" (this feature is experimental and incomplete)\n"); log("\n"); - log(" -nocarry\n"); - log(" disable inference of carry chains\n"); - log("\n"); log(" -nobram\n"); log(" disable inference of block rams\n"); log("\n"); From a625854ac5e2ff3d6bf11e97b7ac676b362e7461 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 15:29:20 -0700 Subject: [PATCH 20/32] Do not use Module::remove() iterator version --- passes/techmap/abc9.cc | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index e2a82f0c8..3721b82b7 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -555,17 +555,18 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri dict abc_box; vector boxes; - for (auto cell : module->cells()) { + for (const auto &it : module->cells_) { + auto cell = it.second; if (cell->type.in("$_AND_", "$_NOT_")) { module->remove(cell); continue; } - auto it = abc_box.find(cell->type); - if (it == abc_box.end()) { + auto jt = abc_box.find(cell->type); + if (jt == abc_box.end()) { RTLIL::Module* box_module = design->module(cell->type); - it = abc_box.insert(std::make_pair(cell->type, box_module && box_module->attributes.count("\\abc_box_id"))).first; + jt = abc_box.insert(std::make_pair(cell->type, box_module && box_module->attributes.count("\\abc_box_id"))).first; } - if (it->second) + if (jt->second) boxes.emplace_back(cell); } From 9398921af1d21b47aa291d240a1f274418adcaf2 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 16:07:14 -0700 Subject: [PATCH 21/32] Refactor for one "abc_carry" attribute on module --- backends/aiger/xaiger.cc | 80 +++++++++++++++++------------------ frontends/aiger/aigerparse.cc | 70 ++++++++++++++++-------------- techlibs/ecp5/cells_sim.v | 8 ++-- techlibs/ice40/cells_sim.v | 4 +- techlibs/xilinx/cells_sim.v | 4 +- 5 files changed, 84 insertions(+), 82 deletions(-) diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 92df899c2..ae690ec49 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -284,8 +284,6 @@ struct XAigerWriter for (auto user_cell : it.second) toposort.edge(driver_cell, user_cell); - pool abc_carry_modules; - #if 0 toposort.analyze_loops = true; #endif @@ -303,54 +301,54 @@ struct XAigerWriter #endif log_assert(no_loops); + pool seen_boxes; for (auto cell_name : toposort.sorted) { RTLIL::Cell *cell = module->cell(cell_name); + log_assert(cell); + RTLIL::Module* box_module = module->design->module(cell->type); if (!box_module || !box_module->attributes.count("\\abc_box_id")) continue; - if (box_module->attributes.count("\\abc_carry") && !abc_carry_modules.count(box_module)) { - RTLIL::Wire* carry_in = nullptr, *carry_out = nullptr; - auto &ports = box_module->ports; - for (auto it = ports.begin(); it != ports.end(); ) { - RTLIL::Wire* w = box_module->wire(*it); - log_assert(w); - if (w->port_input && w->attributes.count("\\abc_carry_in")) { - if (carry_in) - log_error("More than one port with attribute 'abc_carry_in' found in module '%s'\n", log_id(box_module)); - carry_in = w; - it = ports.erase(it); - continue; - } - if (w->port_output && w->attributes.count("\\abc_carry_out")) { - if (carry_out) - log_error("More than one port with attribute 'abc_carry_out' found in module '%s'\n", log_id(box_module)); - carry_out = w; - it = ports.erase(it); - continue; - } - ++it; - } + if (seen_boxes.insert(cell->type).second) { + auto it = box_module->attributes.find("\\abc_carry"); + if (it != box_module->attributes.end()) { + RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr; + auto carry_in_out = it->second.decode_string(); + auto pos = carry_in_out.find(','); + if (pos == std::string::npos) + log_error("'abc_carry' attribute on module '%s' does not contain ','.\n", log_id(cell->type)); + auto carry_in_name = RTLIL::escape_id(carry_in_out.substr(0, pos)); + carry_in = box_module->wire(carry_in_name); + if (!carry_in || !carry_in->port_input) + log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an input port.\n", log_id(cell->type), carry_in_name.c_str()); - if (!carry_in) - log_error("Port with attribute 'abc_carry_in' not found in module '%s'\n", log_id(box_module)); - if (!carry_out) - log_error("Port with attribute 'abc_carry_out' not found in module '%s'\n", log_id(box_module)); + auto carry_out_name = RTLIL::escape_id(carry_in_out.substr(pos+1)); + carry_out = box_module->wire(carry_out_name); + if (!carry_out || !carry_out->port_output) + log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an output port.\n", log_id(cell->type), carry_out_name.c_str()); - for (const auto port_name : ports) { - RTLIL::Wire* w = box_module->wire(port_name); - log_assert(w); - if (w->port_id > carry_in->port_id) - --w->port_id; - if (w->port_id > carry_out->port_id) - --w->port_id; - log_assert(w->port_input || w->port_output); - log_assert(ports[w->port_id-1] == w->name); + auto &ports = box_module->ports; + for (auto jt = ports.begin(); jt != ports.end(); ) { + RTLIL::Wire* w = box_module->wire(*jt); + log_assert(w); + if (w == carry_in || w == carry_out) { + jt = ports.erase(jt); + continue; + } + if (w->port_id > carry_in->port_id) + --w->port_id; + if (w->port_id > carry_out->port_id) + --w->port_id; + log_assert(w->port_input || w->port_output); + log_assert(ports[w->port_id-1] == w->name); + ++jt; + } + ports.push_back(carry_in->name); + carry_in->port_id = ports.size(); + ports.push_back(carry_out->name); + carry_out->port_id = ports.size(); } - ports.push_back(carry_in->name); - carry_in->port_id = ports.size(); - ports.push_back(carry_out->name); - carry_out->port_id = ports.size(); } // Fully pad all unused input connections of this box cell with S0 diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 43337f4c2..7008d0542 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -732,44 +732,50 @@ void AigerReader::parse_aiger_binary() void AigerReader::post_process() { - pool abc_carry_modules; + pool seen_boxes; unsigned ci_count = 0, co_count = 0; for (auto cell : boxes) { RTLIL::Module* box_module = design->module(cell->type); log_assert(box_module); - if (box_module->attributes.count("\\abc_carry") && !abc_carry_modules.count(box_module)) { - RTLIL::Wire* carry_in = nullptr, *carry_out = nullptr; - RTLIL::Wire* last_in = nullptr, *last_out = nullptr; - for (const auto &port_name : box_module->ports) { - RTLIL::Wire* w = box_module->wire(port_name); - log_assert(w); - if (w->port_input) { - if (w->attributes.count("\\abc_carry_in")) { - log_assert(!carry_in); - carry_in = w; - } - log_assert(!last_in || last_in->port_id < w->port_id); - last_in = w; - } - if (w->port_output) { - if (w->attributes.count("\\abc_carry_out")) { - log_assert(!carry_out); - carry_out = w; - } - log_assert(!last_out || last_out->port_id < w->port_id); - last_out = w; - } - } + if (seen_boxes.insert(cell->type).second) { + auto it = box_module->attributes.find("\\abc_carry"); + if (it != box_module->attributes.end()) { + RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr; + auto carry_in_out = it->second.decode_string(); + auto pos = carry_in_out.find(','); + if (pos == std::string::npos) + log_error("'abc_carry' attribute on module '%s' does not contain ','.\n", log_id(cell->type)); + auto carry_in_name = RTLIL::escape_id(carry_in_out.substr(0, pos)); + carry_in = box_module->wire(carry_in_name); + if (!carry_in || !carry_in->port_input) + log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an input port.\n", log_id(cell->type), carry_in_name.c_str()); - if (carry_in != last_in) { - std::swap(box_module->ports[carry_in->port_id], box_module->ports[last_in->port_id]); - std::swap(carry_in->port_id, last_in->port_id); - } - if (carry_out != last_out) { - log_assert(last_out); - std::swap(box_module->ports[carry_out->port_id], box_module->ports[last_out->port_id]); - std::swap(carry_out->port_id, last_out->port_id); + auto carry_out_name = RTLIL::escape_id(carry_in_out.substr(pos+1)); + carry_out = box_module->wire(carry_out_name); + if (!carry_out || !carry_out->port_output) + log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an output port.\n", log_id(cell->type), carry_out_name.c_str()); + + auto &ports = box_module->ports; + for (auto jt = ports.begin(); jt != ports.end(); ) { + RTLIL::Wire* w = box_module->wire(*jt); + log_assert(w); + if (w == carry_in || w == carry_out) { + jt = ports.erase(jt); + continue; + } + if (w->port_id > carry_in->port_id) + --w->port_id; + if (w->port_id > carry_out->port_id) + --w->port_id; + log_assert(w->port_input || w->port_output); + log_assert(ports[w->port_id-1] == w->name); + ++jt; + } + ports.push_back(carry_in->name); + carry_in->port_id = ports.size(); + ports.push_back(carry_out->name); + carry_out->port_id = ports.size(); } } diff --git a/techlibs/ecp5/cells_sim.v b/techlibs/ecp5/cells_sim.v index 08ae0a112..98f915777 100644 --- a/techlibs/ecp5/cells_sim.v +++ b/techlibs/ecp5/cells_sim.v @@ -15,11 +15,9 @@ module L6MUX21 (input D0, D1, SD, output Z); endmodule // --------------------------------------- -(* abc_box_id=1, abc_carry, lib_whitebox *) -module CCU2C((* abc_carry_in *) input CIN, - input A0, B0, C0, D0, A1, B1, C1, D1, - output S0, S1, - (* abc_carry_out *) output COUT); +(* abc_box_id=1, abc_carry="CIN,COUT", lib_whitebox *) +module CCU2C(input CIN, A0, B0, C0, D0, A1, B1, C1, D1, + output S0, S1, COUT); parameter [15:0] INIT0 = 16'h0000; parameter [15:0] INIT1 = 16'h0000; diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v index 317ae2c1f..c7e4101e1 100644 --- a/techlibs/ice40/cells_sim.v +++ b/techlibs/ice40/cells_sim.v @@ -136,8 +136,8 @@ module SB_LUT4 (output O, input I0, I1, I2, I3); assign O = I0 ? s1[1] : s1[0]; endmodule -(* abc_box_id = 1, abc_carry, lib_whitebox *) -module SB_CARRY ((* abc_carry_out *) output CO, input I0, I1, (* abc_carry_in *) input CI); +(* abc_box_id = 1, abc_carry="CI,CO", lib_whitebox *) +module SB_CARRY (output CO, input I0, I1, CI); assign CO = (I0 && I1) || ((I0 || I1) && CI); endmodule diff --git a/techlibs/xilinx/cells_sim.v b/techlibs/xilinx/cells_sim.v index 5fd9973f4..5a148be01 100644 --- a/techlibs/xilinx/cells_sim.v +++ b/techlibs/xilinx/cells_sim.v @@ -173,8 +173,8 @@ module XORCY(output O, input CI, LI); assign O = CI ^ LI; endmodule -(* abc_box_id = 3, abc_carry, lib_whitebox *) -module CARRY4((* abc_carry_out *) output [3:0] CO, output [3:0] O, (* abc_carry_in *) input CI, input CYINIT, input [3:0] DI, S); +(* abc_box_id = 3, abc_carry="CI,CO", lib_whitebox *) +module CARRY4(output [3:0] CO, O, input CI, CYINIT, input [3:0] DI, S); assign O = S ^ {CO[2:0], CI | CYINIT}; assign CO[0] = S[0] ? CI | CYINIT : DI[0]; assign CO[1] = S[1] ? CO[0] : DI[1]; From 4daa74679779a45542b36c1f3630bd1fbae9ec7b Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 16:11:39 -0700 Subject: [PATCH 22/32] Remove noise from ice40/cells_sim.v --- techlibs/ice40/cells_sim.v | 5 ----- 1 file changed, 5 deletions(-) diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v index c7e4101e1..b746ba4e5 100644 --- a/techlibs/ice40/cells_sim.v +++ b/techlibs/ice40/cells_sim.v @@ -144,12 +144,8 @@ endmodule // Positive Edge SiliconBlue FF Cells module SB_DFF (output `SB_DFF_REG, input C, D); -`ifndef _ABC always @(posedge C) Q <= D; -`else - always @* Q <= D; -`endif endmodule module SB_DFFE (output `SB_DFF_REG, input C, E, D); @@ -896,7 +892,6 @@ module SB_WARMBOOT ( ); endmodule -(* nomem2reg *) module SB_SPRAM256KA ( input [13:0] ADDRESS, input [15:0] DATAIN, From af8a5ae5fe35d65742eb17db8cd2bacda93e916e Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 16:12:20 -0700 Subject: [PATCH 23/32] Extraneous newline --- techlibs/ice40/synth_ice40.cc | 1 - 1 file changed, 1 deletion(-) diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc index a782f00b9..caef420d4 100644 --- a/techlibs/ice40/synth_ice40.cc +++ b/techlibs/ice40/synth_ice40.cc @@ -105,7 +105,6 @@ struct SynthIce40Pass : public ScriptPass log("\n"); } - string top_opt, blif_file, edif_file, json_file, abc, device_opt; bool nocarry, nodffe, nobram, dsp, flatten, retime, relut, noabc, abc2, vpr; int min_ce_use; From 00f63d82ce4fbaa0f63ff2c68d4941f7eb16dfc4 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 27 Jun 2019 16:13:22 -0700 Subject: [PATCH 24/32] Reduce diff with upstream --- techlibs/xilinx/cells_map.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/techlibs/xilinx/cells_map.v b/techlibs/xilinx/cells_map.v index b5114758c..9a316fc96 100644 --- a/techlibs/xilinx/cells_map.v +++ b/techlibs/xilinx/cells_map.v @@ -20,16 +20,14 @@ // Convert negative-polarity reset to positive-polarity (* techmap_celltype = "$_DFF_NN0_" *) -module _90_dff_nn0_to_np0(input D, C, R, output Q); \$_DFF_NP0_ _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(~R)); endmodule +module _90_dff_nn0_to_np0 (input D, C, R, output Q); \$_DFF_NP0_ _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(~R)); endmodule (* techmap_celltype = "$_DFF_PN0_" *) -module _90_dff_pn0_to_pp0(input D, C, R, output Q); \$_DFF_PP0_ _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(~R)); endmodule - +module _90_dff_pn0_to_pp0 (input D, C, R, output Q); \$_DFF_PP0_ _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(~R)); endmodule (* techmap_celltype = "$_DFF_NN1_" *) module _90_dff_nn1_to_np1 (input D, C, R, output Q); \$_DFF_NP1 _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(~R)); endmodule (* techmap_celltype = "$_DFF_PN1_" *) module _90_dff_pn1_to_pp1 (input D, C, R, output Q); \$_DFF_PP1 _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(~R)); endmodule - module \$__SHREG_ (input C, input D, input E, output Q); parameter DEPTH = 0; parameter [DEPTH-1:0] INIT = 0; From 6f1c1379891651b0d110e35fb2c73fd78fde3f69 Mon Sep 17 00:00:00 2001 From: "Gabriel L. Somlo" Date: Thu, 27 Jun 2019 22:54:09 -0400 Subject: [PATCH 25/32] tests: use optional ABCEXTERNAL when specified Commits 65924fd1, abc40924, and ebe29b66 hard-code the invocation of yosys-abc, which fails if ABCEXTERNAL was specified during the build. Allow tests to utilize an optional, externally specified abc binary. Signed-off-by: Gabriel Somlo --- Makefile | 10 ++++++++-- tests/aiger/run-test.sh | 14 ++++++++++++-- tests/memories/run-test.sh | 6 ++++-- tests/tools/autotest.sh | 7 +++++-- 4 files changed, 29 insertions(+), 8 deletions(-) diff --git a/Makefile b/Makefile index 67bcb3d15..5ec3e0312 100644 --- a/Makefile +++ b/Makefile @@ -666,6 +666,12 @@ else SEEDOPT="" endif +ifneq ($(ABCEXTERNAL),) +ABCOPT="-A $(ABCEXTERNAL)" +else +ABCOPT="" +endif + test: $(TARGETS) $(EXTRA_TARGETS) +cd tests/simple && bash run-test.sh $(SEEDOPT) +cd tests/hana && bash run-test.sh $(SEEDOPT) @@ -674,13 +680,13 @@ test: $(TARGETS) $(EXTRA_TARGETS) +cd tests/share && bash run-test.sh $(SEEDOPT) +cd tests/fsm && bash run-test.sh $(SEEDOPT) +cd tests/techmap && bash run-test.sh - +cd tests/memories && bash run-test.sh $(SEEDOPT) + +cd tests/memories && bash run-test.sh $(ABCOPT) $(SEEDOPT) +cd tests/bram && bash run-test.sh $(SEEDOPT) +cd tests/various && bash run-test.sh +cd tests/sat && bash run-test.sh +cd tests/svinterfaces && bash run-test.sh $(SEEDOPT) +cd tests/opt && bash run-test.sh - +cd tests/aiger && bash run-test.sh + +cd tests/aiger && bash run-test.sh $(ABCOPT) +cd tests/arch && bash run-test.sh @echo "" @echo " Passed \"make test\"." diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh index 5246c1b48..deaf48a3d 100755 --- a/tests/aiger/run-test.sh +++ b/tests/aiger/run-test.sh @@ -2,6 +2,16 @@ set -e +OPTIND=1 +abcprog="../../yosys-abc" # default to built-in version of abc +while getopts "A:" opt +do + case "$opt" in + A) abcprog="$OPTARG" ;; + esac +done +shift "$((OPTIND-1))" + # NB: *.aag and *.aig must contain a symbol table naming the primary # inputs and outputs, otherwise ABC and Yosys will name them # arbitrarily (and inconsistently with each other). @@ -11,7 +21,7 @@ for aag in *.aag; do # (which would have been created by the reference aig2aig utility, # available from http://fmv.jku.at/aiger/) echo "Checking $aag." - ../../yosys-abc -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v" + $abcprog -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v" ../../yosys -qp " read_verilog ${aag%.*}_ref.v prep @@ -28,7 +38,7 @@ done for aig in *.aig; do echo "Checking $aig." - ../../yosys-abc -q "read -c $aig; write ${aig%.*}_ref.v" + $abcprog -q "read -c $aig; write ${aig%.*}_ref.v" ../../yosys -qp " read_verilog ${aig%.*}_ref.v prep diff --git a/tests/memories/run-test.sh b/tests/memories/run-test.sh index d0537bb98..76acaa9cd 100755 --- a/tests/memories/run-test.sh +++ b/tests/memories/run-test.sh @@ -4,15 +4,17 @@ set -e OPTIND=1 seed="" # default to no seed specified -while getopts "S:" opt +abcopt="" +while getopts "A:S:" opt do case "$opt" in + A) abcopt="-A $OPTARG" ;; S) seed="-S $OPTARG" ;; esac done shift "$((OPTIND-1))" -bash ../tools/autotest.sh $seed -G *.v +bash ../tools/autotest.sh $abcopt $seed -G *.v for f in `egrep -l 'expect-(wr-ports|rd-ports|rd-clk)' *.v`; do echo -n "Testing expectations for $f .." diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh index 96d9cdda9..7b64b357f 100755 --- a/tests/tools/autotest.sh +++ b/tests/tools/autotest.sh @@ -23,12 +23,13 @@ warn_iverilog_git=false # The tests are skipped if firrtl2verilog is the empty string (the default). firrtl2verilog="" xfirrtl="../xfirrtl" +abcprog="$toolsdir/../../yosys-abc" if [ ! -f $toolsdir/cmp_tbdata -o $toolsdir/cmp_tbdata.c -nt $toolsdir/cmp_tbdata ]; then ( set -ex; ${CC:-gcc} -Wall -o $toolsdir/cmp_tbdata $toolsdir/cmp_tbdata.c; ) || exit 1 fi -while getopts xmGl:wkjvref:s:p:n:S:I:-: opt; do +while getopts xmGl:wkjvref:s:p:n:S:I:A:-: opt; do case "$opt" in x) use_xsim=true ;; @@ -65,6 +66,8 @@ while getopts xmGl:wkjvref:s:p:n:S:I:-: opt; do include_opts="$include_opts -I $OPTARG" xinclude_opts="$xinclude_opts -i $OPTARG" minclude_opts="$minclude_opts +incdir+$OPTARG" ;; + A) + abcprog="$OPTARG" ;; -) case "${OPTARG}" in xfirrtl) @@ -147,7 +150,7 @@ do if [[ "$ext" == "v" ]]; then egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext} elif [[ "$ext" == "aig" ]] || [[ "$ext" == "aag" ]]; then - "$toolsdir"/../../yosys-abc -c "read_aiger ../${fn}; write ${bn}_ref.${refext}" + $abcprog -c "read_aiger ../${fn}; write ${bn}_ref.${refext}" else refext=$ext cp ../${fn} ${bn}_ref.${refext} From b9ddee0c87ef3f089995d734ad7f5ea1c65eedce Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 28 Jun 2019 09:45:40 -0700 Subject: [PATCH 26/32] Fix DO4 typo --- techlibs/ecp5/abc_5g.box | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/techlibs/ecp5/abc_5g.box b/techlibs/ecp5/abc_5g.box index 5309aca87..c757d137d 100644 --- a/techlibs/ecp5/abc_5g.box +++ b/techlibs/ecp5/abc_5g.box @@ -16,7 +16,7 @@ CCU2C 1 1 9 3 516 516 516 516 412 412 278 278 43 # Box 2 : TRELLIS_DPR16X4 (16x4 dist ram) -# Outputs: DO0, DO1, DO2, DO3, DO4 +# Outputs: DO0, DO1, DO2, DO3 # name ID w/b ins outs TRELLIS_DPR16X4 2 0 14 4 From 0318860b93f7fa4eee148597811c77d67171e5d3 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 28 Jun 2019 09:45:48 -0700 Subject: [PATCH 27/32] Add write address to abc_scc_break of ECP5 dist RAM --- techlibs/ecp5/cells_sim.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/techlibs/ecp5/cells_sim.v b/techlibs/ecp5/cells_sim.v index 98f915777..acfb6960e 100644 --- a/techlibs/ecp5/cells_sim.v +++ b/techlibs/ecp5/cells_sim.v @@ -104,7 +104,7 @@ module PFUMX (input ALUT, BLUT, C0, output Z); endmodule // --------------------------------------- -(* abc_box_id=2, abc_scc_break="DI,WRE" *) +(* abc_box_id=2, abc_scc_break="DI,WAD,WRE" *) module TRELLIS_DPR16X4 ( input [3:0] DI, input [3:0] WAD, From 3f87575cb6cdace3de8dbe1b494e4d29a478878e Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 28 Jun 2019 09:46:36 -0700 Subject: [PATCH 28/32] Disable boxing of ECP5 dist RAM due to regression --- techlibs/ecp5/cells_sim.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/techlibs/ecp5/cells_sim.v b/techlibs/ecp5/cells_sim.v index acfb6960e..ca88d0a5b 100644 --- a/techlibs/ecp5/cells_sim.v +++ b/techlibs/ecp5/cells_sim.v @@ -104,7 +104,7 @@ module PFUMX (input ALUT, BLUT, C0, output Z); endmodule // --------------------------------------- -(* abc_box_id=2, abc_scc_break="DI,WAD,WRE" *) +//(* abc_box_id=2, abc_scc_break="DI,WAD,WRE" *) module TRELLIS_DPR16X4 ( input [3:0] DI, input [3:0] WAD, From 03705f69f4e7fbd19181297cd4de68472a5f4ba3 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 28 Jun 2019 09:49:01 -0700 Subject: [PATCH 29/32] Update synth_ice40 -device doc to be relevant for -abc9 only --- techlibs/ice40/synth_ice40.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc index caef420d4..9dd5d81f7 100644 --- a/techlibs/ice40/synth_ice40.cc +++ b/techlibs/ice40/synth_ice40.cc @@ -38,8 +38,8 @@ struct SynthIce40Pass : public ScriptPass log("This command runs synthesis for iCE40 FPGAs.\n"); log("\n"); log(" -device < hx | lp | u >\n"); - log(" optimise the synthesis netlist for the specified device.\n"); - log(" HX is the default target if no device argument specified.\n"); + log(" relevant only for '-abc9' flow, optimise timing for the specified device.\n"); + log(" default: hx\n"); log("\n"); log(" -top \n"); log(" use the specified module as top module\n"); From 36e2eb06bb63714d852b758062471222022930c3 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 28 Jun 2019 09:51:43 -0700 Subject: [PATCH 30/32] Fix more potential for undefined behaviour due to container invalidation --- backends/aiger/xaiger.cc | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index ae690ec49..d373ca77e 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -436,14 +436,18 @@ struct XAigerWriter new_wire = module->addWire(wire_name, GetSize(wire)); SigBit new_bit(new_wire, bit.offset); module->connect(new_bit, bit); - if (not_map.count(bit)) - not_map[new_bit] = not_map.at(bit); - else if (and_map.count(bit)) { - //and_map[new_bit] = and_map.at(bit); // Breaks gcc-4.8 - and_map.insert(std::make_pair(new_bit, and_map.at(bit))); + if (not_map.count(bit)) { + auto a = not_map.at(bit); + not_map[new_bit] = a; + } + else if (and_map.count(bit)) { + auto a = and_map.at(bit); + and_map[new_bit] = a; + } + else if (alias_map.count(bit)) { + auto a = alias_map.at(bit); + alias_map[new_bit] = a; } - else if (alias_map.count(bit)) - alias_map[new_bit] = alias_map.at(bit); else alias_map[new_bit] = bit; output_bits.erase(bit); From 524af2131741ae2c74a810cab3b925d5ce950e6e Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 28 Jun 2019 09:55:07 -0700 Subject: [PATCH 31/32] Also fix write_aiger for UB --- backends/aiger/aiger.cc | 54 ++++++++++++++++++++--------------------- 1 file changed, 27 insertions(+), 27 deletions(-) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 2815abda8..7c851bb91 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -70,35 +70,35 @@ struct AigerWriter int bit2aig(SigBit bit) { - if (aig_map.count(bit) == 0) - { - aig_map[bit] = -1; - - if (initstate_bits.count(bit)) { - log_assert(initstate_ff > 0); - aig_map[bit] = initstate_ff; - } else - if (not_map.count(bit)) { - int a = bit2aig(not_map.at(bit)) ^ 1; - aig_map[bit] = a; - } else - if (and_map.count(bit)) { - auto args = and_map.at(bit); - int a0 = bit2aig(args.first); - int a1 = bit2aig(args.second); - aig_map[bit] = mkgate(a0, a1); - } else - if (alias_map.count(bit)) { - int a = bit2aig(alias_map.at(bit)); - aig_map[bit] = a; - } - - if (bit == State::Sx || bit == State::Sz) - log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n"); + auto it = aig_map.find(bit); + if (it != aig_map.end()) { + log_assert(it->second >= 0); + return it->second; } - log_assert(aig_map.at(bit) >= 0); - return aig_map.at(bit); + // NB: Cannot use iterator returned from aig_map.insert() + // since this function is called recursively + + int a = -1; + if (not_map.count(bit)) { + a = bit2aig(not_map.at(bit)) ^ 1; + } else + if (and_map.count(bit)) { + auto args = and_map.at(bit); + int a0 = bit2aig(args.first); + int a1 = bit2aig(args.second); + a = mkgate(a0, a1); + } else + if (alias_map.count(bit)) { + a = bit2aig(alias_map.at(bit)); + } + + if (bit == State::Sx || bit == State::Sz) + log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n"); + + log_assert(a >= 0); + aig_map[bit] = a; + return a; } AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode) : module(module), zinit_mode(zinit_mode), sigmap(module) From 38d8806bd74b9bb448c7488ec571e197fe2f96d6 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 28 Jun 2019 09:59:47 -0700 Subject: [PATCH 32/32] Add generic __builtin_bswap32 function --- backends/aiger/xaiger.cc | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index d373ca77e..eb3d47569 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -25,6 +25,21 @@ #elif defined(__APPLE__) #include #define __builtin_bswap32 OSSwapInt32 +#elif !defined(__GNUC__) +#include +inline uint32_t __builtin_bswap32(uint32_t x) +{ + // https://stackoverflow.com/a/27796212 + register uint32_t value = number_to_be_reversed; + uint8_t lolo = (value >> 0) & 0xFF; + uint8_t lohi = (value >> 8) & 0xFF; + uint8_t hilo = (value >> 16) & 0xFF; + uint8_t hihi = (value >> 24) & 0xFF; + return (hihi << 24) + | (hilo << 16) + | (lohi << 8) + | (lolo << 0); +} #endif #include "kernel/yosys.h"