diff --git a/docs/source/getting_started/installation.rst b/docs/source/getting_started/installation.rst index ff6f3ac49..9cad5c830 100644 --- a/docs/source/getting_started/installation.rst +++ b/docs/source/getting_started/installation.rst @@ -332,7 +332,7 @@ directories: commands. Good starting points for reading example source code to learn how to write - passes are :file:`passes/opt/opt_dff.cc` and :file:`passes/opt/opt_merge.cc`. + passes are :file:`passes/opt/dff/opt_dff.cc` and :file:`passes/opt/opt_merge.cc`. Users of the Qt Creator IDE can generate a QT Creator project file using make qtcreator. Users of the Eclipse IDE can use the "Makefile Project with Existing diff --git a/kernel/qcsat.cc b/kernel/qcsat.cc index a5ecd5cb0..0279a07bd 100644 --- a/kernel/qcsat.cc +++ b/kernel/qcsat.cc @@ -101,11 +101,11 @@ int QuickConeSat::cell_complexity(RTLIL::Cell *cell) return 5; } -void SatEffortBudget::charge_import(QuickConeSat &qcsat, int64_t &cells_charged) +int64_t SatEffortBudget::charge_import(QuickConeSat &qcsat, int64_t cells_charged) { if (enabled()) remaining -= (GetSize(qcsat.imported_cells) - cells_charged) * import_cell_cost; - cells_charged = GetSize(qcsat.imported_cells); + return GetSize(qcsat.imported_cells); } SatEffortBudget::Result SatEffortBudget::solve(QuickConeSat &qcsat, int64_t cap, const std::vector &assumptions) diff --git a/kernel/qcsat.h b/kernel/qcsat.h index 09d072f7c..a773219cb 100644 --- a/kernel/qcsat.h +++ b/kernel/qcsat.h @@ -97,8 +97,8 @@ struct SatEffortBudget { bool spent() const { return enabled() && remaining <= 0; } // Charge for the cells imported into qcsat since the previous call (pricing the cells pulled in) - // cells_charged records how many of qcsat's imported cells are already paid for - void charge_import(QuickConeSat &qcsat, int64_t &cells_charged); + // cells_charged is how many of qcsat's imported cells are already paid for, returns the new count + int64_t charge_import(QuickConeSat &qcsat, int64_t cells_charged); Result solve(QuickConeSat &qcsat, int64_t cap, const std::vector &modelExprs, std::vector &modelVals, const std::vector &assumptions); diff --git a/passes/opt/CMakeLists.txt b/passes/opt/CMakeLists.txt index f5818a13d..f21900b2e 100644 --- a/passes/opt/CMakeLists.txt +++ b/passes/opt/CMakeLists.txt @@ -1,4 +1,5 @@ -add_subdirectory(opt_clean) +add_subdirectory(clean) +add_subdirectory(dff) yosys_pass(opt_merge opt_merge.cc @@ -12,11 +13,6 @@ yosys_pass(opt_muxtree yosys_pass(opt_reduce opt_reduce.cc ) -yosys_pass(opt_dff - opt_dff.cc - REQUIRES - simplemap -) yosys_pass(opt_share opt_share.cc ) diff --git a/passes/opt/opt_clean/CMakeLists.txt b/passes/opt/clean/CMakeLists.txt similarity index 100% rename from passes/opt/opt_clean/CMakeLists.txt rename to passes/opt/clean/CMakeLists.txt diff --git a/passes/opt/opt_clean/cells_all.cc b/passes/opt/clean/cells_all.cc similarity index 99% rename from passes/opt/opt_clean/cells_all.cc rename to passes/opt/clean/cells_all.cc index aa97851e3..0c4eccf59 100644 --- a/passes/opt/opt_clean/cells_all.cc +++ b/passes/opt/clean/cells_all.cc @@ -19,7 +19,7 @@ #include "kernel/ffinit.h" #include "kernel/yosys_common.h" -#include "passes/opt/opt_clean/opt_clean.h" +#include "passes/opt/clean/opt_clean.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN diff --git a/passes/opt/opt_clean/cells_temp.cc b/passes/opt/clean/cells_temp.cc similarity index 98% rename from passes/opt/opt_clean/cells_temp.cc rename to passes/opt/clean/cells_temp.cc index b325b68d9..2b9ff6db9 100644 --- a/passes/opt/opt_clean/cells_temp.cc +++ b/passes/opt/clean/cells_temp.cc @@ -17,7 +17,7 @@ * */ -#include "passes/opt/opt_clean/opt_clean.h" +#include "passes/opt/clean/opt_clean.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN diff --git a/passes/opt/opt_clean/inits.cc b/passes/opt/clean/inits.cc similarity index 98% rename from passes/opt/opt_clean/inits.cc rename to passes/opt/clean/inits.cc index 0618e739a..962164b37 100644 --- a/passes/opt/opt_clean/inits.cc +++ b/passes/opt/clean/inits.cc @@ -17,7 +17,7 @@ * */ -#include "passes/opt/opt_clean/opt_clean.h" +#include "passes/opt/clean/opt_clean.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN diff --git a/passes/opt/opt_clean/keep_cache.h b/passes/opt/clean/keep_cache.h similarity index 100% rename from passes/opt/opt_clean/keep_cache.h rename to passes/opt/clean/keep_cache.h diff --git a/passes/opt/opt_clean/opt_clean.cc b/passes/opt/clean/opt_clean.cc similarity index 99% rename from passes/opt/opt_clean/opt_clean.cc rename to passes/opt/clean/opt_clean.cc index 24085c34e..7bc5f0a34 100644 --- a/passes/opt/opt_clean/opt_clean.cc +++ b/passes/opt/clean/opt_clean.cc @@ -20,7 +20,7 @@ #include "kernel/register.h" #include "kernel/log.h" #include "kernel/log_help.h" -#include "passes/opt/opt_clean/opt_clean.h" +#include "passes/opt/clean/opt_clean.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN diff --git a/passes/opt/opt_clean/opt_clean.h b/passes/opt/clean/opt_clean.h similarity index 98% rename from passes/opt/opt_clean/opt_clean.h rename to passes/opt/clean/opt_clean.h index c48a8188a..7086fdbc9 100644 --- a/passes/opt/opt_clean/opt_clean.h +++ b/passes/opt/clean/opt_clean.h @@ -19,7 +19,7 @@ #include "kernel/rtlil.h" #include "kernel/threading.h" -#include "passes/opt/opt_clean/keep_cache.h" +#include "passes/opt/clean/keep_cache.h" #ifndef OPT_CLEAN_SHARED_H #define OPT_CLEAN_SHARED_H diff --git a/passes/opt/opt_clean/wires.cc b/passes/opt/clean/wires.cc similarity index 99% rename from passes/opt/opt_clean/wires.cc rename to passes/opt/clean/wires.cc index e250bdadd..616426f9d 100644 --- a/passes/opt/opt_clean/wires.cc +++ b/passes/opt/clean/wires.cc @@ -17,7 +17,7 @@ * */ -#include "passes/opt/opt_clean/opt_clean.h" +#include "passes/opt/clean/opt_clean.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN diff --git a/passes/opt/dff/CMakeLists.txt b/passes/opt/dff/CMakeLists.txt new file mode 100644 index 000000000..ed72b57ac --- /dev/null +++ b/passes/opt/dff/CMakeLists.txt @@ -0,0 +1,9 @@ +yosys_pass(opt_dff + opt_dff.cc + simple.cc + constbits.cc + eqbits.cc + opt_dff.h + REQUIRES + simplemap +) diff --git a/passes/opt/dff/constbits.cc b/passes/opt/dff/constbits.cc new file mode 100644 index 000000000..4345c17b8 --- /dev/null +++ b/passes/opt/dff/constbits.cc @@ -0,0 +1,355 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Claire Xenia Wolf + * Copyright (C) 2020 Marcelina Kościelnicka + * + * 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. + * + */ + +#include "kernel/ff.h" +#include "passes/opt/dff/opt_dff.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct ConstBitsContext +{ + OptDffWorker &worker; + + // opt_dff -sat rebuilds the solver in batches of at most this many imported + // cells, so one pathological module can't grow a single giant solver + static constexpr int sat_batch_cells = 10000; + + ConstBitsContext(OptDffWorker &worker) : worker(worker) { } + + // lattice join of candidate constants: Sx is the identity (unless -keepdc + // pins it), equal values join, Sm marks a conflict + State combine_const(State a, State b) { + if (a == State::Sx && !worker.opt.keepdc) return b; + if (b == State::Sx && !worker.opt.keepdc) return a; + if (a == b) return a; + return State::Sm; + } + + // candidate stuck-at value of ff bit i, joined over every non-D way the bit + // can acquire a value: init, arst, srst and sr (a clr/set that can ever + // fire forces 0/1) + // returns S0/S1 as the candidate, Sx if unconstrained, Sm on conflict + // the candidate doubles as the induction base case + State check_constbit(FfData &ff, int i) + { + State val = ff.val_init[i]; + if (ff.has_arst) val = combine_const(val, ff.val_arst[i]); + if (ff.has_srst) val = combine_const(val, ff.val_srst[i]); + if (ff.has_sr) { + if (!worker.is_inactive(worker.sigmap(ff.sig_clr[i]), ff.pol_clr)) + val = combine_const(val, State::S0); + if (!worker.is_inactive(worker.sigmap(ff.sig_set[i]), ff.pol_set)) + val = combine_const(val, State::S1); + } + + return val; + } + + // candidate constant of one ff bit, with every constant input already folded in + struct ConstCandidate { + State val = State::Sm; + SigBit d; + SigBit ad; + + bool needs_proof() const { return d.wire || ad.wire; } + }; + + // one suspected-constant ff bit: q (output of cell at bit idx) looks stuck + // at val, and sat must show that every target feeds val back into the bit + struct ConstObligation { + enum Status { Pending, Proven, Dropped }; + + Cell *cell; + int idx; + State val; + SigBit q; + std::vector targets; // non-const inputs (D, AD), must be shown to be eq + Status status = Pending; + + int q_lit = -1; // valid within the current batch + int differ_lit = -1; // some target differs from the candidate value + }; + + // the solver model captures (differ, q) of every pending obligation so one + // counterexample can disprove many at once + struct ConstWatchList { + // interleaved pairs, exprs[2k] = differ_lit and exprs[2k + 1] = q_lit of obs[k] + std::vector exprs; + std::vector obs; + + void watch(ConstObligation &ob) { + exprs.push_back(ob.differ_lit); + exprs.push_back(ob.q_lit); + obs.push_back(&ob); + } + + // drop every obligation whose q holds its constant while some target differs + void drop_disproven(const std::vector &model) const { + for (int k = 0; k < GetSize(obs); k++) { + bool want = (obs[k]->val == State::S1); + if (model[2*k + 1] == want && model[2*k]) + obs[k]->status = ConstObligation::Dropped; + } + } + }; + + void commit_const(dict> &const_bits, Cell *cell, int idx, SigBit q, State val) + { + log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n", + val == State::S1 ? 1 : 0, idx, cell, cell->type.unescape(), worker.module); + worker.initvals.remove_init(q); + worker.module->connect(q, val); + const_bits[cell].insert(idx); + } + + // a wire input can only be proven against a definite candidate value that + // is actually driven somewhere in the design + bool add_const_target(ConstObligation &ob, SigBit sig) + { + if (ob.val != State::S0 && ob.val != State::S1) + return false; + if (!worker.get_modwalker().has_drivers(sig)) + return false; + ob.targets.push_back(sig); + return true; + } + + // try to decide obligation ob under the given per-query effort cap, returns + // true if the cap was hit and the obligation had to be left pending + bool resolve_const_obligation(QuickConeSat &qcsat, int64_t cap, ConstObligation &ob, + const ConstWatchList &watches) + { + // induction step: assuming q already holds the candidate value, the values + // fed through the targets must equal it again, since check_constbit provides the + // base case, so unsat makes the constant an inductive invariant + int vlit = qcsat.ez->value(ob.val == State::S1); + std::vector assumptions; + assumptions.push_back(qcsat.ez->IFF(ob.q_lit, vlit)); + assumptions.push_back(ob.differ_lit); + + std::vector model; + auto res = worker.sat_budget.solve(qcsat, cap, watches.exprs, model, assumptions); + + if (res == SatEffortBudget::Result::LimitReached) + return true; + if (res == SatEffortBudget::Result::Unsat) { + ob.status = ConstObligation::Proven; + return false; + } + + watches.drop_disproven(model); + ob.status = ConstObligation::Dropped; + return false; + } + + // fold every constant input into the candidate from check_constbit, so a + // wire input that sigmaps to a constant counts as constant too + ConstCandidate fold_const_inputs(FfData &ff, int i) + { + ConstCandidate cand; + + State val = check_constbit(ff, i); + if (val == State::Sm) + return cand; + + bool has_d = ff.has_clk || ff.has_gclk; + SigBit d = has_d ? worker.sigmap(ff.sig_d[i]) : SigBit(); + SigBit ad = ff.has_aload ? worker.sigmap(ff.sig_ad[i]) : SigBit(); + + if (has_d) { + if (d.wire) + cand.d = d; + else + val = combine_const(val, d.data); + } + if (ff.has_aload) { + if (ad.wire) + cand.ad = ad; + else + val = combine_const(val, ad.data); + } + + cand.val = val; + return cand; + } + + // commit the bits that are constant by folding alone and return the ones + // that still have a wire input + std::vector fold_const_bits(dict> &const_bits) + { + std::vector obligations; + + for (auto cell : worker.module->selected_cells()) { + if (!cell->is_builtin_ff()) + continue; + + FfData ff(&worker.initvals, cell); + + for (int i = 0; i < ff.width; i++) { + ConstCandidate cand = fold_const_inputs(ff, i); + if (cand.val == State::Sm) + continue; + + if (!cand.needs_proof()) { + commit_const(const_bits, cell, i, ff.sig_q[i], cand.val); + continue; + } + + if (!worker.opt.sat) + continue; + + ConstObligation ob; + ob.cell = cell; + ob.idx = i; + ob.val = cand.val; + ob.q = ff.sig_q[i]; + + bool feasible = true; + if (cand.d.wire) + feasible = add_const_target(ob, cand.d); + if (feasible && cand.ad.wire) + feasible = add_const_target(ob, cand.ad); + if (!feasible) + continue; + + obligations.push_back(std::move(ob)); + } + } + + return obligations; + } + + int build_const_batch(QuickConeSat &qcsat, std::vector &obligations, int batch_begin) + { + int64_t cells_charged = 0; + int batch_end = batch_begin; + + while (batch_end < GetSize(obligations) && !worker.warn_if_budget_spent()) { + auto &ob = obligations[batch_end]; + if (ob.status != ConstObligation::Pending) { + batch_end++; + continue; + } + if (batch_end > batch_begin && GetSize(qcsat.imported_cells) >= sat_batch_cells) + break; + ob.q_lit = qcsat.importSigBit(ob.q); + int vlit = qcsat.ez->value(ob.val == State::S1); + std::vector differ; + for (auto sig : ob.targets) + differ.push_back(qcsat.ez->NOT(qcsat.ez->IFF(qcsat.importSigBit(sig), vlit))); + ob.differ_lit = qcsat.ez->expression(ezSAT::OpOr, differ); + qcsat.prepare(); + cells_charged = worker.sat_budget.charge_import(qcsat, cells_charged); + batch_end++; + } + + return batch_end; + } + + // sweep the batch under the cheap screening cap first, then re-sweep the + // still-undecided obligations with the full remaining budget + void sweep_const_batch(QuickConeSat &qcsat, std::vector &obligations, + int batch_begin, int batch_end, int64_t screen_cap) + { + for (int64_t cap : {screen_cap, (int64_t)0}) { + bool all_resolved = true; + + // watch every pending obligation in the batch + ConstWatchList watches; + for (int obi = batch_begin; obi < batch_end; obi++) { + auto &ob = obligations[obi]; + if (ob.status == ConstObligation::Pending) + watches.watch(ob); + } + + for (int obi = batch_begin; obi < batch_end; obi++) { + auto &ob = obligations[obi]; + if (ob.status != ConstObligation::Pending) + continue; + if (worker.warn_if_budget_spent()) + return; + bool given_up = resolve_const_obligation(qcsat, cap, ob, watches); + if (given_up) + all_resolved = false; + } + + if (all_resolved) + return; + } + } + + // sat: prove or drop the pending obligations in place + void solve_const_obligations(std::vector &obligations) + { + log_assert(worker.opt.sat); + int64_t num_queries = GetSize(obligations); + if (num_queries == 0) + return; + + ModWalker &modwalker = worker.get_modwalker(); + + // screening cap + int64_t screen_cap = 0; + if (worker.sat_budget.enabled()) { + // scale down when we can't afford a full screening round + screen_cap = max((int64_t)20000, min((int64_t)200000, worker.sat_budget.total / (4 * num_queries))); + } + + // NOTE: each obligation is proven independently, so processing obligations in + // batches and stopping early on an exhausted budget should be safe + for (int batch_begin = 0; batch_begin < GetSize(obligations) && !worker.warn_if_budget_spent(); ) { + QuickConeSat qcsat(modwalker); + int batch_end = build_const_batch(qcsat, obligations, batch_begin); + sweep_const_batch(qcsat, obligations, batch_begin, batch_end, screen_cap); + batch_begin = batch_end; + } + } + + bool run_constbits() + { + dict> const_bits; + + std::vector obligations = fold_const_bits(const_bits); + + if (worker.opt.sat) { + solve_const_obligations(obligations); + for (auto &ob : obligations) + if (ob.status == ConstObligation::Proven) + commit_const(const_bits, ob.cell, ob.idx, ob.q, ob.val); + } + + for (auto &[cell, drop] : const_bits) + worker.remove_ff_bits(cell, drop); + + return !const_bits.empty(); + } +}; + +PRIVATE_NAMESPACE_END + +YOSYS_NAMESPACE_BEGIN + +bool OptDffWorker::run_constbits() +{ + return ConstBitsContext(*this).run_constbits(); +} + +YOSYS_NAMESPACE_END diff --git a/passes/opt/dff/eqbits.cc b/passes/opt/dff/eqbits.cc new file mode 100644 index 000000000..c0b8d8dbe --- /dev/null +++ b/passes/opt/dff/eqbits.cc @@ -0,0 +1,510 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Claire Xenia Wolf + * Copyright (C) 2020 Marcelina Kościelnicka + * + * 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. + * + */ + +#include "kernel/ff.h" +#include "passes/opt/dff/opt_dff.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +// Bit-parallel random simulation used as a cheap pre-filter for equivalence +struct BitSim { + Module *module; + SigMap &sigmap; + ModWalker &modwalker; + dict sim_vals; + uint64_t rng_state; + int max_depth; + int evals_left; + + BitSim(Module *m, SigMap &sm, ModWalker &mw) + : module(m), sigmap(sm), modwalker(mw), rng_state(1337) + { + max_depth = module->design->scratchpad_get_int("opt_dff.sim_depth", 10000); + evals_left = module->design->scratchpad_get_int("opt_dff.sim_evals", 1000000); + } + + uint64_t next_rand() { + uint32_t lo = mkhash_xorshift((uint32_t)rng_state); + uint32_t hi = mkhash_xorshift((uint32_t)(rng_state >> 32) ^ lo); + rng_state = ((uint64_t)hi << 32) | lo; + return rng_state; + } + + uint64_t eval_bit(SigBit b, int depth = 0) { + SigBit mapped = sigmap(b); + if (mapped == State::S0) return 0ULL; + if (mapped == State::S1) return ~0ULL; + if (mapped == State::Sx || mapped == State::Sz) return 0ULL; + + auto it = sim_vals.find(mapped); + if (it != sim_vals.end()) return it->second; + + // Failsafe for huge designs + if (depth >= max_depth || evals_left <= 0) { + uint64_t r = next_rand(); + sim_vals[mapped] = r; + return r; + } + evals_left--; + + // pre-seed to break combinational loops + sim_vals[mapped] = 0; + uint64_t res = 0; + + auto drv = modwalker.signal_drivers.find(mapped); + if (drv == modwalker.signal_drivers.end() || drv->second.empty()) { + res = next_rand(); + } else { + auto driver = *drv->second.begin(); + Cell *cell = driver.cell; + + if (cell->is_builtin_ff()) { + res = next_rand(); + } else if (cell->type == ID($_AND_)) { + res = eval_bit(cell->getPort(ID::A)[0], depth+1) & eval_bit(cell->getPort(ID::B)[0], depth+1); + } else if (cell->type == ID($_OR_)) { + res = eval_bit(cell->getPort(ID::A)[0], depth+1) | eval_bit(cell->getPort(ID::B)[0], depth+1); + } else if (cell->type == ID($_XOR_)) { + res = eval_bit(cell->getPort(ID::A)[0], depth+1) ^ eval_bit(cell->getPort(ID::B)[0], depth+1); + } else if (cell->type == ID($_NOT_)) { + res = ~eval_bit(cell->getPort(ID::A)[0], depth+1); + } else if (cell->type == ID($_MUX_)) { + uint64_t s = eval_bit(cell->getPort(ID::S)[0], depth+1); + uint64_t a = eval_bit(cell->getPort(ID::A)[0], depth+1); + uint64_t b = eval_bit(cell->getPort(ID::B)[0], depth+1); + res = (a & ~s) | (b & s); + } else if (cell->type == ID($mux)) { + uint64_t s = eval_bit(cell->getPort(ID::S)[0], depth+1); + uint64_t a = eval_bit(cell->getPort(ID::A)[driver.offset], depth+1); + uint64_t b = eval_bit(cell->getPort(ID::B)[driver.offset], depth+1); + res = (a & ~s) | (b & s); + } else { + res = next_rand(); + } + } + + sim_vals[mapped] = res; + return res; + } +}; + +// concrete 0/1 bit, as opposed to x/z +bool is_def(State s) { + return s == State::S0 || s == State::S1; +} + +struct EqBitsContext +{ + OptDffWorker &worker; + + EqBitsContext(OptDffWorker &worker) : worker(worker) { } + + struct EqBit { + Cell *cell; + int idx; + SigBit q; + }; + + // NOTE: This intentionally duplicates a subset of FfData, as flattening just the + // fields that matter for merging into a single comparable/hashable key is cheaper + struct SigKey { + enum Flag : uint16_t { + InitOne = 1u << 0, + InitX = 1u << 1, + PolClk = 1u << 2, + PolCe = 1u << 3, + PolSrst = 1u << 4, + PolArst = 1u << 5, + PolAload = 1u << 6, + PolClr = 1u << 7, + PolSet = 1u << 8, + CeOverSrst = 1u << 9, + }; + + SigBit clk, ce, srst, arst, aload, clr, set; + IdString cell_type; // for SR + uint16_t flags; + + bool operator==(const SigKey &o) const { + return flags == o.flags && clk == o.clk && ce == o.ce && srst == o.srst && arst == o.arst + && aload == o.aload && clr == o.clr && set == o.set && cell_type == o.cell_type; + } + + Hasher hash_into(Hasher h) const { + h.eat(flags); + h.eat(clk); + h.eat(ce); + h.eat(srst); + h.eat(arst); + h.eat(aload); + h.eat(clr); + h.eat(set); + h.eat(cell_type); + return h; + } + }; + + struct EqCandidates { + std::vector bits; + dict ffs; + std::vector> classes; + }; + + EqCandidates gather_initial_eq_classes() + { + EqCandidates cand; + std::vector keys; + + // Collect FF bits eligible for merging + for (auto cell : worker.module->selected_cells()) { + if (!cell->is_builtin_ff()) + continue; + + FfData ff(&worker.initvals, cell); + if (!ff.has_clk && !ff.has_gclk) + continue; + + cand.ffs.emplace(cell, ff); + + for (int i = 0; i < ff.width; i++) { + // Skip bits whose reset value is undefined (x) + if (ff.has_srst && !is_def(ff.val_srst[i])) continue; + if (ff.has_arst && !is_def(ff.val_arst[i])) continue; + + // Class members are assumed equal in the current cycle and proven equal in the next, which needs + // a base case anchoring them to a common known value + bool def_init = is_def(ff.val_init[i]); + if (!def_init && !ff.has_srst && !ff.has_arst) + continue; + + SigKey k = {}; + + // Flags + if (def_init && ff.val_init[i] == State::S1) + k.flags |= SigKey::InitOne; + else if (!def_init) + k.flags |= SigKey::InitX; + + if (ff.has_clk) { + k.clk = ff.sig_clk; + if (ff.pol_clk) k.flags |= SigKey::PolClk; + } + if (ff.has_ce) { + k.ce = ff.sig_ce; + if (ff.pol_ce) k.flags |= SigKey::PolCe; + } + if (ff.has_srst) { + k.srst = ff.sig_srst; + if (ff.pol_srst) k.flags |= SigKey::PolSrst; + if (ff.ce_over_srst) k.flags |= SigKey::CeOverSrst; + } + if (ff.has_arst) { + k.arst = ff.sig_arst; + if (ff.pol_arst) k.flags |= SigKey::PolArst; + } + if (ff.has_aload) { + k.aload = ff.sig_aload; + if (ff.pol_aload) k.flags |= SigKey::PolAload; + } + if (ff.has_sr) { + k.clr = ff.sig_clr[i]; + k.set = ff.sig_set[i]; + k.cell_type = cell->type; + if (ff.pol_clr) k.flags |= SigKey::PolClr; + if (ff.pol_set) k.flags |= SigKey::PolSet; + } + + cand.bits.push_back({cell, i, ff.sig_q[i]}); + keys.push_back(k); + } + } + + dict> buckets; + for (int i = 0; i < GetSize(cand.bits); i++) + buckets[keys[i]].push_back(i); + + for (auto &kv : buckets) + if (GetSize(kv.second) >= 2) + cand.classes.push_back(std::move(kv.second)); + + return cand; + } + + void filter_classes_sim(EqCandidates &cand) + { + BitSim sim(worker.module, worker.sigmap, worker.get_modwalker()); + + // Assume same class + for (auto &cls : cand.classes) { + uint64_t class_q_val = sim.next_rand(); + for (int idx : cls) { + sim.sim_vals[worker.sigmap(cand.bits[idx].q)] = class_q_val; + } + } + + std::vector> refined_classes; + for (auto &cls : cand.classes) { + dict> sim_buckets; + for (int idx : cls) { + const EqBit &eb = cand.bits[idx]; + const FfData &ff = cand.ffs.at(eb.cell); + uint64_t n_val = sim.eval_bit(ff.sig_d[eb.idx]); + + if (ff.has_aload) { + uint64_t al = sim.eval_bit(ff.sig_aload); + if (!ff.pol_aload) al = ~al; + uint64_t ad = sim.eval_bit(ff.sig_ad[eb.idx]); + n_val = (n_val & ~al) | (ad & al); + } + if (ff.has_arst) { + uint64_t ar = sim.eval_bit(ff.sig_arst); + if (!ff.pol_arst) ar = ~ar; + uint64_t ar_val = (ff.val_arst[eb.idx] == State::S1) ? ~0ULL : 0ULL; + n_val = (n_val & ~ar) | (ar_val & ar); + } + if (ff.has_sr) { + uint64_t clr = sim.eval_bit(ff.sig_clr[eb.idx]); + if (!ff.pol_clr) clr = ~clr; + uint64_t set = sim.eval_bit(ff.sig_set[eb.idx]); + if (!ff.pol_set) set = ~set; + n_val = ~clr & (set | n_val); + } + if (ff.has_srst) { + uint64_t srst = sim.eval_bit(ff.sig_srst); + if (!ff.pol_srst) srst = ~srst; + uint64_t srst_val = (ff.val_srst[eb.idx] == State::S1) ? ~0ULL : 0ULL; + n_val = (n_val & ~srst) | (srst_val & srst); + } + + sim_buckets[n_val].push_back(idx); + } + + for (auto &kv : sim_buckets) + if (GetSize(kv.second) >= 2) + refined_classes.push_back(std::move(kv.second)); + } + + cand.classes = std::move(refined_classes); + } + + void drop_all_classes(EqCandidates &cand) + { + log("opt_dff -sat: skipping all equivalent-flip-flop merges in module %s (solver effort budget " + "exhausted before the equivalences could be proven).\n", log_id(worker.module)); + cand.classes.clear(); + } + + void filter_classes_sat(EqCandidates &cand) + { + auto &classes = cand.classes; + auto &bits = cand.bits; + QuickConeSat qcsat(worker.get_modwalker()); + std::vector q_lit(bits.size(), -1); + std::vector n_lit(bits.size(), -1); + + // Build the next-state function n_lit[idx] of every candidate bit by + // folding the FF's control logic on top of the D input (-> next value) + int64_t cells_charged = 0; + + // Two bits are equivalent if their next states always agree whenever their + // current states (and those of every other candidate pair) agree + for (auto &cls : classes) { + if (worker.warn_if_budget_spent()) + return drop_all_classes(cand); + for (int idx : cls) { + const EqBit &eb = bits[idx]; + const FfData &ff = cand.ffs.at(eb.cell); + q_lit[idx] = qcsat.importSigBit(eb.q); + int n = qcsat.importSigBit(ff.sig_d[eb.idx]); + + if (ff.has_aload) { + int al = qcsat.importSigBit(ff.sig_aload); + if (!ff.pol_aload) al = qcsat.ez->NOT(al); + n = qcsat.ez->ITE(al, qcsat.importSigBit(ff.sig_ad[eb.idx]), n); + } + if (ff.has_arst) { + int ar = qcsat.importSigBit(ff.sig_arst); + if (!ff.pol_arst) ar = qcsat.ez->NOT(ar); + n = qcsat.ez->ITE(ar, qcsat.ez->value(ff.val_arst[eb.idx] == State::S1), n); + } + if (ff.has_sr) { + int clr = qcsat.importSigBit(ff.sig_clr[eb.idx]); + if (!ff.pol_clr) clr = qcsat.ez->NOT(clr); + int set = qcsat.importSigBit(ff.sig_set[eb.idx]); + if (!ff.pol_set) set = qcsat.ez->NOT(set); + n = qcsat.ez->AND(qcsat.ez->NOT(clr), qcsat.ez->OR(set, n)); + } + if (ff.has_srst) { + int srst = qcsat.importSigBit(ff.sig_srst); + if (!ff.pol_srst) srst = qcsat.ez->NOT(srst); + n = qcsat.ez->ITE(srst, qcsat.ez->value(ff.val_srst[eb.idx] == State::S1), n); + } + + n_lit[idx] = n; + } + qcsat.prepare(); + cells_charged = worker.sat_budget.charge_import(qcsat, cells_charged); + } + + // Assume the induction hypo (that every current class is internally equal in the present cycle), and try + // to prove that the members of each class therefore also agree in the next cycle + + // A class survives only if no counterexample exists under that hypo, so combined with the common init/reset + // value that every class shares, this makes the equality an inductive invariant -> bits are eq and safe to merge + std::vector worklist; + std::vector in_worklist(GetSize(classes), true); + + for (int i = 0; i < GetSize(classes); i++) + worklist.push_back(i); + + while (!worklist.empty()) { + int cls_idx = worklist.back(); + worklist.pop_back(); + in_worklist[cls_idx] = false; + + auto &cls = classes[cls_idx]; + if (GetSize(cls) < 2) continue; + + // Induction hypo: assume every candidate class is equal + std::vector assumptions; + for (auto &c : classes) { + if (GetSize(c) < 2) continue; + int rep = c[0]; + for (int k = 1; k < GetSize(c); k++) + assumptions.push_back(qcsat.ez->IFF(q_lit[rep], q_lit[c[k]])); + } + + // Scan the class members against the representative and issue a query per pair, + // stopping early at the first counterexample, which is reused to split the entire + // class at once + int rep = cls[0]; + for (int i = 1; i < GetSize(cls); i++) { + if (n_lit[rep] == n_lit[cls[i]]) + continue; + + if (worker.warn_if_budget_spent()) + return drop_all_classes(cand); + + // Can the next state of the rep and this member ever differ? + int query = qcsat.ez->XOR(n_lit[rep], n_lit[cls[i]]); + // Capture every member's next-state value in that model so one counterexample + // partitions the whole class + std::vector modelExprs; + for (int b : cls) + modelExprs.push_back(n_lit[b]); + + std::vector modelVals; + assumptions.push_back(query); + + auto res = worker.sat_budget.solve(qcsat, 0, modelExprs, modelVals, assumptions); + + if (res == SatEffortBudget::Result::LimitReached) { + worker.warn_if_budget_spent(); + return drop_all_classes(cand); + } + + if (res == SatEffortBudget::Result::Sat) { + // SAT -> partition entire class + std::vector sub0; + std::vector sub1; + + for (int b_idx = 0; b_idx < GetSize(cls); b_idx++) { + if (modelVals[b_idx]) + sub1.push_back(cls[b_idx]); + else + sub0.push_back(cls[b_idx]); + } + + classes[cls_idx] = std::move(sub0); + classes.push_back(std::move(sub1)); + in_worklist.push_back(false); + + // Partition was split -> the induction hypo weakened + for (int j = 0; j < GetSize(classes); j++) { + if (GetSize(classes[j]) >= 2 && !in_worklist[j]) { + worklist.push_back(j); + in_worklist[j] = true; + } + } + + break; // Process new splits + } + + assumptions.pop_back(); // Remove query for the next pairwise check if UNSAT + } + } + } + + bool apply_eq_merges(const EqCandidates &cand) + { + bool any_change = false; + dict> remove_bits; + + // Drive every non-rep Q from its class rep, drop merged bits from their FFs + for (auto &cls : cand.classes) { + if (GetSize(cls) < 2) + continue; + SigBit rep_q = cand.bits[cls[0]].q; + any_change = true; + for (int k = 1; k < GetSize(cls); k++) { + const EqBit &eb = cand.bits[cls[k]]; + worker.initvals.remove_init(eb.q); + worker.module->connect(eb.q, rep_q); + remove_bits[eb.cell].insert(eb.idx); + } + } + + for (auto &[cell, drop] : remove_bits) + worker.remove_ff_bits(cell, drop); + + return any_change; + } + + bool run_eqbits() + { + EqCandidates cand = gather_initial_eq_classes(); + if (cand.classes.empty()) + return false; + + // Simulation prepass + filter_classes_sim(cand); + if (cand.classes.empty()) + return false; + + // SAT prove + filter_classes_sat(cand); + if (cand.classes.empty()) + return false; + + return apply_eq_merges(cand); + } +}; + +PRIVATE_NAMESPACE_END + +YOSYS_NAMESPACE_BEGIN + +bool OptDffWorker::run_eqbits() +{ + return EqBitsContext(*this).run_eqbits(); +} + +YOSYS_NAMESPACE_END diff --git a/passes/opt/dff/opt_dff.cc b/passes/opt/dff/opt_dff.cc new file mode 100644 index 000000000..4e6d459df --- /dev/null +++ b/passes/opt/dff/opt_dff.cc @@ -0,0 +1,144 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Claire Xenia Wolf + * Copyright (C) 2020 Marcelina Kościelnicka + * + * 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. + * + */ + +#include "kernel/log.h" +#include "kernel/register.h" +#include "kernel/ff.h" +#include "passes/opt/dff/opt_dff.h" +#include +#include + +USING_YOSYS_NAMESPACE + +YOSYS_NAMESPACE_BEGIN + +OptDffWorker::OptDffWorker(const OptDffOptions &opt, Module *mod) + : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod) +{ + sat_budget = SatEffortBudget(module->design->scratchpad_get_int("opt_dff.sat_effort", 1000000000)); +} + +void OptDffWorker::remove_ff_bits(Cell *cell, const pool &drop) +{ + FfData ff(&initvals, cell); + std::vector keep; + for (int i = 0; i < ff.width; i++) + if (!drop.count(i)) + keep.push_back(i); + + FfData new_ff = ff.slice(keep); + new_ff.cell = cell; + new_ff.emit(); +} + +YOSYS_NAMESPACE_END + +PRIVATE_NAMESPACE_BEGIN + +struct OptDffPass : public Pass { + OptDffPass() : Pass("opt_dff", "perform DFF optimizations") { } + + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" opt_dff [-nodffe] [-nosdff] [-keepdc] [-sat] [selection]\n"); + log("\n"); + log("This pass converts flip-flops to a more suitable type by merging clock enables\n"); + log("and synchronous reset multiplexers, removing unused control inputs, or\n"); + log("potentially removes the flip-flop altogether, converting it to a constant\n"); + log("driver.\n"); + log("\n"); + log(" -nodffe\n"); + log(" disables dff -> dffe conversion, and other transforms recognizing clock\n"); + log(" enable\n"); + log("\n"); + log(" -nosdff\n"); + log(" disables dff -> sdff conversion, and other transforms recognizing sync\n"); + log(" resets\n"); + log("\n"); + log(" -simple-dffe\n"); + log(" only enables clock enable recognition transform for obvious cases\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(" or merged with equivalent flip-flops. this reasons in 2-valued logic\n"); + log(" and may resolve don't-care bits, so it is incompatible with -keepdc.\n"); + log(" the scratchpad option 'opt_dff.sat_effort' (solver propagation steps,\n"); + log(" default 1000000000, 0 = unlimited) deterministically bounds the total\n"); + log(" sat effort spent per module, remaining proofs are skipped once exceeded.\n"); + log("\n"); + log(" -keepdc\n"); + log(" some optimizations change the behavior of the circuit with respect to\n"); + log(" don't-care bits. for example in 'a+0' a single x-bit in 'a' will cause\n"); + log(" all result bits to be set to x. this behavior changes when 'a+0' is\n"); + log(" replaced by 'a'. the -keepdc option disables all such optimizations.\n"); + log("\n"); + } + + void execute(std::vector args, RTLIL::Design *design) override + { + log_header(design, "Executing OPT_DFF pass (perform DFF optimizations).\n"); + + OptDffOptions opt; + opt.nodffe = false; + opt.nosdff = false; + opt.simple_dffe = false; + opt.keepdc = false; + opt.sat = false; + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-nodffe") { opt.nodffe = true; continue; } + if (args[argidx] == "-nosdff") { opt.nosdff = true; continue; } + if (args[argidx] == "-simple-dffe") { opt.simple_dffe = true; continue; } + if (args[argidx] == "-keepdc") { opt.keepdc = true; continue; } + if (args[argidx] == "-sat") { opt.sat = true; continue; } + break; + } + extra_args(args, argidx, design); + + // The SAT engine reasons in 2-valued logic (a constant x is treated as + // 0), so it can resolve don't-care bits to concrete values -- exactly + // what -keepdc promises not to do. Refuse the combination rather than + // silently ignore -keepdc. + if (opt.sat && opt.keepdc) + log_cmd_error("The -sat and -keepdc options are mutually exclusive.\n"); + + bool did_something = false; + for (auto mod : design->selected_modules()) { + OptDffWorker worker(opt, mod); + if (worker.run()) + did_something = true; + // constbits also runs without -sat: it folds bits with all-constant + // inputs, -sat additionally proves bits with wire inputs + if (worker.run_constbits()) + did_something = true; + if (opt.sat && worker.run_eqbits()) + did_something = true; + } + + if (did_something) + design->scratchpad_set_bool("opt.did_something", true); + } +} OptDffPass; + +PRIVATE_NAMESPACE_END diff --git a/passes/opt/dff/opt_dff.h b/passes/opt/dff/opt_dff.h new file mode 100644 index 000000000..837c9297d --- /dev/null +++ b/passes/opt/dff/opt_dff.h @@ -0,0 +1,103 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Claire Xenia Wolf + * Copyright (C) 2020 Marcelina Kościelnicka + * + * 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. + * + */ + +#include "kernel/log.h" +#include "kernel/rtlil.h" +#include "kernel/qcsat.h" +#include "kernel/modtools.h" +#include "kernel/sigtools.h" +#include "kernel/ffinit.h" + +#ifndef OPT_DFF_H +#define OPT_DFF_H + +YOSYS_NAMESPACE_BEGIN + +struct OptDffOptions +{ + bool nosdff; + bool nodffe; + bool simple_dffe; + bool sat; + bool keepdc; +}; + +struct OptDffWorker +{ + const OptDffOptions &opt; + Module *module; + + SigMap sigmap; // Signal aliasing + FfInitVals initvals; + + SatEffortBudget sat_budget; + bool sat_warned = false; + + // modwalker is expensive to build, so share one lazily between constbits and eqbits + std::unique_ptr modwalker_ptr; + + OptDffWorker(const OptDffOptions &opt, Module *mod); + + ModWalker &get_modwalker() + { + if (!modwalker_ptr) + modwalker_ptr = std::make_unique(module->design, module); + return *modwalker_ptr; + } + + bool warn_if_budget_spent() + { + if (!sat_budget.spent()) + return false; + if (!sat_warned) + log_warning("opt_dff -sat: solver effort budget for module %s is exhausted, leaving the " + "remaining FFs un-optimized. Raise or clear the limit with the scratchpad " + "option 'opt_dff.sat_effort' (0 disables it).\n", log_id(module)); + sat_warned = true; + return true; + } + + + bool is_active(SigBit sig, bool pol) const { + return sig == (pol ? State::S1 : State::S0); + } + + bool is_inactive(SigBit sig, bool pol) const { + return sig == (pol ? State::S0 : State::S1); + } + + bool is_always_active(SigBit sig, bool pol) const { + return is_active(sig, pol) || (!opt.keepdc && sig == State::Sx); + } + + bool is_always_inactive(SigBit sig, bool pol) const { + return is_inactive(sig, pol) || (!opt.keepdc && sig == State::Sx); + } + + void remove_ff_bits(Cell *cell, const pool &drop); + + bool run(); + bool run_constbits(); + bool run_eqbits(); +}; + +YOSYS_NAMESPACE_END + +#endif /* OPT_DFF_H */ diff --git a/passes/opt/dff/simple.cc b/passes/opt/dff/simple.cc new file mode 100644 index 000000000..9d0a6faef --- /dev/null +++ b/passes/opt/dff/simple.cc @@ -0,0 +1,768 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Claire Xenia Wolf + * Copyright (C) 2020 Marcelina Kościelnicka + * + * 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. + * + */ + +#include "kernel/ff.h" +#include "kernel/pattern.h" +#include "passes/opt/dff/opt_dff.h" +#include "passes/techmap/simplemap.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct SimpleContext +{ + OptDffWorker &worker; + + // Cell to port bit index + typedef std::pair cell_int_t; + + dict bitusers; // Signal sink count + dict bit2mux; // Signal bit to driving MUX + + std::vector dff_cells; + + SimpleContext(OptDffWorker &worker) : worker(worker) + { + // Gathering two kinds of information here for every sigmapped SigBit: + // - bitusers: how many users it has (muxes will only be merged into FFs if the FF is the only user) + // - bit2mux: the mux cell and bit index that drives it, if any + + for (auto wire : worker.module->wires()) + if (wire->port_output) + for (auto bit : worker.sigmap(wire)) + bitusers[bit]++; + + for (auto cell : worker.module->cells()) { + if (cell->type.in(ID($mux), ID($pmux), ID($_MUX_))) { + RTLIL::SigSpec sig_y = worker.sigmap(cell->getPort(ID::Y)); + for (int i = 0; i < GetSize(sig_y); i++) + bit2mux[sig_y[i]] = cell_int_t(cell, i); + } + + for (auto conn : cell->connections()) { + bool is_output = cell->output(conn.first); + if (!is_output || !cell->known()) + for (auto bit : worker.sigmap(conn.second)) + bitusers[bit]++; + } + + if (worker.module->design->selected(worker.module, cell) && cell->is_builtin_ff()) + dff_cells.push_back(cell); + } + } + + SigSpec create_not(SigSpec a, bool is_fine) { + if (is_fine) + return worker.module->NotGate(NEW_ID, a); + else + return worker.module->Not(NEW_ID, a); + } + + SigSpec create_and(SigSpec a, SigSpec b, bool is_fine) { + if (is_fine) + return worker.module->AndGate(NEW_ID, a, b); + else + return worker.module->And(NEW_ID, a, b); + } + + void create_mux_to_output(SigSpec a, SigSpec b, SigSpec sel, SigSpec y, bool pol, bool is_fine) { + if (is_fine) { + if (pol) + worker.module->addMuxGate(NEW_ID, a, b, sel, y); + else + worker.module->addMuxGate(NEW_ID, b, a, sel, y); + } else { + if (pol) + worker.module->addMux(NEW_ID, a, b, sel, y); + else + worker.module->addMux(NEW_ID, b, a, sel, y); + } + } + + void maybe_simplemap(Cell *c, bool make_gates) { + if (make_gates) { + simplemap(worker.module, c); + worker.module->remove(c); + } + } + + patterns_t find_muxtree_feedback_patterns(RTLIL::SigBit d, RTLIL::SigBit q, pattern_t path) + { + // Find feedback paths D->Q through mux tree, replacing found paths with Sx + patterns_t ret; + + if (d == q) { + ret.insert(path); + return ret; // Feedback found + } + + if (bit2mux.count(d) == 0 || bitusers[d] > 1) + return ret; // D not driven by MUX / MUX drives multiple loads + + cell_int_t mbit = bit2mux.at(d); + RTLIL::SigSpec sig_a = worker.sigmap(mbit.first->getPort(ID::A)); + RTLIL::SigSpec sig_b = worker.sigmap(mbit.first->getPort(ID::B)); + RTLIL::SigSpec sig_s = worker.sigmap(mbit.first->getPort(ID::S)); + int width = GetSize(sig_a), index = mbit.second; + + // Traverse MUX tree + for (int i = 0; i < GetSize(sig_s); i++) { + if (path.count(sig_s[i]) && path.at(sig_s[i])) { + ret = find_muxtree_feedback_patterns(sig_b[i*width + index], q, path); + if (sig_b[i*width + index] == q) { + RTLIL::SigSpec s = mbit.first->getPort(ID::B); + s[i*width + index] = RTLIL::Sx; + mbit.first->setPort(ID::B, s); + } + + return ret; + } + } + + // Specific path wasn't forced, explore the 0 branch + pattern_t path_else = path; + for (int i = 0; i < GetSize(sig_s); i++) { + if (path.count(sig_s[i])) + continue; + + pattern_t path_this = path; + path_else[sig_s[i]] = false; // Assume S=0 for 'else' path + path_this[sig_s[i]] = true; // Assume S=1 for 'this' path + + // Selected when S=1 + for (auto &pat : find_muxtree_feedback_patterns(sig_b[i*width + index], q, path_this)) + ret.insert(pat); + + if (sig_b[i*width + index] == q) { + RTLIL::SigSpec s = mbit.first->getPort(ID::B); + s[i*width + index] = RTLIL::Sx; + mbit.first->setPort(ID::B, s); + } + } + + // Selected when S=0 + for (auto &pat : find_muxtree_feedback_patterns(sig_a[index], q, path_else)) + ret.insert(pat); + + if (sig_a[index] == q) { + RTLIL::SigSpec s = mbit.first->getPort(ID::A); + s[index] = RTLIL::Sx; + mbit.first->setPort(ID::A, s); + } + + return ret; + } + + ctrl_t make_patterns_logic(const patterns_t &patterns, const ctrls_t &ctrls, bool make_gates) + { + if (patterns.empty() && GetSize(ctrls) == 1) + return *ctrls.begin(); + + RTLIL::SigSpec or_input; + + // Build logic for each feedback pattern + for (auto pat : patterns) { + RTLIL::SigSpec s1, s2; + + for (auto it : pat) { + s1.append(it.first); + s2.append(it.second); + } + + RTLIL::SigSpec y = worker.module->addWire(NEW_ID); + RTLIL::Cell *c = worker.module->addNe(NEW_ID, s1, s2, y); + maybe_simplemap(c, make_gates); + or_input.append(y); + } + + // Add existing control signals + for (auto item : ctrls) { + if (item.second) + or_input.append(item.first); + else + or_input.append(create_not(item.first, make_gates)); + } + + if (GetSize(or_input) == 0) return ctrl_t(State::S1, true); + if (GetSize(or_input) == 1) return ctrl_t(or_input, true); + + RTLIL::SigSpec y = worker.module->addWire(NEW_ID); + RTLIL::Cell *c = worker.module->addReduceAnd(NEW_ID, or_input, y); + maybe_simplemap(c, make_gates); + return ctrl_t(y, true); + } + + ctrl_t combine_resets(const ctrls_t &ctrls, bool make_gates) + { + if (GetSize(ctrls) == 1) + return *ctrls.begin(); + + bool final_pol = false; + for (auto item : ctrls) + if (item.second) + final_pol = true; + + RTLIL::SigSpec or_input; + for (auto item : ctrls) { + if (item.second == final_pol) + or_input.append(item.first); + else + or_input.append(create_not(item.first, make_gates)); + } + + RTLIL::SigSpec y = worker.module->addWire(NEW_ID); + RTLIL::Cell *c = final_pol + ? worker.module->addReduceOr(NEW_ID, or_input, y) + : worker.module->addReduceAnd(NEW_ID, or_input, y); + maybe_simplemap(c, make_gates); + return ctrl_t(y, final_pol); + } + + bool signal_all_same(const SigSpec &sig) { + for (int i = 1; i < GetSize(sig); i++) + if (sig[i] != sig[0]) + return false; + return true; + } + + bool optimize_sr(FfData &ff, Cell *cell, bool &changed) + { + // Removes SR if CLR/SET are always active + // Converts SR to ARST if one pin is never active + // Converts SR to ARST if SET/CLR are inverses of eachother + bool sr_removed = false; + std::vector keep_bits; + + // Check for constant Set/Clear inputs + for (int i = 0; i < ff.width; i++) { + if (worker.is_always_active(ff.sig_clr[i], ff.pol_clr)) { + worker.initvals.remove_init(ff.sig_q[i]); + worker.module->connect(ff.sig_q[i], State::S0); + log("Handling always-active CLR at position %d on %s (%s) from module %s (changing to const driver).\n", + i, cell, cell->type.unescape(), worker.module); + sr_removed = true; + } else if (worker.is_always_active(ff.sig_set[i], ff.pol_set)) { + worker.initvals.remove_init(ff.sig_q[i]); + if (!ff.pol_clr) + worker.module->connect(ff.sig_q[i], ff.sig_clr[i]); + else if (ff.is_fine) + worker.module->addNotGate(NEW_ID, ff.sig_clr[i], ff.sig_q[i]); + else + worker.module->addNot(NEW_ID, ff.sig_clr[i], ff.sig_q[i]); + log("Handling always-active SET at position %d on %s (%s) from module %s (changing to combinatorial circuit).\n", + i, cell, cell->type.unescape(), worker.module); + sr_removed = true; + } else { + keep_bits.push_back(i); + } + } + + if (sr_removed) { + if (keep_bits.empty()) { + worker.module->remove(cell); + return true; // FF fully removed + } + ff = ff.slice(keep_bits); + ff.cell = cell; + changed = true; + } + + // Try SR -> ARST conversion + bool clr_inactive = ff.pol_clr ? ff.sig_clr.is_fully_zero() : ff.sig_clr.is_fully_ones(); + bool set_inactive = ff.pol_set ? ff.sig_set.is_fully_zero() : ff.sig_set.is_fully_ones(); + + if (clr_inactive && signal_all_same(ff.sig_set)) { + log("Removing never-active CLR on %s (%s) from module %s.\n", + cell, cell->type.unescape(), worker.module); + ff.has_sr = false; + ff.has_arst = true; + ff.pol_arst = ff.pol_set; + ff.sig_arst = ff.sig_set[0]; + ff.val_arst = Const(State::S1, ff.width); + changed = true; + } else if (set_inactive && signal_all_same(ff.sig_clr)) { + log("Removing never-active SET on %s (%s) from module %s.\n", + cell, cell->type.unescape(), worker.module); + ff.has_sr = false; + ff.has_arst = true; + ff.pol_arst = ff.pol_clr; + ff.sig_arst = ff.sig_clr[0]; + ff.val_arst = Const(State::S0, ff.width); + changed = true; + } else if (ff.pol_clr == ff.pol_set) { + State val_neutral = ff.pol_set ? State::S0 : State::S1; + SigBit sig_arst = (ff.sig_clr[0] == val_neutral) ? ff.sig_set[0] : ff.sig_clr[0]; + + bool failed = false; + Const::Builder val_arst_builder(ff.width); + for (int i = 0; i < ff.width; i++) { + if (ff.sig_clr[i] == sig_arst && ff.sig_set[i] == val_neutral) + val_arst_builder.push_back(State::S0); + else if (ff.sig_set[i] == sig_arst && ff.sig_clr[i] == val_neutral) + val_arst_builder.push_back(State::S1); + else { + failed = true; + break; + } + } + + if (!failed) { + log("Converting CLR/SET to ARST on %s (%s) from module %s.\n", + cell, cell->type.unescape(), worker.module); + ff.has_sr = false; + ff.has_arst = true; + ff.val_arst = val_arst_builder.build(); + ff.sig_arst = sig_arst; + ff.pol_arst = ff.pol_clr; + changed = true; + } + } + + return false; + } + + bool optimize_aload(FfData &ff, Cell *cell, bool &changed) + { + // Removes unused Async Load + // Converts constant Async Load to ARST + if (worker.is_always_inactive(ff.sig_aload, ff.pol_aload)) { + log("Removing never-active async load on %s (%s) from module %s.\n", + cell, cell->type.unescape(), worker.module); + ff.has_aload = false; + changed = true; + return false; + } + + if (worker.is_active(ff.sig_aload, ff.pol_aload)) { + // ALOAD always active + log("Handling always-active async load on %s (%s) from module %s (changing to combinatorial circuit).\n", + cell, cell->type.unescape(), worker.module); + ff.remove(); + + if (ff.has_sr) { + SigSpec tmp; + if (ff.is_fine) { + tmp = ff.pol_set + ? worker.module->MuxGate(NEW_ID, ff.sig_ad, State::S1, ff.sig_set) + : worker.module->MuxGate(NEW_ID, State::S1, ff.sig_ad, ff.sig_set); + + if (ff.pol_clr) + worker.module->addMuxGate(NEW_ID, tmp, State::S0, ff.sig_clr, ff.sig_q); + else + worker.module->addMuxGate(NEW_ID, State::S0, tmp, ff.sig_clr, ff.sig_q); + } else { + tmp = ff.pol_set + ? worker.module->Or(NEW_ID, ff.sig_ad, ff.sig_set) + : worker.module->Or(NEW_ID, ff.sig_ad, worker.module->Not(NEW_ID, ff.sig_set)); + + if (ff.pol_clr) + worker.module->addAnd(NEW_ID, tmp, worker.module->Not(NEW_ID, ff.sig_clr), ff.sig_q); + else + worker.module->addAnd(NEW_ID, tmp, ff.sig_clr, ff.sig_q); + } + } else if (ff.has_arst) { + create_mux_to_output(ff.sig_ad, ff.val_arst, ff.sig_arst, ff.sig_q, ff.pol_arst, ff.is_fine); + } else { + worker.module->connect(ff.sig_q, ff.sig_ad); + } + return true; + } + + // AD is constant -> ARST + if (ff.sig_ad.is_fully_const() && !ff.has_arst && !ff.has_sr) { + log("Changing const-value async load to async reset on %s (%s) from module %s.\n", + cell, cell->type.unescape(), worker.module); + ff.has_arst = true; + ff.has_aload = false; + ff.sig_arst = ff.sig_aload; + ff.pol_arst = ff.pol_aload; + ff.val_arst = ff.sig_ad.as_const(); + changed = true; + } + + return false; + } + + bool optimize_arst(FfData &ff, Cell *cell, bool &changed) + { + // Removes ARST if never active or replaces FF if always active + if (worker.is_inactive(ff.sig_arst, ff.pol_arst)) { + log("Removing never-active ARST on %s (%s) from module %s.\n", + cell, cell->type.unescape(), worker.module); + ff.has_arst = false; + changed = true; + } else if (worker.is_always_active(ff.sig_arst, ff.pol_arst)) { + log("Handling always-active ARST on %s (%s) from module %s (changing to const driver).\n", + cell, cell->type.unescape(), worker.module); + ff.remove(); + worker.module->connect(ff.sig_q, ff.val_arst); + return true; + } + + return false; + } + + void optimize_srst(FfData &ff, Cell *cell, bool &changed) + { + // Removes SRST if never active or forces D to reset value if always active + if (worker.is_inactive(ff.sig_srst, ff.pol_srst)) { + log("Removing never-active SRST on %s (%s) from module %s.\n", + cell, cell->type.unescape(), worker.module); + ff.has_srst = false; + changed = true; + } else if (worker.is_always_active(ff.sig_srst, ff.pol_srst)) { + log("Handling always-active SRST on %s (%s) from module %s (changing to const D).\n", + cell, cell->type.unescape(), worker.module); + ff.has_srst = false; + if (!ff.ce_over_srst) + ff.has_ce = false; + + ff.sig_d = ff.val_srst; + changed = true; + } + } + + void optimize_ce(FfData &ff, Cell *cell, bool &changed) + { + if (worker.is_always_inactive(ff.sig_ce, ff.pol_ce)) { + if (ff.has_srst && !ff.ce_over_srst) { + log("Handling never-active EN on %s (%s) from module %s (connecting SRST instead).\n", + cell, cell->type.unescape(), worker.module); + ff.pol_ce = ff.pol_srst; + ff.sig_ce = ff.sig_srst; + ff.has_srst = false; + ff.sig_d = ff.val_srst; + changed = true; + } else if (!worker.opt.keepdc || ff.val_init.is_fully_def()) { + log("Handling never-active EN on %s (%s) from module %s (removing D path).\n", + cell, cell->type.unescape(), worker.module); + ff.has_ce = ff.has_clk = ff.has_srst = false; + changed = true; + } else { + ff.sig_d = ff.sig_q; + ff.has_ce = ff.has_srst = false; + changed = true; + } + } else if (worker.is_active(ff.sig_ce, ff.pol_ce)) { + log("Removing always-active EN on %s (%s) from module %s.\n", + cell, cell->type.unescape(), worker.module); + ff.has_ce = false; + changed = true; + } + } + + void optimize_const_clk(FfData &ff, Cell *cell, bool &changed) + { + if (!worker.opt.keepdc || ff.val_init.is_fully_def()) { + log("Handling const CLK on %s (%s) from module %s (removing D path).\n", + cell, cell->type.unescape(), worker.module); + ff.has_ce = ff.has_clk = ff.has_srst = false; + changed = true; + } else if (ff.has_ce || ff.has_srst || ff.sig_d != ff.sig_q) { + ff.sig_d = ff.sig_q; + ff.has_ce = ff.has_srst = false; + changed = true; + } + } + + void optimize_d_equals_q(FfData &ff, Cell *cell, bool &changed) + { + // Detect feedback loops where D is hardwired to Q + if (ff.has_clk && ff.has_srst) { + log("Handling D = Q on %s (%s) from module %s (conecting SRST instead).\n", + cell, cell->type.unescape(), worker.module); + if (ff.has_ce && ff.ce_over_srst) { + SigSpec ce = ff.pol_ce ? ff.sig_ce : create_not(ff.sig_ce, ff.is_fine); + SigSpec srst = ff.pol_srst ? ff.sig_srst : create_not(ff.sig_srst, ff.is_fine); + ff.sig_ce = create_and(ce, srst, ff.is_fine); + ff.pol_ce = true; + } else { + ff.pol_ce = ff.pol_srst; + ff.sig_ce = ff.sig_srst; + } + + ff.has_ce = true; + ff.has_srst = false; + ff.sig_d = ff.val_srst; + changed = true; + } else if (!worker.opt.keepdc || ff.val_init.is_fully_def()) { + log("Handling D = Q on %s (%s) from module %s (removing D path).\n", + cell, cell->type.unescape(), worker.module); + ff.has_gclk = ff.has_clk = ff.has_ce = false; + changed = true; + } + } + + bool try_merge_srst(FfData &ff, Cell *cell, bool &changed) + { + std::map> groups; + std::vector remaining_indices; + Const::Builder val_srst_builder(ff.width); + + for (int i = 0; i < ff.width; i++) { + ctrls_t resets; + State reset_val = ff.has_srst ? ff.val_srst[i] : State::Sx; + + while (bit2mux.count(ff.sig_d[i]) && bitusers[ff.sig_d[i]] == 1) { + cell_int_t mbit = bit2mux.at(ff.sig_d[i]); + if (GetSize(mbit.first->getPort(ID::S)) != 1) + break; + + SigBit s = mbit.first->getPort(ID::S); + SigBit a = mbit.first->getPort(ID::A)[mbit.second]; + SigBit b = mbit.first->getPort(ID::B)[mbit.second]; + + if ((a == State::S0 || a == State::S1) && (b == State::S0 || b == State::S1)) + break; + + bool b_const = (b == State::S0 || b == State::S1); + bool a_const = (a == State::S0 || a == State::S1); + + if (b_const && (b == reset_val || reset_val == State::Sx) && a != ff.sig_q[i]) { + reset_val = b.data; + resets.insert(ctrl_t(s, true)); + ff.sig_d[i] = a; + } else if (a_const && (a == reset_val || reset_val == State::Sx) && b != ff.sig_q[i]) { + reset_val = a.data; + resets.insert(ctrl_t(s, false)); + ff.sig_d[i] = b; + } else { + break; + } + } + + if (!resets.empty()) { + if (ff.has_srst) + resets.insert(ctrl_t(ff.sig_srst, ff.pol_srst)); + + groups[resets].push_back(i); + } else { + remaining_indices.push_back(i); + } + + val_srst_builder.push_back(reset_val); + } + + Const val_srst = val_srst_builder.build(); + + for (auto &it : groups) { + FfData new_ff = ff.slice(it.second); + Const::Builder new_val_srst_builder(new_ff.width); + for (int i = 0; i < new_ff.width; i++) + new_val_srst_builder.push_back(val_srst[it.second[i]]); + + new_ff.val_srst = new_val_srst_builder.build(); + + ctrl_t srst = combine_resets(it.first, ff.is_fine); + new_ff.has_srst = true; + new_ff.sig_srst = srst.first; + new_ff.pol_srst = srst.second; + if (new_ff.has_ce) + new_ff.ce_over_srst = true; + + Cell *new_cell = new_ff.emit(); + if (new_cell) + dff_cells.push_back(new_cell); + + log("Adding SRST signal on %s (%s) from module %s (D = %s, Q = %s, rval = %s).\n", + cell, cell->type.unescape(), worker.module, + log_signal(new_ff.sig_d), log_signal(new_ff.sig_q), log_signal(new_ff.val_srst)); + } + + if (remaining_indices.empty()) { + worker.module->remove(cell); + return true; + } + + if (GetSize(remaining_indices) != ff.width) { + ff = ff.slice(remaining_indices); + ff.cell = cell; + changed = true; + } + + return false; + } + + bool try_merge_ce(FfData &ff, Cell *cell, bool &changed) + { + std::map, std::vector> groups; + std::vector remaining_indices; + + for (int i = 0; i < ff.width; i++) { + ctrls_t enables; + + while (bit2mux.count(ff.sig_d[i]) && bitusers[ff.sig_d[i]] == 1) { + cell_int_t mbit = bit2mux.at(ff.sig_d[i]); + if (GetSize(mbit.first->getPort(ID::S)) != 1) + break; + + SigBit s = mbit.first->getPort(ID::S); + SigBit a = mbit.first->getPort(ID::A)[mbit.second]; + SigBit b = mbit.first->getPort(ID::B)[mbit.second]; + + if (a == ff.sig_q[i]) { + enables.insert(ctrl_t(s, true)); + ff.sig_d[i] = b; + } else if (b == ff.sig_q[i]) { + enables.insert(ctrl_t(s, false)); + ff.sig_d[i] = a; + } else { + break; + } + } + + patterns_t patterns; + if (!worker.opt.simple_dffe) + patterns = find_muxtree_feedback_patterns(ff.sig_d[i], ff.sig_q[i], pattern_t()); + + if (!patterns.empty() || !enables.empty()) { + if (ff.has_ce) + enables.insert(ctrl_t(ff.sig_ce, ff.pol_ce)); + simplify_patterns(patterns); + groups[std::make_pair(patterns, enables)].push_back(i); + } else { + remaining_indices.push_back(i); + } + } + + for (auto &it : groups) { + FfData new_ff = ff.slice(it.second); + ctrl_t en = make_patterns_logic(it.first.first, it.first.second, ff.is_fine); + + new_ff.has_ce = true; + new_ff.sig_ce = en.first; + new_ff.pol_ce = en.second; + new_ff.ce_over_srst = false; + + Cell *new_cell = new_ff.emit(); + if (new_cell) + dff_cells.push_back(new_cell); + + log("Adding EN signal on %s (%s) from module %s (D = %s, Q = %s).\n", + cell, cell->type.unescape(), worker.module, + log_signal(new_ff.sig_d), log_signal(new_ff.sig_q)); + } + + if (remaining_indices.empty()) { + worker.module->remove(cell); + return true; + } + + if (GetSize(remaining_indices) != ff.width) { + ff = ff.slice(remaining_indices); + ff.cell = cell; + changed = true; + } + + return false; + } + + bool run() + { + bool did_something = false; + + while (!dff_cells.empty()) { + Cell *cell = dff_cells.back(); + dff_cells.pop_back(); + + FfData ff(&worker.initvals, cell); + bool changed = false; + + if (!ff.width) { + ff.remove(); + did_something = true; + continue; + } + + // Async control signal opt + if (ff.has_sr && optimize_sr(ff, cell, changed)) { + did_something = true; + continue; + } + + if (ff.has_aload && optimize_aload(ff, cell, changed)) { + did_something = true; + continue; + } + + if (ff.has_arst && optimize_arst(ff, cell, changed)) { + did_something = true; + continue; + } + + // Sync control signal opt + if (ff.has_srst) + optimize_srst(ff, cell, changed); + + if (ff.has_ce) + optimize_ce(ff, cell, changed); + + if (ff.has_clk && ff.sig_clk.is_fully_const()) + optimize_const_clk(ff, cell, changed); + + // Feedback (D=Q) opt + if ((ff.has_clk || ff.has_gclk) && ff.sig_d == ff.sig_q) + optimize_d_equals_q(ff, cell, changed); + + if (ff.has_aload && !ff.has_clk && ff.sig_ad == ff.sig_q) { + log("Handling AD = Q on %s (%s) from module %s (removing async load path).\n", + cell, cell->type.unescape(), worker.module); + ff.has_aload = false; + changed = true; + } + + // Mux merging + if (ff.has_clk && ff.sig_d != ff.sig_q) { + bool can_merge_srst = !ff.has_arst && !ff.has_sr && + (!ff.has_srst || !ff.has_ce || ff.ce_over_srst) && !worker.opt.nosdff; + + if (can_merge_srst && try_merge_srst(ff, cell, changed)) { + did_something = true; + continue; + } + + bool can_merge_ce = (!ff.has_srst || !ff.has_ce || !ff.ce_over_srst) && !worker.opt.nodffe; + + if (can_merge_ce && try_merge_ce(ff, cell, changed)) { + did_something = true; + continue; + } + } + + if (changed) { + ff.emit(); + did_something = true; + } + } + + return did_something; + } +}; + +PRIVATE_NAMESPACE_END + +YOSYS_NAMESPACE_BEGIN + +bool OptDffWorker::run() +{ + return SimpleContext(*this).run(); +} + +YOSYS_NAMESPACE_END diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc deleted file mode 100644 index 5ca955c67..000000000 --- a/passes/opt/opt_dff.cc +++ /dev/null @@ -1,1678 +0,0 @@ -/* - * yosys -- Yosys Open SYnthesis Suite - * - * Copyright (C) 2012 Claire Xenia Wolf - * Copyright (C) 2020 Marcelina Kościelnicka - * - * 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. - * - */ - -#include "kernel/log.h" -#include "kernel/register.h" -#include "kernel/rtlil.h" -#include "kernel/qcsat.h" -#include "kernel/modtools.h" -#include "kernel/sigtools.h" -#include "kernel/ffinit.h" -#include "kernel/ff.h" -#include "kernel/pattern.h" -#include "passes/techmap/simplemap.h" -#include -#include - -USING_YOSYS_NAMESPACE -PRIVATE_NAMESPACE_BEGIN - -struct OptDffOptions -{ - bool nosdff; - bool nodffe; - bool simple_dffe; - bool sat; - bool keepdc; -}; - -// Bit-parallel random simulation used as a cheap pre-filter for equivalence -struct BitSim { - Module *module; - SigMap &sigmap; - ModWalker &modwalker; - dict sim_vals; - uint64_t rng_state; - int max_depth; - int evals_left; - - BitSim(Module *m, SigMap &sm, ModWalker &mw) - : module(m), sigmap(sm), modwalker(mw), rng_state(1337) - { - max_depth = module->design->scratchpad_get_int("opt_dff.sim_depth", 10000); - evals_left = module->design->scratchpad_get_int("opt_dff.sim_evals", 1000000); - } - - uint64_t next_rand() { - uint32_t lo = mkhash_xorshift((uint32_t)rng_state); - uint32_t hi = mkhash_xorshift((uint32_t)(rng_state >> 32) ^ lo); - rng_state = ((uint64_t)hi << 32) | lo; - return rng_state; - } - - uint64_t eval_bit(SigBit b, int depth = 0) { - SigBit mapped = sigmap(b); - if (mapped == State::S0) return 0ULL; - if (mapped == State::S1) return ~0ULL; - if (mapped == State::Sx || mapped == State::Sz) return 0ULL; - - auto it = sim_vals.find(mapped); - if (it != sim_vals.end()) return it->second; - - // Failsafe for huge designs - if (depth >= max_depth || evals_left <= 0) { - uint64_t r = next_rand(); - sim_vals[mapped] = r; - return r; - } - evals_left--; - - sim_vals[mapped] = 0; - uint64_t res = 0; - - if (!modwalker.has_drivers(mapped)) { - res = next_rand(); - } else { - auto &drivers = modwalker.signal_drivers[mapped]; - if (drivers.empty()) { - res = next_rand(); - } else { - auto driver = *drivers.begin(); - Cell *cell = driver.cell; - - if (cell->is_builtin_ff()) { - res = next_rand(); - } else if (cell->type == ID($_AND_)) { - res = eval_bit(cell->getPort(ID::A)[0], depth+1) & eval_bit(cell->getPort(ID::B)[0], depth+1); - } else if (cell->type == ID($_OR_)) { - res = eval_bit(cell->getPort(ID::A)[0], depth+1) | eval_bit(cell->getPort(ID::B)[0], depth+1); - } else if (cell->type == ID($_XOR_)) { - res = eval_bit(cell->getPort(ID::A)[0], depth+1) ^ eval_bit(cell->getPort(ID::B)[0], depth+1); - } else if (cell->type == ID($_NOT_)) { - res = ~eval_bit(cell->getPort(ID::A)[0], depth+1); - } else if (cell->type == ID($_MUX_)) { - uint64_t s = eval_bit(cell->getPort(ID::S)[0], depth+1); - uint64_t a = eval_bit(cell->getPort(ID::A)[0], depth+1); - uint64_t b = eval_bit(cell->getPort(ID::B)[0], depth+1); - res = (a & ~s) | (b & s); - } else if (cell->type == ID($mux)) { - uint64_t s = eval_bit(cell->getPort(ID::S)[0], depth+1); - uint64_t a = eval_bit(cell->getPort(ID::A)[driver.offset], depth+1); - uint64_t b = eval_bit(cell->getPort(ID::B)[driver.offset], depth+1); - res = (a & ~s) | (b & s); - } else { - res = next_rand(); - } - } - } - - sim_vals[mapped] = res; - return res; - } -}; - -struct OptDffWorker -{ - const OptDffOptions &opt; - Module *module; - - // Cell to port bit index - typedef std::pair cell_int_t; - - SigMap sigmap; // Signal aliasing - FfInitVals initvals; - dict bitusers; // Signal sink count - dict bit2mux; // Signal bit to driving MUX - - std::vector dff_cells; - - // opt_dff -sat rebuilds the solver in batches of at most this many imported - // cells, so one pathological module can't grow a single giant solver - static constexpr int sat_batch_cells = 10000; - - SatEffortBudget sat_budget; - bool sat_warned = false; - - // modwalker is expensive to build, so share one lazily between constbits and eqbits - std::unique_ptr modwalker_ptr; - - ModWalker &get_modwalker() - { - if (!modwalker_ptr) - modwalker_ptr = std::make_unique(module->design, module); - return *modwalker_ptr; - } - - bool warn_if_budget_spent() - { - if (!sat_budget.spent()) - return false; - if (!sat_warned) - log_warning("opt_dff -sat: solver effort budget for module %s is exhausted, leaving the " - "remaining FFs un-optimized. Raise or clear the limit with the scratchpad " - "option 'opt_dff.sat_effort' (0 disables it).\n", log_id(module)); - sat_warned = true; - return true; - } - - bool is_active(SigBit sig, bool pol) const { - return sig == (pol ? State::S1 : State::S0); - } - - bool is_inactive(SigBit sig, bool pol) const { - return sig == (pol ? State::S0 : State::S1); - } - - bool is_always_active(SigBit sig, bool pol) const { - return is_active(sig, pol) || (!opt.keepdc && sig == State::Sx); - } - - bool is_always_inactive(SigBit sig, bool pol) const { - return is_inactive(sig, pol) || (!opt.keepdc && sig == State::Sx); - } - - SigSpec create_not(SigSpec a, bool is_fine) { - if (is_fine) - return module->NotGate(NEW_ID, a); - else - return module->Not(NEW_ID, a); - } - - SigSpec create_and(SigSpec a, SigSpec b, bool is_fine) { - if (is_fine) - return module->AndGate(NEW_ID, a, b); - else - return module->And(NEW_ID, a, b); - } - - void create_mux_to_output(SigSpec a, SigSpec b, SigSpec sel, SigSpec y, bool pol, bool is_fine) { - if (is_fine) { - if (pol) - module->addMuxGate(NEW_ID, a, b, sel, y); - else - module->addMuxGate(NEW_ID, b, a, sel, y); - } else { - if (pol) - module->addMux(NEW_ID, a, b, sel, y); - else - module->addMux(NEW_ID, b, a, sel, y); - } - } - - void maybe_simplemap(Cell *c, bool make_gates) { - if (make_gates) { - simplemap(module, c); - module->remove(c); - } - } - - OptDffWorker(const OptDffOptions &opt, Module *mod) - : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod) - { - sat_budget = SatEffortBudget(module->design->scratchpad_get_int("opt_dff.sat_effort", 1000000000)); - - // Gathering two kinds of information here for every sigmapped SigBit: - // - bitusers: how many users it has (muxes will only be merged into FFs if the FF is the only user) - // - bit2mux: the mux cell and bit index that drives it, if any - - for (auto wire : module->wires()) - if (wire->port_output) - for (auto bit : sigmap(wire)) - bitusers[bit]++; - - for (auto cell : module->cells()) { - if (cell->type.in(ID($mux), ID($pmux), ID($_MUX_))) { - RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y)); - for (int i = 0; i < GetSize(sig_y); i++) - bit2mux[sig_y[i]] = cell_int_t(cell, i); - } - - for (auto conn : cell->connections()) { - bool is_output = cell->output(conn.first); - if (!is_output || !cell->known()) - for (auto bit : sigmap(conn.second)) - bitusers[bit]++; - } - - if (module->design->selected(module, cell) && cell->is_builtin_ff()) - dff_cells.push_back(cell); - } - } - - State combine_const(State a, State b) { - // Combine constants: returns Sm if values conflict - if (a == State::Sx && !opt.keepdc) return b; - if (b == State::Sx && !opt.keepdc) return a; - if (a == b) return a; - return State::Sm; - } - - patterns_t find_muxtree_feedback_patterns(RTLIL::SigBit d, RTLIL::SigBit q, pattern_t path) - { - // Find feedback paths D->Q through mux tree, replacing found paths with Sx - patterns_t ret; - - if (d == q) { - ret.insert(path); - return ret; // Feedback found - } - - if (bit2mux.count(d) == 0 || bitusers[d] > 1) - return ret; // D not driven by MUX / MUX drives multiple loads - - cell_int_t mbit = bit2mux.at(d); - RTLIL::SigSpec sig_a = sigmap(mbit.first->getPort(ID::A)); - RTLIL::SigSpec sig_b = sigmap(mbit.first->getPort(ID::B)); - RTLIL::SigSpec sig_s = sigmap(mbit.first->getPort(ID::S)); - int width = GetSize(sig_a), index = mbit.second; - - // Traverse MUX tree - for (int i = 0; i < GetSize(sig_s); i++) { - if (path.count(sig_s[i]) && path.at(sig_s[i])) { - ret = find_muxtree_feedback_patterns(sig_b[i*width + index], q, path); - if (sig_b[i*width + index] == q) { - RTLIL::SigSpec s = mbit.first->getPort(ID::B); - s[i*width + index] = RTLIL::Sx; - mbit.first->setPort(ID::B, s); - } - - return ret; - } - } - - // Specific path wasn't forced, explore the 0 branch - pattern_t path_else = path; - for (int i = 0; i < GetSize(sig_s); i++) { - if (path.count(sig_s[i])) - continue; - - pattern_t path_this = path; - path_else[sig_s[i]] = false; // Assume S=0 for 'else' path - path_this[sig_s[i]] = true; // Assume S=1 for 'this' path - - // Selected when S=1 - for (auto &pat : find_muxtree_feedback_patterns(sig_b[i*width + index], q, path_this)) - ret.insert(pat); - - if (sig_b[i*width + index] == q) { - RTLIL::SigSpec s = mbit.first->getPort(ID::B); - s[i*width + index] = RTLIL::Sx; - mbit.first->setPort(ID::B, s); - } - } - - // Selected when S=0 - for (auto &pat : find_muxtree_feedback_patterns(sig_a[index], q, path_else)) - ret.insert(pat); - - if (sig_a[index] == q) { - RTLIL::SigSpec s = mbit.first->getPort(ID::A); - s[index] = RTLIL::Sx; - mbit.first->setPort(ID::A, s); - } - - return ret; - } - - ctrl_t make_patterns_logic(const patterns_t &patterns, const ctrls_t &ctrls, bool make_gates) - { - if (patterns.empty() && GetSize(ctrls) == 1) - return *ctrls.begin(); - - RTLIL::SigSpec or_input; - - // Build logic for each feedback pattern - for (auto pat : patterns) { - RTLIL::SigSpec s1, s2; - - for (auto it : pat) { - s1.append(it.first); - s2.append(it.second); - } - - RTLIL::SigSpec y = module->addWire(NEW_ID); - RTLIL::Cell *c = module->addNe(NEW_ID, s1, s2, y); - maybe_simplemap(c, make_gates); - or_input.append(y); - } - - // Add existing control signals - for (auto item : ctrls) { - if (item.second) - or_input.append(item.first); - else - or_input.append(create_not(item.first, make_gates)); - } - - if (GetSize(or_input) == 0) return ctrl_t(State::S1, true); - if (GetSize(or_input) == 1) return ctrl_t(or_input, true); - - RTLIL::SigSpec y = module->addWire(NEW_ID); - RTLIL::Cell *c = module->addReduceAnd(NEW_ID, or_input, y); - maybe_simplemap(c, make_gates); - return ctrl_t(y, true); - } - - ctrl_t combine_resets(const ctrls_t &ctrls, bool make_gates) - { - if (GetSize(ctrls) == 1) - return *ctrls.begin(); - - bool final_pol = false; - for (auto item : ctrls) - if (item.second) - final_pol = true; - - RTLIL::SigSpec or_input; - for (auto item : ctrls) { - if (item.second == final_pol) - or_input.append(item.first); - else - or_input.append(create_not(item.first, make_gates)); - } - - RTLIL::SigSpec y = module->addWire(NEW_ID); - RTLIL::Cell *c = final_pol - ? module->addReduceOr(NEW_ID, or_input, y) - : module->addReduceAnd(NEW_ID, or_input, y); - maybe_simplemap(c, make_gates); - return ctrl_t(y, final_pol); - } - - bool signal_all_same(const SigSpec &sig) { - for (int i = 1; i < GetSize(sig); i++) - if (sig[i] != sig[0]) - return false; - return true; - } - - bool optimize_sr(FfData &ff, Cell *cell, bool &changed) - { - // Removes SR if CLR/SET are always active - // Converts SR to ARST if one pin is never active - // Converts SR to ARST if SET/CLR are inverses of eachother - bool sr_removed = false; - std::vector keep_bits; - - // Check for constant Set/Clear inputs - for (int i = 0; i < ff.width; i++) { - if (is_always_active(ff.sig_clr[i], ff.pol_clr)) { - initvals.remove_init(ff.sig_q[i]); - module->connect(ff.sig_q[i], State::S0); - log("Handling always-active CLR at position %d on %s (%s) from module %s (changing to const driver).\n", - i, cell, cell->type.unescape(), module); - sr_removed = true; - } else if (is_always_active(ff.sig_set[i], ff.pol_set)) { - initvals.remove_init(ff.sig_q[i]); - if (!ff.pol_clr) - module->connect(ff.sig_q[i], ff.sig_clr[i]); - else if (ff.is_fine) - module->addNotGate(NEW_ID, ff.sig_clr[i], ff.sig_q[i]); - else - module->addNot(NEW_ID, ff.sig_clr[i], ff.sig_q[i]); - log("Handling always-active SET at position %d on %s (%s) from module %s (changing to combinatorial circuit).\n", - i, cell, cell->type.unescape(), module); - sr_removed = true; - } else { - keep_bits.push_back(i); - } - } - - if (sr_removed) { - if (keep_bits.empty()) { - module->remove(cell); - return true; // FF fully removed - } - ff = ff.slice(keep_bits); - ff.cell = cell; - changed = true; - } - - // Try SR -> ARST conversion - bool clr_inactive = ff.pol_clr ? ff.sig_clr.is_fully_zero() : ff.sig_clr.is_fully_ones(); - bool set_inactive = ff.pol_set ? ff.sig_set.is_fully_zero() : ff.sig_set.is_fully_ones(); - - if (clr_inactive && signal_all_same(ff.sig_set)) { - log("Removing never-active CLR on %s (%s) from module %s.\n", - cell, cell->type.unescape(), module); - ff.has_sr = false; - ff.has_arst = true; - ff.pol_arst = ff.pol_set; - ff.sig_arst = ff.sig_set[0]; - ff.val_arst = Const(State::S1, ff.width); - changed = true; - } else if (set_inactive && signal_all_same(ff.sig_clr)) { - log("Removing never-active SET on %s (%s) from module %s.\n", - cell, cell->type.unescape(), module); - ff.has_sr = false; - ff.has_arst = true; - ff.pol_arst = ff.pol_clr; - ff.sig_arst = ff.sig_clr[0]; - ff.val_arst = Const(State::S0, ff.width); - changed = true; - } else if (ff.pol_clr == ff.pol_set) { - State val_neutral = ff.pol_set ? State::S0 : State::S1; - SigBit sig_arst = (ff.sig_clr[0] == val_neutral) ? ff.sig_set[0] : ff.sig_clr[0]; - - bool failed = false; - Const::Builder val_arst_builder(ff.width); - for (int i = 0; i < ff.width; i++) { - if (ff.sig_clr[i] == sig_arst && ff.sig_set[i] == val_neutral) - val_arst_builder.push_back(State::S0); - else if (ff.sig_set[i] == sig_arst && ff.sig_clr[i] == val_neutral) - val_arst_builder.push_back(State::S1); - else { - failed = true; - break; - } - } - - if (!failed) { - log("Converting CLR/SET to ARST on %s (%s) from module %s.\n", - cell, cell->type.unescape(), module); - ff.has_sr = false; - ff.has_arst = true; - ff.val_arst = val_arst_builder.build(); - ff.sig_arst = sig_arst; - ff.pol_arst = ff.pol_clr; - changed = true; - } - } - - return false; - } - - bool optimize_aload(FfData &ff, Cell *cell, bool &changed) - { - // Removes unused Async Load - // Converts constant Async Load to ARST - if (is_always_inactive(ff.sig_aload, ff.pol_aload)) { - log("Removing never-active async load on %s (%s) from module %s.\n", - cell, cell->type.unescape(), module); - ff.has_aload = false; - changed = true; - return false; - } - - if (is_active(ff.sig_aload, ff.pol_aload)) { - // ALOAD always active - log("Handling always-active async load on %s (%s) from module %s (changing to combinatorial circuit).\n", - cell, cell->type.unescape(), module); - ff.remove(); - - if (ff.has_sr) { - SigSpec tmp; - if (ff.is_fine) { - tmp = ff.pol_set - ? module->MuxGate(NEW_ID, ff.sig_ad, State::S1, ff.sig_set) - : module->MuxGate(NEW_ID, State::S1, ff.sig_ad, ff.sig_set); - - if (ff.pol_clr) - module->addMuxGate(NEW_ID, tmp, State::S0, ff.sig_clr, ff.sig_q); - else - module->addMuxGate(NEW_ID, State::S0, tmp, ff.sig_clr, ff.sig_q); - } else { - tmp = ff.pol_set - ? module->Or(NEW_ID, ff.sig_ad, ff.sig_set) - : module->Or(NEW_ID, ff.sig_ad, module->Not(NEW_ID, ff.sig_set)); - - if (ff.pol_clr) - module->addAnd(NEW_ID, tmp, module->Not(NEW_ID, ff.sig_clr), ff.sig_q); - else - module->addAnd(NEW_ID, tmp, ff.sig_clr, ff.sig_q); - } - } else if (ff.has_arst) { - create_mux_to_output(ff.sig_ad, ff.val_arst, ff.sig_arst, ff.sig_q, ff.pol_arst, ff.is_fine); - } else { - module->connect(ff.sig_q, ff.sig_ad); - } - return true; - } - - // AD is constant -> ARST - if (ff.sig_ad.is_fully_const() && !ff.has_arst && !ff.has_sr) { - log("Changing const-value async load to async reset on %s (%s) from module %s.\n", - cell, cell->type.unescape(), module); - ff.has_arst = true; - ff.has_aload = false; - ff.sig_arst = ff.sig_aload; - ff.pol_arst = ff.pol_aload; - ff.val_arst = ff.sig_ad.as_const(); - changed = true; - } - - return false; - } - - bool optimize_arst(FfData &ff, Cell *cell, bool &changed) - { - // Removes ARST if never active or replaces FF if always active - if (is_inactive(ff.sig_arst, ff.pol_arst)) { - log("Removing never-active ARST on %s (%s) from module %s.\n", - cell, cell->type.unescape(), module); - ff.has_arst = false; - changed = true; - } else if (is_always_active(ff.sig_arst, ff.pol_arst)) { - log("Handling always-active ARST on %s (%s) from module %s (changing to const driver).\n", - cell, cell->type.unescape(), module); - ff.remove(); - module->connect(ff.sig_q, ff.val_arst); - return true; - } - - return false; - } - - void optimize_srst(FfData &ff, Cell *cell, bool &changed) - { - // Removes SRST if never active or forces D to reset value if always active - if (is_inactive(ff.sig_srst, ff.pol_srst)) { - log("Removing never-active SRST on %s (%s) from module %s.\n", - cell, cell->type.unescape(), module); - ff.has_srst = false; - changed = true; - } else if (is_always_active(ff.sig_srst, ff.pol_srst)) { - log("Handling always-active SRST on %s (%s) from module %s (changing to const D).\n", - cell, cell->type.unescape(), module); - ff.has_srst = false; - if (!ff.ce_over_srst) - ff.has_ce = false; - - ff.sig_d = ff.val_srst; - changed = true; - } - } - - void optimize_ce(FfData &ff, Cell *cell, bool &changed) - { - if (is_always_inactive(ff.sig_ce, ff.pol_ce)) { - if (ff.has_srst && !ff.ce_over_srst) { - log("Handling never-active EN on %s (%s) from module %s (connecting SRST instead).\n", - cell, cell->type.unescape(), module); - ff.pol_ce = ff.pol_srst; - ff.sig_ce = ff.sig_srst; - ff.has_srst = false; - ff.sig_d = ff.val_srst; - changed = true; - } else if (!opt.keepdc || ff.val_init.is_fully_def()) { - log("Handling never-active EN on %s (%s) from module %s (removing D path).\n", - cell, cell->type.unescape(), module); - ff.has_ce = ff.has_clk = ff.has_srst = false; - changed = true; - } else { - ff.sig_d = ff.sig_q; - ff.has_ce = ff.has_srst = false; - changed = true; - } - } else if (is_active(ff.sig_ce, ff.pol_ce)) { - log("Removing always-active EN on %s (%s) from module %s.\n", - cell, cell->type.unescape(), module); - ff.has_ce = false; - changed = true; - } - } - - void optimize_const_clk(FfData &ff, Cell *cell, bool &changed) - { - if (!opt.keepdc || ff.val_init.is_fully_def()) { - log("Handling const CLK on %s (%s) from module %s (removing D path).\n", - cell, cell->type.unescape(), module); - ff.has_ce = ff.has_clk = ff.has_srst = false; - changed = true; - } else if (ff.has_ce || ff.has_srst || ff.sig_d != ff.sig_q) { - ff.sig_d = ff.sig_q; - ff.has_ce = ff.has_srst = false; - changed = true; - } - } - - void optimize_d_equals_q(FfData &ff, Cell *cell, bool &changed) - { - // Detect feedback loops where D is hardwired to Q - if (ff.has_clk && ff.has_srst) { - log("Handling D = Q on %s (%s) from module %s (conecting SRST instead).\n", - cell, cell->type.unescape(), module); - if (ff.has_ce && ff.ce_over_srst) { - SigSpec ce = ff.pol_ce ? ff.sig_ce : create_not(ff.sig_ce, ff.is_fine); - SigSpec srst = ff.pol_srst ? ff.sig_srst : create_not(ff.sig_srst, ff.is_fine); - ff.sig_ce = create_and(ce, srst, ff.is_fine); - ff.pol_ce = true; - } else { - ff.pol_ce = ff.pol_srst; - ff.sig_ce = ff.sig_srst; - } - - ff.has_ce = true; - ff.has_srst = false; - ff.sig_d = ff.val_srst; - changed = true; - } else if (!opt.keepdc || ff.val_init.is_fully_def()) { - log("Handling D = Q on %s (%s) from module %s (removing D path).\n", - cell, cell->type.unescape(), module); - ff.has_gclk = ff.has_clk = ff.has_ce = false; - changed = true; - } - } - - bool try_merge_srst(FfData &ff, Cell *cell, bool &changed) - { - std::map> groups; - std::vector remaining_indices; - Const::Builder val_srst_builder(ff.width); - - for (int i = 0; i < ff.width; i++) { - ctrls_t resets; - State reset_val = ff.has_srst ? ff.val_srst[i] : State::Sx; - - while (bit2mux.count(ff.sig_d[i]) && bitusers[ff.sig_d[i]] == 1) { - cell_int_t mbit = bit2mux.at(ff.sig_d[i]); - if (GetSize(mbit.first->getPort(ID::S)) != 1) - break; - - SigBit s = mbit.first->getPort(ID::S); - SigBit a = mbit.first->getPort(ID::A)[mbit.second]; - SigBit b = mbit.first->getPort(ID::B)[mbit.second]; - - if ((a == State::S0 || a == State::S1) && (b == State::S0 || b == State::S1)) - break; - - bool b_const = (b == State::S0 || b == State::S1); - bool a_const = (a == State::S0 || a == State::S1); - - if (b_const && (b == reset_val || reset_val == State::Sx) && a != ff.sig_q[i]) { - reset_val = b.data; - resets.insert(ctrl_t(s, true)); - ff.sig_d[i] = a; - } else if (a_const && (a == reset_val || reset_val == State::Sx) && b != ff.sig_q[i]) { - reset_val = a.data; - resets.insert(ctrl_t(s, false)); - ff.sig_d[i] = b; - } else { - break; - } - } - - if (!resets.empty()) { - if (ff.has_srst) - resets.insert(ctrl_t(ff.sig_srst, ff.pol_srst)); - - groups[resets].push_back(i); - } else { - remaining_indices.push_back(i); - } - - val_srst_builder.push_back(reset_val); - } - - Const val_srst = val_srst_builder.build(); - - for (auto &it : groups) { - FfData new_ff = ff.slice(it.second); - Const::Builder new_val_srst_builder(new_ff.width); - for (int i = 0; i < new_ff.width; i++) - new_val_srst_builder.push_back(val_srst[it.second[i]]); - - new_ff.val_srst = new_val_srst_builder.build(); - - ctrl_t srst = combine_resets(it.first, ff.is_fine); - new_ff.has_srst = true; - new_ff.sig_srst = srst.first; - new_ff.pol_srst = srst.second; - if (new_ff.has_ce) - new_ff.ce_over_srst = true; - - Cell *new_cell = new_ff.emit(); - if (new_cell) - dff_cells.push_back(new_cell); - - log("Adding SRST signal on %s (%s) from module %s (D = %s, Q = %s, rval = %s).\n", - cell, cell->type.unescape(), module, - log_signal(new_ff.sig_d), log_signal(new_ff.sig_q), log_signal(new_ff.val_srst)); - } - - if (remaining_indices.empty()) { - module->remove(cell); - return true; - } - - if (GetSize(remaining_indices) != ff.width) { - ff = ff.slice(remaining_indices); - ff.cell = cell; - changed = true; - } - - return false; - } - - bool try_merge_ce(FfData &ff, Cell *cell, bool &changed) - { - std::map, std::vector> groups; - std::vector remaining_indices; - - for (int i = 0; i < ff.width; i++) { - ctrls_t enables; - - while (bit2mux.count(ff.sig_d[i]) && bitusers[ff.sig_d[i]] == 1) { - cell_int_t mbit = bit2mux.at(ff.sig_d[i]); - if (GetSize(mbit.first->getPort(ID::S)) != 1) - break; - - SigBit s = mbit.first->getPort(ID::S); - SigBit a = mbit.first->getPort(ID::A)[mbit.second]; - SigBit b = mbit.first->getPort(ID::B)[mbit.second]; - - if (a == ff.sig_q[i]) { - enables.insert(ctrl_t(s, true)); - ff.sig_d[i] = b; - } else if (b == ff.sig_q[i]) { - enables.insert(ctrl_t(s, false)); - ff.sig_d[i] = a; - } else { - break; - } - } - - patterns_t patterns; - if (!opt.simple_dffe) - patterns = find_muxtree_feedback_patterns(ff.sig_d[i], ff.sig_q[i], pattern_t()); - - if (!patterns.empty() || !enables.empty()) { - if (ff.has_ce) - enables.insert(ctrl_t(ff.sig_ce, ff.pol_ce)); - simplify_patterns(patterns); - groups[std::make_pair(patterns, enables)].push_back(i); - } else { - remaining_indices.push_back(i); - } - } - - for (auto &it : groups) { - FfData new_ff = ff.slice(it.second); - ctrl_t en = make_patterns_logic(it.first.first, it.first.second, ff.is_fine); - - new_ff.has_ce = true; - new_ff.sig_ce = en.first; - new_ff.pol_ce = en.second; - new_ff.ce_over_srst = false; - - Cell *new_cell = new_ff.emit(); - if (new_cell) - dff_cells.push_back(new_cell); - - log("Adding EN signal on %s (%s) from module %s (D = %s, Q = %s).\n", - cell, cell->type.unescape(), module, - log_signal(new_ff.sig_d), log_signal(new_ff.sig_q)); - } - - if (remaining_indices.empty()) { - module->remove(cell); - return true; - } - - if (GetSize(remaining_indices) != ff.width) { - ff = ff.slice(remaining_indices); - ff.cell = cell; - changed = true; - } - - return false; - } - - bool run() - { - bool did_something = false; - - while (!dff_cells.empty()) { - Cell *cell = dff_cells.back(); - dff_cells.pop_back(); - - FfData ff(&initvals, cell); - bool changed = false; - - if (!ff.width) { - ff.remove(); - did_something = true; - continue; - } - - // Async control signal opt - if (ff.has_sr && optimize_sr(ff, cell, changed)) { - did_something = true; - continue; - } - - if (ff.has_aload && optimize_aload(ff, cell, changed)) { - did_something = true; - continue; - } - - if (ff.has_arst && optimize_arst(ff, cell, changed)) { - did_something = true; - continue; - } - - // Sync control signal opt - if (ff.has_srst) - optimize_srst(ff, cell, changed); - - if (ff.has_ce) - optimize_ce(ff, cell, changed); - - if (ff.has_clk && ff.sig_clk.is_fully_const()) - optimize_const_clk(ff, cell, changed); - - // Feedback (D=Q) opt - if ((ff.has_clk || ff.has_gclk) && ff.sig_d == ff.sig_q) - optimize_d_equals_q(ff, cell, changed); - - if (ff.has_aload && !ff.has_clk && ff.sig_ad == ff.sig_q) { - log("Handling AD = Q on %s (%s) from module %s (removing async load path).\n", - cell, cell->type.unescape(), module); - ff.has_aload = false; - changed = true; - } - - // Mux merging - if (ff.has_clk && ff.sig_d != ff.sig_q) { - bool can_merge_srst = !ff.has_arst && !ff.has_sr && - (!ff.has_srst || !ff.has_ce || ff.ce_over_srst) && !opt.nosdff; - - if (can_merge_srst && try_merge_srst(ff, cell, changed)) { - did_something = true; - continue; - } - - bool can_merge_ce = (!ff.has_srst || !ff.has_ce || !ff.ce_over_srst) && !opt.nodffe; - - if (can_merge_ce && try_merge_ce(ff, cell, changed)) { - did_something = true; - continue; - } - } - - if (changed) { - ff.emit(); - did_something = true; - } - } - - return did_something; - } - - State check_constbit(FfData &ff, int i) - { - State val = ff.val_init[i]; - if (ff.has_arst) val = combine_const(val, ff.val_arst[i]); - if (ff.has_srst) val = combine_const(val, ff.val_srst[i]); - if (ff.has_sr) { - if (ff.sig_clr[i] != (ff.pol_clr ? State::S0 : State::S1)) - val = combine_const(val, State::S0); - if (ff.sig_set[i] != (ff.pol_set ? State::S0 : State::S1)) - val = combine_const(val, State::S1); - } - - return val; - } - - // One FF bit whose constness needs SAT proofs; each target is a non-const input (D and/or AD) - // that must be shown eq to val - struct ConstTarget { - SigBit sig; - int lit = -1; - bool proven = false; - }; - - struct ConstObligation { - Cell *cell; - int idx; - State val; - SigBit q; - int q_lit = -1; - bool dropped = false; - std::vector targets; - }; - - void commit_const(dict> &const_bits, Cell *cell, int i, SigBit q, State val) - { - log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n", - val == State::S1 ? 1 : 0, i, cell, cell->type.unescape(), module); - initvals.remove_init(q); - module->connect(q, val); - const_bits[cell].insert(i); - } - - bool add_const_target(ModWalker &modwalker, ConstObligation &ob, SigBit sig) - { - if (!opt.sat || (ob.val != State::S0 && ob.val != State::S1) || !modwalker.has_drivers(sig)) - return false; - ob.targets.push_back(ConstTarget{sig}); - return true; - } - - // Try to decide whether target t of obligation ob is constant, under the given per-query cap. - bool resolve_const_target(QuickConeSat &qcsat, int64_t cap, ConstObligation &ob, ConstTarget &t, - const std::vector &modelExprs, const std::vector &model_obs) - { - // Prove that the next value equals the constant in every state where Q already holds it - int vlit = qcsat.ez->value(ob.val == State::S1); - std::vector assumptions; - assumptions.push_back(qcsat.ez->IFF(ob.q_lit, vlit)); - assumptions.push_back(qcsat.ez->NOT(qcsat.ez->IFF(t.lit, vlit))); - - std::vector modelVals; - // One counterexample can prune many targets - auto res = sat_budget.solve(qcsat, cap, modelExprs, modelVals, assumptions); - - if (res == SatEffortBudget::Result::LimitReached) - return false; // Nothing changed - if (res == SatEffortBudget::Result::Unsat) { - t.proven = true; // t is proven to be const - return true; - } - - // Counterexample: this bit is not constant. Any other pending bit whose Q holds its - // constant while its next value differs is disproven by the same state - for (int k = 0; k < GetSize(model_obs); k++) { - ConstObligation *ob2 = model_obs[k]; - if (ob2->dropped) - continue; - bool want = (ob2->val == State::S1); - bool t_val = modelVals[2*k]; - bool q_val = modelVals[2*k + 1]; - if (q_val == want && t_val != want) - ob2->dropped = true; - } - ob.dropped = true; - return true; - } - - bool run_constbits() - { - // Find FFs that are provably constant - ModWalker &modwalker = get_modwalker(); - - dict> const_bits; - bool did_something = false; - - // fold constant D/AD inputs into the tested value first - // bits whose remaining inputs are wires become SAT proof obligations - std::vector obligations; - - for (auto cell : module->selected_cells()) { - if (!cell->is_builtin_ff()) - continue; - - FfData ff(&initvals, cell); - - for (int i = 0; i < ff.width; i++) { - State val = check_constbit(ff, i); - if (val == State::Sm) - continue; - - // Fold all const inputs first, so the SAT targets are checked against the final const - if ((ff.has_clk || ff.has_gclk) && !ff.sig_d[i].wire) { - val = combine_const(val, ff.sig_d[i].data); - if (val == State::Sm) continue; - } - if (ff.has_aload && !ff.sig_ad[i].wire) { - val = combine_const(val, ff.sig_ad[i].data); - if (val == State::Sm) continue; - } - - ConstObligation ob; - ob.cell = cell; - ob.idx = i; - ob.val = val; - ob.q = ff.sig_q[i]; - - bool feasible = true; - if ((ff.has_clk || ff.has_gclk) && ff.sig_d[i].wire) - feasible = add_const_target(modwalker, ob, ff.sig_d[i]); - if (feasible && ff.has_aload && ff.sig_ad[i].wire) - feasible = add_const_target(modwalker, ob, ff.sig_ad[i]); - if (!feasible) - continue; - - if (ob.targets.empty()) { - commit_const(const_bits, cell, i, ff.sig_q[i], val); - did_something = true; - continue; - } - obligations.push_back(ob); - } - } - - int64_t screen_cap = 0; - if (sat_budget.enabled() && !obligations.empty()) { - // Screening cap, scaled down when the budget cannot afford a full-price screening round - int64_t num_queries = 0; - for (auto &ob : obligations) - num_queries += GetSize(ob.targets); - screen_cap = max((int64_t)20000, min((int64_t)200000, sat_budget.total / (4 * num_queries))); - } - - // Each obligation is proven independently, so processing obligations in - // batches and stopping early on an exhausted budget is safe - for (int batch_begin = 0; batch_begin < GetSize(obligations) && !warn_if_budget_spent(); ) { - QuickConeSat qcsat(modwalker); - int64_t cells_charged = 0; - int batch_end = batch_begin; - - while (batch_end < GetSize(obligations) && !warn_if_budget_spent()) { - if (batch_end > batch_begin && GetSize(qcsat.imported_cells) >= sat_batch_cells) - break; - auto &ob = obligations[batch_end]; - ob.q_lit = qcsat.importSigBit(ob.q); - for (auto &t : ob.targets) - t.lit = qcsat.importSigBit(t.sig); - qcsat.prepare(); - sat_budget.charge_import(qcsat, cells_charged); - batch_end++; - } - - // Sweep the batch under a cheap screening cap, then re-sweep the still-undecided targets - int64_t cap = screen_cap; - bool out_of_budget = false; - - while (!out_of_budget) { - bool all_resolved = true; - - // Counter ex.: every pending target in the batch. Entries that get proven or dropped later - // in the sweep are harmless (a proven bit is constant in every model) - std::vector modelExprs; - std::vector model_obs; - for (int obi = batch_begin; obi < batch_end; obi++) { - auto &ob = obligations[obi]; - if (ob.dropped) - continue; - for (auto &t : ob.targets) - if (!t.proven) { - modelExprs.push_back(t.lit); - modelExprs.push_back(ob.q_lit); - model_obs.push_back(&ob); - } - } - - for (int obi = batch_begin; obi < batch_end && !out_of_budget; obi++) { - auto &ob = obligations[obi]; - if (ob.dropped) - continue; - for (auto &t : ob.targets) { - if (t.proven || ob.dropped) - continue; - if (warn_if_budget_spent()) { - out_of_budget = true; - break; - } - if (!resolve_const_target(qcsat, cap, ob, t, modelExprs, model_obs)) - all_resolved = false; - } - } - - if (out_of_budget || all_resolved) - break; - cap = 0; - } - - batch_begin = batch_end; - } - - for (auto &ob : obligations) { - if (ob.dropped) - continue; - bool all_proven = true; - for (auto &t : ob.targets) - all_proven &= t.proven; - if (all_proven) { - commit_const(const_bits, ob.cell, ob.idx, ob.q, ob.val); - did_something = true; - } - } - - // Reconstruct FF with constant bits removed - std::vector cells_to_remove; - std::vector ffs_to_emit; - - for (auto &kv : const_bits) { - Cell *cell = kv.first; - FfData ff(&initvals, cell); - std::vector keep_bits; - for (int i = 0; i < ff.width; i++) - if (!kv.second.count(i)) - keep_bits.push_back(i); - - if (keep_bits.empty()) { - cells_to_remove.push_back(cell); - } else { - ff = ff.slice(keep_bits); - ff.cell = cell; - ffs_to_emit.push_back(ff); - } - } - - for (auto* cell : cells_to_remove) - module->remove(cell); - - for (auto& ff : ffs_to_emit) - ff.emit(); - - return did_something; - } - - struct EqBit { - Cell *cell; - int idx; - SigBit q; - }; - - // NOTE: This intentionally duplicates a subset of FfData, as flattening just the - // fields that matter for merging into a single comparable/hashable key is cheaper - struct SigKey { - enum Flag : uint16_t { - InitOne = 1u << 0, - InitX = 1u << 1, - PolClk = 1u << 2, - PolCe = 1u << 3, - PolSrst = 1u << 4, - PolArst = 1u << 5, - PolAload = 1u << 6, - PolClr = 1u << 7, - PolSet = 1u << 8, - CeOverSrst = 1u << 9, - }; - - SigBit clk, ce, srst, arst, aload, clr, set; - IdString cell_type; // for SR - uint16_t flags; - - bool operator==(const SigKey &o) const { - return flags == o.flags && clk == o.clk && ce == o.ce && srst == o.srst && arst == o.arst - && aload == o.aload && clr == o.clr && set == o.set && cell_type == o.cell_type; - } - - Hasher hash_into(Hasher h) const { - h.eat(flags); - h.eat(clk); - h.eat(ce); - h.eat(srst); - h.eat(arst); - h.eat(aload); - h.eat(clr); - h.eat(set); - h.eat(cell_type); - return h; - } - }; - - bool is_def(State s) { - // Concrete constant bit (0 or 1), as opposed to x/z - return s == State::S0 || s == State::S1; - } - - std::vector> gather_initial_eq_classes(std::vector &bits, dict &ff_for_cell) - { - std::vector keys; - - // Collect FF bits eligible for merging - for (auto cell : module->selected_cells()) { - if (!cell->is_builtin_ff()) - continue; - - FfData ff(&initvals, cell); - if (!ff.has_clk && !ff.has_gclk) - continue; - - ff_for_cell.emplace(cell, ff); - - for (int i = 0; i < ff.width; i++) { - // Skip bits whose reset value is undefined (x) - if (ff.has_srst && !is_def(ff.val_srst[i])) continue; - if (ff.has_arst && !is_def(ff.val_arst[i])) continue; - - // Class members are assumed equal in the current cycle and proven equal in the next, which needs - // a base case anchoring them to a common known value - bool def_init = is_def(ff.val_init[i]); - if (!def_init && !ff.has_srst && !ff.has_arst) - continue; - - SigKey k = {}; - - // Flags - if (def_init && ff.val_init[i] == State::S1) - k.flags |= SigKey::InitOne; - else if (!def_init) - k.flags |= SigKey::InitX; - - if (ff.has_clk) { - k.clk = ff.sig_clk; - if (ff.pol_clk) k.flags |= SigKey::PolClk; - } - if (ff.has_ce) { - k.ce = ff.sig_ce; - if (ff.pol_ce) k.flags |= SigKey::PolCe; - } - if (ff.has_srst) { - k.srst = ff.sig_srst; - if (ff.pol_srst) k.flags |= SigKey::PolSrst; - if (ff.ce_over_srst) k.flags |= SigKey::CeOverSrst; - } - if (ff.has_arst) { - k.arst = ff.sig_arst; - if (ff.pol_arst) k.flags |= SigKey::PolArst; - } - if (ff.has_aload) { - k.aload = ff.sig_aload; - if (ff.pol_aload) k.flags |= SigKey::PolAload; - } - if (ff.has_sr) { - k.clr = ff.sig_clr[i]; - k.set = ff.sig_set[i]; - k.cell_type = cell->type; - if (ff.pol_clr) k.flags |= SigKey::PolClr; - if (ff.pol_set) k.flags |= SigKey::PolSet; - } - - bits.push_back({cell, i, ff.sig_q[i]}); - keys.push_back(k); - } - } - - dict> buckets; - for (int i = 0; i < GetSize(bits); i++) - buckets[keys[i]].push_back(i); - - std::vector> classes; - for (auto &kv : buckets) - if (GetSize(kv.second) >= 2) - classes.push_back(std::move(kv.second)); - - return classes; - } - - std::vector> filter_classes_sim( - const std::vector> &classes, - const std::vector &bits, - const dict &ff_for_cell, - ModWalker &modwalker - ) { - BitSim sim(module, sigmap, modwalker); - - // Assume same class - for (auto &cls : classes) { - uint64_t class_q_val = sim.next_rand(); - for (int idx : cls) { - sim.sim_vals[sigmap(bits[idx].q)] = class_q_val; - } - } - - std::vector> refined_classes; - for (auto &cls : classes) { - dict> sim_buckets; - for (int idx : cls) { - const EqBit &eb = bits[idx]; - const FfData &ff = ff_for_cell.at(eb.cell); - uint64_t n_val = sim.eval_bit(ff.sig_d[eb.idx]); - - if (ff.has_aload) { - uint64_t al = sim.eval_bit(ff.sig_aload); - if (!ff.pol_aload) al = ~al; - uint64_t ad = sim.eval_bit(ff.sig_ad[eb.idx]); - n_val = (n_val & ~al) | (ad & al); - } - if (ff.has_arst) { - uint64_t ar = sim.eval_bit(ff.sig_arst); - if (!ff.pol_arst) ar = ~ar; - uint64_t ar_val = (ff.val_arst[eb.idx] == State::S1) ? ~0ULL : 0ULL; - n_val = (n_val & ~ar) | (ar_val & ar); - } - if (ff.has_sr) { - uint64_t clr = sim.eval_bit(ff.sig_clr[eb.idx]); - if (!ff.pol_clr) clr = ~clr; - uint64_t set = sim.eval_bit(ff.sig_set[eb.idx]); - if (!ff.pol_set) set = ~set; - n_val = ~clr & (set | n_val); - } - if (ff.has_srst) { - uint64_t srst = sim.eval_bit(ff.sig_srst); - if (!ff.pol_srst) srst = ~srst; - uint64_t srst_val = (ff.val_srst[eb.idx] == State::S1) ? ~0ULL : 0ULL; - n_val = (n_val & ~srst) | (srst_val & srst); - } - - sim_buckets[n_val].push_back(idx); - } - - for (auto &kv : sim_buckets) - if (GetSize(kv.second) >= 2) - refined_classes.push_back(std::move(kv.second)); - } - - return refined_classes; - } - - std::vector> drop_all_classes() - { - log("opt_dff -sat: skipping all equivalent-flip-flop merges in module %s (solver effort budget " - "exhausted before the equivalences could be proven).\n", log_id(module)); - return {}; - } - - std::vector> filter_classes_sat( - std::vector> classes, - const std::vector &bits, - const dict &ff_for_cell, - ModWalker &modwalker - ) { - QuickConeSat qcsat(modwalker); - std::vector q_lit(bits.size(), -1); - std::vector n_lit(bits.size(), -1); - - // Build the next-state function n_lit[idx] of every candidate bit by - // folding the FF's control logic on top of the D input (-> next value) - int64_t cells_charged = 0; - - // Two bits are equivalent if their next states always agree whenever their - // current states (and those of every other candidate pair) agree - for (auto &cls : classes) { - if (warn_if_budget_spent()) - return drop_all_classes(); - for (int idx : cls) { - const EqBit &eb = bits[idx]; - const FfData &ff = ff_for_cell.at(eb.cell); - q_lit[idx] = qcsat.importSigBit(eb.q); - int n = qcsat.importSigBit(ff.sig_d[eb.idx]); - - if (ff.has_aload) { - int al = qcsat.importSigBit(ff.sig_aload); - if (!ff.pol_aload) al = qcsat.ez->NOT(al); - n = qcsat.ez->ITE(al, qcsat.importSigBit(ff.sig_ad[eb.idx]), n); - } - if (ff.has_arst) { - int ar = qcsat.importSigBit(ff.sig_arst); - if (!ff.pol_arst) ar = qcsat.ez->NOT(ar); - n = qcsat.ez->ITE(ar, qcsat.ez->value(ff.val_arst[eb.idx] == State::S1), n); - } - if (ff.has_sr) { - int clr = qcsat.importSigBit(ff.sig_clr[eb.idx]); - if (!ff.pol_clr) clr = qcsat.ez->NOT(clr); - int set = qcsat.importSigBit(ff.sig_set[eb.idx]); - if (!ff.pol_set) set = qcsat.ez->NOT(set); - n = qcsat.ez->AND(qcsat.ez->NOT(clr), qcsat.ez->OR(set, n)); - } - if (ff.has_srst) { - int srst = qcsat.importSigBit(ff.sig_srst); - if (!ff.pol_srst) srst = qcsat.ez->NOT(srst); - n = qcsat.ez->ITE(srst, qcsat.ez->value(ff.val_srst[eb.idx] == State::S1), n); - } - - n_lit[idx] = n; - } - qcsat.prepare(); - sat_budget.charge_import(qcsat, cells_charged); - } - - // Assume the induction hypo (that every current class is internally equal in the present cycle), and try - // to prove that the members of each class therefore also agree in the next cycle - - // A class survives only if no counterexample exists under that hypo, so combined with the common init/reset - // value that every class shares, this makes the equality an inductive invariant -> bits are eq and safe to merge - std::vector worklist; - std::vector in_worklist(GetSize(classes), true); - - for (int i = 0; i < GetSize(classes); i++) - worklist.push_back(i); - - while (!worklist.empty()) { - int cls_idx = worklist.back(); - worklist.pop_back(); - in_worklist[cls_idx] = false; - - auto &cls = classes[cls_idx]; - if (GetSize(cls) < 2) continue; - - // Induction hypo: assume every candidate class is equal - std::vector assumptions; - for (auto &c : classes) { - if (GetSize(c) < 2) continue; - int rep = c[0]; - for (int k = 1; k < GetSize(c); k++) - assumptions.push_back(qcsat.ez->IFF(q_lit[rep], q_lit[c[k]])); - } - - // Scan the class members against the representative and issue a query per pair, - // stopping early at the first counterexample, which is reused to split the entire - // class at once - int rep = cls[0]; - for (int i = 1; i < GetSize(cls); i++) { - if (n_lit[rep] == n_lit[cls[i]]) - continue; - - if (warn_if_budget_spent()) - return drop_all_classes(); - - // Can the next state of the rep and this member ever differ? - int query = qcsat.ez->XOR(n_lit[rep], n_lit[cls[i]]); - // Capture every member's next-state value in that model so one counterexample - // partitions the whole class - std::vector modelExprs; - for (int b : cls) - modelExprs.push_back(n_lit[b]); - - std::vector modelVals; - assumptions.push_back(query); - - auto res = sat_budget.solve(qcsat, 0, modelExprs, modelVals, assumptions); - - if (res == SatEffortBudget::Result::LimitReached) { - warn_if_budget_spent(); - return drop_all_classes(); - } - - if (res == SatEffortBudget::Result::Sat) { - // SAT -> partition entire class - std::vector sub0; - std::vector sub1; - - for (size_t b_idx = 0; b_idx < cls.size(); b_idx++) { - if (modelVals[b_idx]) - sub1.push_back(cls[b_idx]); - else - sub0.push_back(cls[b_idx]); - } - - classes[cls_idx] = std::move(sub0); - classes.push_back(std::move(sub1)); - in_worklist.push_back(false); - - // Partition was split -> the induction hypo weakened - for (int j = 0; j < GetSize(classes); j++) { - if (GetSize(classes[j]) >= 2 && !in_worklist[j]) { - worklist.push_back(j); - in_worklist[j] = true; - } - } - - break; // Process new splits - } - - assumptions.pop_back(); // Remove query for the next pairwise check if UNSAT - } - } - - return classes; - } - - bool apply_eq_merges(const std::vector> &classes, const std::vector &bits, dict &ff_for_cell) - { - bool any_change = false; - dict> remove_bits; - - // Drive every non-rep Q from its class rep, drop merged bits from their FFs - for (auto &cls : classes) { - if (GetSize(cls) < 2) - continue; - SigBit rep_q = bits[cls[0]].q; - any_change = true; - for (int k = 1; k < GetSize(cls); k++) { - const EqBit &eb = bits[cls[k]]; - initvals.remove_init(eb.q); - module->connect(eb.q, rep_q); - remove_bits[eb.cell].insert(eb.idx); - } - } - - for (auto &kv : remove_bits) { - Cell *cell = kv.first; - const std::set &drop = kv.second; - FfData &ff = ff_for_cell.at(cell); - std::vector keep; - - for (int i = 0; i < ff.width; i++) - if (!drop.count(i)) - keep.push_back(i); - - if (keep.empty()) { - module->remove(cell); - } else { - FfData new_ff = ff.slice(keep); - new_ff.cell = cell; - new_ff.emit(); - } - } - - return any_change; - } - - bool run_eqbits() - { - if (!opt.sat) - return false; - - std::vector bits; - dict ff_for_cell; - - std::vector> classes = gather_initial_eq_classes(bits, ff_for_cell); - if (classes.empty()) - return false; - - ModWalker &modwalker = get_modwalker(); - - // Simulation prepass - classes = filter_classes_sim(classes, bits, ff_for_cell, modwalker); - if (classes.empty()) - return false; - - // SAT prove - classes = filter_classes_sat(std::move(classes), bits, ff_for_cell, modwalker); - if (classes.empty()) - return false; - - return apply_eq_merges(classes, bits, ff_for_cell); - } -}; - -struct OptDffPass : public Pass { - OptDffPass() : Pass("opt_dff", "perform DFF optimizations") { } - - void help() override - { - // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| - log("\n"); - log(" opt_dff [-nodffe] [-nosdff] [-keepdc] [-sat] [selection]\n"); - log("\n"); - log("This pass converts flip-flops to a more suitable type by merging clock enables\n"); - log("and synchronous reset multiplexers, removing unused control inputs, or\n"); - log("potentially removes the flip-flop altogether, converting it to a constant\n"); - log("driver.\n"); - log("\n"); - log(" -nodffe\n"); - log(" disables dff -> dffe conversion, and other transforms recognizing clock\n"); - log(" enable\n"); - log("\n"); - log(" -nosdff\n"); - log(" disables dff -> sdff conversion, and other transforms recognizing sync\n"); - log(" resets\n"); - log("\n"); - log(" -simple-dffe\n"); - log(" only enables clock enable recognition transform for obvious cases\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(" or merged with equivalent flip-flops. this reasons in 2-valued logic\n"); - log(" and may resolve don't-care bits, so it is incompatible with -keepdc.\n"); - log(" the scratchpad option 'opt_dff.sat_effort' (solver propagation steps,\n"); - log(" default 1000000000, 0 = unlimited) deterministically bounds the total\n"); - log(" sat effort spent per module, remaining proofs are skipped once exceeded.\n"); - log("\n"); - log(" -keepdc\n"); - log(" some optimizations change the behavior of the circuit with respect to\n"); - log(" don't-care bits. for example in 'a+0' a single x-bit in 'a' will cause\n"); - log(" all result bits to be set to x. this behavior changes when 'a+0' is\n"); - log(" replaced by 'a'. the -keepdc option disables all such optimizations.\n"); - log("\n"); - } - - void execute(std::vector args, RTLIL::Design *design) override - { - log_header(design, "Executing OPT_DFF pass (perform DFF optimizations).\n"); - - OptDffOptions opt; - opt.nodffe = false; - opt.nosdff = false; - opt.simple_dffe = false; - opt.keepdc = false; - opt.sat = false; - - size_t argidx; - for (argidx = 1; argidx < args.size(); argidx++) { - if (args[argidx] == "-nodffe") { opt.nodffe = true; continue; } - if (args[argidx] == "-nosdff") { opt.nosdff = true; continue; } - if (args[argidx] == "-simple-dffe") { opt.simple_dffe = true; continue; } - if (args[argidx] == "-keepdc") { opt.keepdc = true; continue; } - if (args[argidx] == "-sat") { opt.sat = true; continue; } - break; - } - extra_args(args, argidx, design); - - // The SAT engine reasons in 2-valued logic (a constant x is treated as - // 0), so it can resolve don't-care bits to concrete values -- exactly - // what -keepdc promises not to do. Refuse the combination rather than - // silently ignore -keepdc. - if (opt.sat && opt.keepdc) - log_cmd_error("The -sat and -keepdc options are mutually exclusive.\n"); - - bool did_something = false; - for (auto mod : design->selected_modules()) { - OptDffWorker worker(opt, mod); - if (worker.run()) - did_something = true; - if (worker.run_constbits()) - did_something = true; - if (worker.run_eqbits()) - did_something = true; - } - - if (did_something) - design->scratchpad_set_bool("opt.did_something", true); - } -} OptDffPass; - -PRIVATE_NAMESPACE_END diff --git a/tests/opt/opt_dff_const_nosat.ys b/tests/opt/opt_dff_const_nosat.ys new file mode 100644 index 000000000..89e02a819 --- /dev/null +++ b/tests/opt/opt_dff_const_nosat.ys @@ -0,0 +1,24 @@ +logger -werror "solver effort budget" +scratchpad -set opt_dff.sat_effort 1 + +read_verilog <