From 7cea58eead3f52516159f4f6235e4cc3a1ff5c17 Mon Sep 17 00:00:00 2001 From: nella Date: Mon, 10 Aug 2026 09:52:14 +0200 Subject: [PATCH 01/17] More sat constbits tests. --- tests/opt/opt_dff_sat_const.ys | 144 +++++++++++++++++++++++++++++++++ 1 file changed, 144 insertions(+) diff --git a/tests/opt/opt_dff_sat_const.ys b/tests/opt/opt_dff_sat_const.ys index 8c8000e8a..eae8550a0 100644 --- a/tests/opt/opt_dff_sat_const.ys +++ b/tests/opt/opt_dff_sat_const.ys @@ -170,3 +170,147 @@ async2sync equiv_make test_case gate equiv equiv_induct equiv equiv_status -assert + + +# async reset +design -reset +read_verilog -sv < Date: Mon, 10 Aug 2026 11:37:41 +0200 Subject: [PATCH 02/17] Document constbits candidate logic. --- passes/opt/opt_dff.cc | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 5ca955c67..90f1d3252 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -256,8 +256,9 @@ struct OptDffWorker } } + // 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) { - // 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; @@ -916,6 +917,11 @@ struct OptDffWorker return did_something; } + // 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 + // computes the induction base case only, commits happen in run_constbits State check_constbit(FfData &ff, int i) { State val = ff.val_init[i]; @@ -966,7 +972,15 @@ struct OptDffWorker return true; } - // Try to decide whether target t of obligation ob is constant, under the given per-query cap. + // try to decide target t of obligation ob under the given per-query effort cap + // returns false if the cap was hit and the target is still undecided + // + // induction step: assuming q already holds the candidate value, the value fed + // through this target must equal it again; check_constbit provides the base + // case, so unsat makes the constant an inductive invariant + // + // the qcsat cone is an over-approximation (complex cells become free inputs), + // so only unsat is binding; a spurious sat model merely drops a valid proof bool resolve_const_target(QuickConeSat &qcsat, int64_t cap, ConstObligation &ob, ConstTarget &t, const std::vector &modelExprs, const std::vector &model_obs) { From 8943824f078fe512d50ae27cf4958b74713f8fdf Mon Sep 17 00:00:00 2001 From: nella Date: Mon, 10 Aug 2026 14:19:07 +0200 Subject: [PATCH 03/17] Sigmap const checks. --- passes/opt/opt_dff.cc | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 90f1d3252..8e9a6276e 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -928,9 +928,9 @@ struct OptDffWorker 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)) + if (!is_inactive(sigmap(ff.sig_clr[i]), ff.pol_clr)) val = combine_const(val, State::S0); - if (ff.sig_set[i] != (ff.pol_set ? State::S0 : State::S1)) + if (!is_inactive(sigmap(ff.sig_set[i]), ff.pol_set)) val = combine_const(val, State::S1); } @@ -1040,13 +1040,18 @@ struct OptDffWorker 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); + bool has_d = ff.has_clk || ff.has_gclk; + SigBit d = has_d ? sigmap(ff.sig_d[i]) : SigBit(); + SigBit ad = ff.has_aload ? sigmap(ff.sig_ad[i]) : SigBit(); + + // fold all const inputs first, so the sat targets are checked + // against the final candidate + if (has_d && !d.wire) { + val = combine_const(val, d.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 (ff.has_aload && !ad.wire) { + val = combine_const(val, ad.data); if (val == State::Sm) continue; } @@ -1057,10 +1062,10 @@ struct OptDffWorker 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 (has_d && d.wire) + feasible = add_const_target(modwalker, ob, d); + if (feasible && ff.has_aload && ad.wire) + feasible = add_const_target(modwalker, ob, ad); if (!feasible) continue; From 5a5fe1619b2354c734a7e20d551bbbed9141dbad Mon Sep 17 00:00:00 2001 From: nella Date: Mon, 10 Aug 2026 17:03:56 +0200 Subject: [PATCH 04/17] Split constbits into gather/solve/commit. --- passes/opt/opt_dff.cc | 155 ++++++++++++++++++++++-------------------- 1 file changed, 80 insertions(+), 75 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 8e9a6276e..5aa3a79d2 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -937,14 +937,16 @@ struct OptDffWorker 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 + // one non-const input (D and/or AD) of a suspected-constant ff bit; the sat + // pass must show it equal to the candidate value struct ConstTarget { SigBit sig; int lit = -1; bool proven = false; }; + // one ff bit suspected to be stuck at val; committed once every target is + // proven, dropped as soon as one counterexample disproves it struct ConstObligation { Cell *cell; int idx; @@ -953,20 +955,29 @@ struct OptDffWorker int q_lit = -1; bool dropped = false; std::vector targets; + + bool proven() const { + for (auto &t : targets) + if (!t.proven) + return false; + return true; + } }; - void commit_const(dict> &const_bits, Cell *cell, int i, SigBit q, State val) + void commit_const(dict> &const_bits, const ConstObligation &ob) { 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); + ob.val == State::S1 ? 1 : 0, ob.idx, ob.cell, ob.cell->type.unescape(), module); + initvals.remove_init(ob.q); + module->connect(ob.q, ob.val); + const_bits[ob.cell].insert(ob.idx); } - bool add_const_target(ModWalker &modwalker, ConstObligation &ob, SigBit sig) + bool add_const_target(ConstObligation &ob, SigBit sig) { - if (!opt.sat || (ob.val != State::S0 && ob.val != State::S1) || !modwalker.has_drivers(sig)) + if (!opt.sat || (ob.val != State::S0 && ob.val != State::S1)) + return false; + if (!get_modwalker().has_drivers(sig)) return false; ob.targets.push_back(ConstTarget{sig}); return true; @@ -1017,16 +1028,25 @@ struct OptDffWorker return true; } - bool run_constbits() + void remove_ff_bits(Cell *cell, const pool &drop) { - // Find FFs that are provably constant - ModWalker &modwalker = get_modwalker(); + FfData ff(&initvals, cell); + std::vector keep; + for (int i = 0; i < ff.width; i++) + if (!drop.count(i)) + keep.push_back(i); - dict> const_bits; - bool did_something = false; + // emit removes the cell outright when no bits are kept + FfData new_ff = ff.slice(keep); + new_ff.cell = cell; + new_ff.emit(); + } - // fold constant D/AD inputs into the tested value first - // bits whose remaining inputs are wires become SAT proof obligations + // fold constant D/AD inputs into the candidate value; bits with remaining + // wire inputs get sat proof targets (only when -sat is in effect), bits + // with none are trivially proven + std::vector gather_const_obligations() + { std::vector obligations; for (auto cell : module->selected_cells()) { @@ -1063,31 +1083,38 @@ struct OptDffWorker bool feasible = true; if (has_d && d.wire) - feasible = add_const_target(modwalker, ob, d); + feasible = add_const_target(ob, d); if (feasible && ff.has_aload && ad.wire) - feasible = add_const_target(modwalker, ob, ad); + feasible = add_const_target(ob, ad); 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); + obligations.push_back(std::move(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))); - } + return obligations; + } - // Each obligation is proven independently, so processing obligations in + // sat phase: prove the gathered obligations, marking targets proven or + // obligations dropped in place + void solve_const_obligations(std::vector &obligations) + { + int64_t num_queries = 0; + for (auto &ob : obligations) + num_queries += GetSize(ob.targets); + if (num_queries == 0) + return; + + ModWalker &modwalker = get_modwalker(); + + // screening cap, scaled down when the budget cannot afford a + // full-price screening round + int64_t screen_cap = 0; + if (sat_budget.enabled()) + 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); @@ -1095,9 +1122,13 @@ struct OptDffWorker int batch_end = batch_begin; while (batch_end < GetSize(obligations) && !warn_if_budget_spent()) { + auto &ob = obligations[batch_end]; + if (ob.targets.empty()) { + batch_end++; + continue; + } 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); @@ -1106,11 +1137,10 @@ struct OptDffWorker batch_end++; } - // Sweep the batch under a cheap screening cap, then re-sweep the still-undecided targets - int64_t cap = screen_cap; + // sweep the batch under the cheap screening cap first, then re-sweep + // the still-undecided targets with the full remaining budget bool out_of_budget = false; - - while (!out_of_budget) { + for (int64_t cap : {screen_cap, (int64_t)0}) { bool all_resolved = true; // Counter ex.: every pending target in the batch. Entries that get proven or dropped later @@ -1147,52 +1177,27 @@ struct OptDffWorker 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; - } - } + bool run_constbits() + { + std::vector obligations = gather_const_obligations(); - // Reconstruct FF with constant bits removed - std::vector cells_to_remove; - std::vector ffs_to_emit; + solve_const_obligations(obligations); - 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); + dict> const_bits; + for (auto &ob : obligations) + if (!ob.dropped && ob.proven()) + commit_const(const_bits, ob); - 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, drop] : const_bits) + remove_ff_bits(cell, drop); - for (auto* cell : cells_to_remove) - module->remove(cell); - - for (auto& ff : ffs_to_emit) - ff.emit(); - - return did_something; + return !const_bits.empty(); } struct EqBit { From 4c0979e88ed4ac00249b1b32e1c448ab9ec3b865 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 12 Aug 2026 08:12:33 +0200 Subject: [PATCH 05/17] Separate constbits batching. --- passes/opt/opt_dff.cc | 130 ++++++++++++++++++++++-------------------- 1 file changed, 69 insertions(+), 61 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 5aa3a79d2..79cf68684 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -1096,6 +1096,73 @@ struct OptDffWorker 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) && !warn_if_budget_spent()) { + auto &ob = obligations[batch_end]; + if (ob.targets.empty()) { + batch_end++; + continue; + } + if (batch_end > batch_begin && GetSize(qcsat.imported_cells) >= sat_batch_cells) + break; + 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++; + } + + return batch_end; + } + + // sweep the batch under the cheap screening cap first, then re-sweep the + // still-undecided targets 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; + + // 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; obi++) { + auto &ob = obligations[obi]; + for (auto &t : ob.targets) { + if (ob.dropped) + break; + if (t.proven) + continue; + if (warn_if_budget_spent()) + return; + if (!resolve_const_target(qcsat, cap, ob, t, modelExprs, model_obs)) + all_resolved = false; + } + } + + if (all_resolved) + return; + } + } + // sat phase: prove the gathered obligations, marking targets proven or // obligations dropped in place void solve_const_obligations(std::vector &obligations) @@ -1118,67 +1185,8 @@ struct OptDffWorker // 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()) { - auto &ob = obligations[batch_end]; - if (ob.targets.empty()) { - batch_end++; - continue; - } - if (batch_end > batch_begin && GetSize(qcsat.imported_cells) >= sat_batch_cells) - break; - 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 the cheap screening cap first, then re-sweep - // the still-undecided targets with the full remaining budget - bool out_of_budget = false; - for (int64_t cap : {screen_cap, (int64_t)0}) { - 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; - } - + 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; } } From 040dbe08395bf76b4746d430114593e1ce468934 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 12 Aug 2026 08:47:10 +0200 Subject: [PATCH 06/17] Constbits counterexample watch list. --- passes/opt/opt_dff.cc | 65 ++++++++++++++++++++++++------------------- 1 file changed, 36 insertions(+), 29 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 79cf68684..4e4619d1f 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -964,6 +964,29 @@ struct OptDffWorker } }; + // counterexample watch list: the solver model captures (target, q) of every + // pending target so one counterexample can disprove many obligations at once + struct ConstWatchList { + std::vector exprs; + std::vector obs; + + void watch(ConstObligation &ob, const ConstTarget &t) { + exprs.push_back(t.lit); + exprs.push_back(ob.q_lit); + obs.push_back(&ob); + } + + // drop every obligation whose q holds its constant while the watched + // target differs in the model + 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] != want) + obs[k]->dropped = true; + } + } + }; + void commit_const(dict> &const_bits, const ConstObligation &ob) { log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n", @@ -993,37 +1016,24 @@ struct OptDffWorker // the qcsat cone is an over-approximation (complex cells become free inputs), // so only unsat is binding; a spurious sat model merely drops a valid proof bool resolve_const_target(QuickConeSat &qcsat, int64_t cap, ConstObligation &ob, ConstTarget &t, - const std::vector &modelExprs, const std::vector &model_obs) + const ConstWatchList &watches) { - // 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); + std::vector model; + auto res = sat_budget.solve(qcsat, cap, watches.exprs, model, assumptions); if (res == SatEffortBudget::Result::LimitReached) - return false; // Nothing changed + return false; if (res == SatEffortBudget::Result::Unsat) { - t.proven = true; // t is proven to be const + t.proven = true; 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; - } + watches.drop_disproven(model); ob.dropped = true; return true; } @@ -1128,20 +1138,17 @@ struct OptDffWorker for (int64_t cap : {screen_cap, (int64_t)0}) { 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; + // watch 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) + ConstWatchList watches; 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); - } + if (!t.proven) + watches.watch(ob, t); } for (int obi = batch_begin; obi < batch_end; obi++) { @@ -1153,7 +1160,7 @@ struct OptDffWorker continue; if (warn_if_budget_spent()) return; - if (!resolve_const_target(qcsat, cap, ob, t, modelExprs, model_obs)) + if (!resolve_const_target(qcsat, cap, ob, t, watches)) all_resolved = false; } } From 96e776fbfcbc7f4c44288f994d4446bbacb3c3b1 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 12 Aug 2026 09:21:48 +0200 Subject: [PATCH 07/17] Single driver lookup in bitsim. --- passes/opt/opt_dff.cc | 57 ++++++++++++++++++++----------------------- 1 file changed, 27 insertions(+), 30 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 4e4619d1f..cf65f6663 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -84,42 +84,39 @@ struct BitSim { } evals_left--; + // pre-seed to break combinational loops sim_vals[mapped] = 0; uint64_t res = 0; - if (!modwalker.has_drivers(mapped)) { + auto drv = modwalker.signal_drivers.find(mapped); + if (drv == modwalker.signal_drivers.end() || drv->second.empty()) { 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; + 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(); - } + 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(); } } From fc4b87363e1b95183a3d6f7153fbe39b1f361062 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 12 Aug 2026 09:58:22 +0200 Subject: [PATCH 08/17] Bundle eqbits candidates. --- passes/opt/opt_dff.cc | 119 +++++++++++++++++------------------------- 1 file changed, 48 insertions(+), 71 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index cf65f6663..de7f792b6 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -1257,13 +1257,20 @@ struct OptDffWorker } }; + // concrete 0/1 bit, as opposed to x/z 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) + 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 @@ -1275,7 +1282,7 @@ struct OptDffWorker if (!ff.has_clk && !ff.has_gclk) continue; - ff_for_cell.emplace(cell, ff); + cand.ffs.emplace(cell, ff); for (int i = 0; i < ff.width; i++) { // Skip bits whose reset value is undefined (x) @@ -1325,45 +1332,40 @@ struct OptDffWorker if (ff.pol_set) k.flags |= SigKey::PolSet; } - bits.push_back({cell, i, ff.sig_q[i]}); + cand.bits.push_back({cell, i, ff.sig_q[i]}); keys.push_back(k); } } dict> buckets; - for (int i = 0; i < GetSize(bits); i++) + for (int i = 0; i < GetSize(cand.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)); + cand.classes.push_back(std::move(kv.second)); - return classes; + return cand; } - 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); + void filter_classes_sim(EqCandidates &cand) + { + BitSim sim(module, sigmap, get_modwalker()); // Assume same class - for (auto &cls : classes) { + for (auto &cls : cand.classes) { uint64_t class_q_val = sim.next_rand(); for (int idx : cls) { - sim.sim_vals[sigmap(bits[idx].q)] = class_q_val; + sim.sim_vals[sigmap(cand.bits[idx].q)] = class_q_val; } } std::vector> refined_classes; - for (auto &cls : classes) { + for (auto &cls : cand.classes) { dict> sim_buckets; for (int idx : cls) { - const EqBit &eb = bits[idx]; - const FfData &ff = ff_for_cell.at(eb.cell); + 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) { @@ -1400,23 +1402,21 @@ struct OptDffWorker refined_classes.push_back(std::move(kv.second)); } - return refined_classes; + cand.classes = std::move(refined_classes); } - std::vector> drop_all_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(module)); - return {}; + cand.classes.clear(); } - std::vector> filter_classes_sat( - std::vector> classes, - const std::vector &bits, - const dict &ff_for_cell, - ModWalker &modwalker - ) { - QuickConeSat qcsat(modwalker); + void filter_classes_sat(EqCandidates &cand) + { + auto &classes = cand.classes; + auto &bits = cand.bits; + QuickConeSat qcsat(get_modwalker()); std::vector q_lit(bits.size(), -1); std::vector n_lit(bits.size(), -1); @@ -1428,10 +1428,10 @@ struct OptDffWorker // current states (and those of every other candidate pair) agree for (auto &cls : classes) { if (warn_if_budget_spent()) - return drop_all_classes(); + return drop_all_classes(cand); for (int idx : cls) { const EqBit &eb = bits[idx]; - const FfData &ff = ff_for_cell.at(eb.cell); + const FfData &ff = cand.ffs.at(eb.cell); q_lit[idx] = qcsat.importSigBit(eb.q); int n = qcsat.importSigBit(ff.sig_d[eb.idx]); @@ -1501,7 +1501,7 @@ struct OptDffWorker continue; if (warn_if_budget_spent()) - return drop_all_classes(); + 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]]); @@ -1518,7 +1518,7 @@ struct OptDffWorker if (res == SatEffortBudget::Result::LimitReached) { warn_if_budget_spent(); - return drop_all_classes(); + return drop_all_classes(cand); } if (res == SatEffortBudget::Result::Sat) { @@ -1551,47 +1551,29 @@ struct OptDffWorker 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 apply_eq_merges(const EqCandidates &cand) { bool any_change = false; - dict> remove_bits; + dict> remove_bits; // Drive every non-rep Q from its class rep, drop merged bits from their FFs - for (auto &cls : classes) { + for (auto &cls : cand.classes) { if (GetSize(cls) < 2) continue; - SigBit rep_q = bits[cls[0]].q; + SigBit rep_q = cand.bits[cls[0]].q; any_change = true; for (int k = 1; k < GetSize(cls); k++) { - const EqBit &eb = bits[cls[k]]; + const EqBit &eb = cand.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(); - } - } + for (auto &[cell, drop] : remove_bits) + remove_ff_bits(cell, drop); return any_change; } @@ -1601,26 +1583,21 @@ struct OptDffWorker 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()) + EqCandidates cand = gather_initial_eq_classes(); + if (cand.classes.empty()) return false; - ModWalker &modwalker = get_modwalker(); - // Simulation prepass - classes = filter_classes_sim(classes, bits, ff_for_cell, modwalker); - if (classes.empty()) + filter_classes_sim(cand); + if (cand.classes.empty()) return false; // SAT prove - classes = filter_classes_sat(std::move(classes), bits, ff_for_cell, modwalker); - if (classes.empty()) + filter_classes_sat(cand); + if (cand.classes.empty()) return false; - return apply_eq_merges(classes, bits, ff_for_cell); + return apply_eq_merges(cand); } }; From 01df56414d0db36435c392a6b03448e7c3c0561d Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 12 Aug 2026 10:26:05 +0200 Subject: [PATCH 09/17] One sat query per obligation. --- passes/opt/opt_dff.cc | 133 +++++++++++++++++------------------------- 1 file changed, 54 insertions(+), 79 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index de7f792b6..e041a32ac 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -934,52 +934,39 @@ struct OptDffWorker return val; } - // one non-const input (D and/or AD) of a suspected-constant ff bit; the sat - // pass must show it equal to the candidate value - struct ConstTarget { - SigBit sig; - int lit = -1; - bool proven = false; - }; - - // one ff bit suspected to be stuck at val; committed once every target is - // proven, dropped as soon as one counterexample disproves it struct ConstObligation { + enum Status { Pending, Proven, Dropped }; + Cell *cell; int idx; State val; SigBit q; - int q_lit = -1; - bool dropped = false; - std::vector targets; + std::vector targets; // non-const inputs (D, AD), must be shown to be eq + Status status = Pending; - bool proven() const { - for (auto &t : targets) - if (!t.proven) - return false; - return true; - } + + int q_lit = -1; // valid within the current batch + int differ_lit = -1; // some target differs from the candidate value }; - // counterexample watch list: the solver model captures (target, q) of every - // pending target so one counterexample can disprove many obligations at once + // the solver model captures (differ, q) of every pending obligation so one + // counterexample can disprove many at once struct ConstWatchList { std::vector exprs; std::vector obs; - void watch(ConstObligation &ob, const ConstTarget &t) { - exprs.push_back(t.lit); + 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 the watched - // target differs in the model + // 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] != want) - obs[k]->dropped = true; + if (model[2*k + 1] == want && model[2*k]) + obs[k]->status = ConstObligation::Dropped; } } }; @@ -999,26 +986,21 @@ struct OptDffWorker return false; if (!get_modwalker().has_drivers(sig)) return false; - ob.targets.push_back(ConstTarget{sig}); + ob.targets.push_back(sig); return true; } - // try to decide target t of obligation ob under the given per-query effort cap - // returns false if the cap was hit and the target is still undecided - // - // induction step: assuming q already holds the candidate value, the value fed - // through this target must equal it again; check_constbit provides the base - // case, so unsat makes the constant an inductive invariant - // - // the qcsat cone is an over-approximation (complex cells become free inputs), - // so only unsat is binding; a spurious sat model merely drops a valid proof - bool resolve_const_target(QuickConeSat &qcsat, int64_t cap, ConstObligation &ob, ConstTarget &t, + // try to decide obligation ob under the given per-query effort cap + 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(qcsat.ez->NOT(qcsat.ez->IFF(t.lit, vlit))); + assumptions.push_back(ob.differ_lit); std::vector model; auto res = sat_budget.solve(qcsat, cap, watches.exprs, model, assumptions); @@ -1026,12 +1008,12 @@ struct OptDffWorker if (res == SatEffortBudget::Result::LimitReached) return false; if (res == SatEffortBudget::Result::Unsat) { - t.proven = true; + ob.status = ConstObligation::Proven; return true; } watches.drop_disproven(model); - ob.dropped = true; + ob.status = ConstObligation::Dropped; return true; } @@ -1043,7 +1025,6 @@ struct OptDffWorker if (!drop.count(i)) keep.push_back(i); - // emit removes the cell outright when no bits are kept FfData new_ff = ff.slice(keep); new_ff.cell = cell; new_ff.emit(); @@ -1073,14 +1054,12 @@ struct OptDffWorker // fold all const inputs first, so the sat targets are checked // against the final candidate - if (has_d && !d.wire) { + if (has_d && !d.wire) val = combine_const(val, d.data); - if (val == State::Sm) continue; - } - if (ff.has_aload && !ad.wire) { + if (ff.has_aload && !ad.wire) val = combine_const(val, ad.data); - if (val == State::Sm) continue; - } + if (val == State::Sm) + continue; ConstObligation ob; ob.cell = cell; @@ -1096,6 +1075,8 @@ struct OptDffWorker if (!feasible) continue; + if (ob.targets.empty()) + ob.status = ConstObligation::Proven; obligations.push_back(std::move(ob)); } } @@ -1110,15 +1091,18 @@ struct OptDffWorker while (batch_end < GetSize(obligations) && !warn_if_budget_spent()) { auto &ob = obligations[batch_end]; - if (ob.targets.empty()) { + 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); - for (auto &t : ob.targets) - t.lit = qcsat.importSigBit(t.sig); + 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(); sat_budget.charge_import(qcsat, cells_charged); batch_end++; @@ -1128,38 +1112,29 @@ struct OptDffWorker } // sweep the batch under the cheap screening cap first, then re-sweep the - // still-undecided targets with the full remaining budget + // 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 target in the batch; entries that get proven - // or dropped later in the sweep are harmless (a proven bit is - // constant in every model) + // watch every pending obligation in the batch ConstWatchList watches; 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) - watches.watch(ob, t); + if (ob.status == ConstObligation::Pending) + watches.watch(ob); } for (int obi = batch_begin; obi < batch_end; obi++) { auto &ob = obligations[obi]; - for (auto &t : ob.targets) { - if (ob.dropped) - break; - if (t.proven) - continue; - if (warn_if_budget_spent()) - return; - if (!resolve_const_target(qcsat, cap, ob, t, watches)) - all_resolved = false; - } + if (ob.status != ConstObligation::Pending) + continue; + if (warn_if_budget_spent()) + return; + if (!resolve_const_obligation(qcsat, cap, ob, watches)) + all_resolved = false; } if (all_resolved) @@ -1167,26 +1142,26 @@ struct OptDffWorker } } - // sat phase: prove the gathered obligations, marking targets proven or - // obligations dropped in place + // sat: prove or drop the still-pending obligations in place void solve_const_obligations(std::vector &obligations) { int64_t num_queries = 0; for (auto &ob : obligations) - num_queries += GetSize(ob.targets); + num_queries += (ob.status == ConstObligation::Pending); if (num_queries == 0) return; ModWalker &modwalker = get_modwalker(); - // screening cap, scaled down when the budget cannot afford a - // full-price screening round + // screening cap int64_t screen_cap = 0; - if (sat_budget.enabled()) + if (sat_budget.enabled()) { + // scale down when we can't afford a full screening round 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 + // 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) && !warn_if_budget_spent(); ) { QuickConeSat qcsat(modwalker); int batch_end = build_const_batch(qcsat, obligations, batch_begin); @@ -1203,7 +1178,7 @@ struct OptDffWorker dict> const_bits; for (auto &ob : obligations) - if (!ob.dropped && ob.proven()) + if (ob.status == ConstObligation::Proven) commit_const(const_bits, ob); for (auto &[cell, drop] : const_bits) From 5f5c1a7a3359bdc2c56ce9dd3fbef30fc23b50fc Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 12 Aug 2026 10:52:39 +0200 Subject: [PATCH 10/17] Comment and style touchups. --- passes/opt/opt_dff.cc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index e041a32ac..a15e018a6 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -918,7 +918,7 @@ struct OptDffWorker // 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 - // computes the induction base case only, commits happen in run_constbits + // the candidate doubles as the induction base case State check_constbit(FfData &ff, int i) { State val = ff.val_init[i]; @@ -952,6 +952,7 @@ struct OptDffWorker // 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; @@ -1501,7 +1502,7 @@ struct OptDffWorker std::vector sub0; std::vector sub1; - for (size_t b_idx = 0; b_idx < cls.size(); b_idx++) { + for (int b_idx = 0; b_idx < GetSize(cls); b_idx++) { if (modelVals[b_idx]) sub1.push_back(cls[b_idx]); else From 32a9fd228115ed19b720caee5acd1c45eabbec31 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 12 Aug 2026 10:58:47 +0200 Subject: [PATCH 11/17] Whitespace. --- passes/opt/opt_dff.cc | 1 - 1 file changed, 1 deletion(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index a15e018a6..21fa418a0 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -944,7 +944,6 @@ struct OptDffWorker 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 }; From 95baa38274b1a94daf5297976ba4b67ba801973c Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 12 Aug 2026 11:52:32 +0200 Subject: [PATCH 12/17] Document ConstObligation. --- passes/opt/opt_dff.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 21fa418a0..391858bca 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -934,6 +934,8 @@ struct OptDffWorker return val; } + // 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 }; From f8bf9ad1c899e551006cff1339327854f32fba68 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 12 Aug 2026 18:44:30 +0200 Subject: [PATCH 13/17] opt_dff: split up --- docs/source/getting_started/installation.rst | 2 +- passes/opt/CMakeLists.txt | 8 +- passes/opt/dff/CMakeLists.txt | 9 + passes/opt/dff/constbits.cc | 298 ++++ passes/opt/dff/eqbits.cc | 500 ++++++ passes/opt/dff/opt_dff.cc | 168 ++ passes/opt/dff/opt_dff.h | 156 ++ passes/opt/dff/simple.cc | 715 ++++++++ passes/opt/opt_dff.cc | 1668 ------------------ 9 files changed, 1849 insertions(+), 1675 deletions(-) create mode 100644 passes/opt/dff/CMakeLists.txt create mode 100644 passes/opt/dff/constbits.cc create mode 100644 passes/opt/dff/eqbits.cc create mode 100644 passes/opt/dff/opt_dff.cc create mode 100644 passes/opt/dff/opt_dff.h create mode 100644 passes/opt/dff/simple.cc delete mode 100644 passes/opt/opt_dff.cc 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/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/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..3639dc809 --- /dev/null +++ b/passes/opt/dff/constbits.cc @@ -0,0 +1,298 @@ +/* + * 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 "passes/opt/dff/opt_dff.h" + +USING_YOSYS_NAMESPACE + +YOSYS_NAMESPACE_BEGIN + +// lattice join of candidate constants: Sx is the identity (unless -keepdc +// pins it), equal values join, Sm marks a conflict +State OptDffWorker::combine_const(State a, State b) { + if (a == State::Sx && !opt.keepdc) return b; + if (b == State::Sx && !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 OptDffWorker::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 (!is_inactive(sigmap(ff.sig_clr[i]), ff.pol_clr)) + val = combine_const(val, State::S0); + if (!is_inactive(sigmap(ff.sig_set[i]), ff.pol_set)) + val = combine_const(val, State::S1); + } + + return val; +} + +// 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 OptDffWorker::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 OptDffWorker::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 OptDffWorker::commit_const(dict> &const_bits, const ConstObligation &ob) +{ + log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n", + ob.val == State::S1 ? 1 : 0, ob.idx, ob.cell, ob.cell->type.unescape(), module); + initvals.remove_init(ob.q); + module->connect(ob.q, ob.val); + const_bits[ob.cell].insert(ob.idx); +} + +bool OptDffWorker::add_const_target(ConstObligation &ob, SigBit sig) +{ + if (!opt.sat || (ob.val != State::S0 && ob.val != State::S1)) + return false; + if (!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 +bool OptDffWorker::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 = sat_budget.solve(qcsat, cap, watches.exprs, model, assumptions); + + if (res == SatEffortBudget::Result::LimitReached) + return false; + if (res == SatEffortBudget::Result::Unsat) { + ob.status = ConstObligation::Proven; + return true; + } + + watches.drop_disproven(model); + ob.status = ConstObligation::Dropped; + return true; +} + +// fold constant D/AD inputs into the candidate value; bits with remaining +// wire inputs get sat proof targets (only when -sat is in effect), bits +// with none are trivially proven +std::vector OptDffWorker::gather_const_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; + + bool has_d = ff.has_clk || ff.has_gclk; + SigBit d = has_d ? sigmap(ff.sig_d[i]) : SigBit(); + SigBit ad = ff.has_aload ? sigmap(ff.sig_ad[i]) : SigBit(); + + // fold all const inputs first, so the sat targets are checked + // against the final candidate + if (has_d && !d.wire) + val = combine_const(val, d.data); + if (ff.has_aload && !ad.wire) + val = combine_const(val, ad.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 (has_d && d.wire) + feasible = add_const_target(ob, d); + if (feasible && ff.has_aload && ad.wire) + feasible = add_const_target(ob, ad); + if (!feasible) + continue; + + if (ob.targets.empty()) + ob.status = ConstObligation::Proven; + obligations.push_back(std::move(ob)); + } + } + + return obligations; +} + +int OptDffWorker::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) && !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(); + 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 OptDffWorker::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 (warn_if_budget_spent()) + return; + if (!resolve_const_obligation(qcsat, cap, ob, watches)) + all_resolved = false; + } + + if (all_resolved) + return; + } +} + +// sat: prove or drop the still-pending obligations in place +void OptDffWorker::solve_const_obligations(std::vector &obligations) +{ + int64_t num_queries = 0; + for (auto &ob : obligations) + num_queries += (ob.status == ConstObligation::Pending); + if (num_queries == 0) + return; + + ModWalker &modwalker = get_modwalker(); + + // screening cap + int64_t screen_cap = 0; + if (sat_budget.enabled()) { + // scale down when we can't afford a full screening round + screen_cap = max((int64_t)20000, min((int64_t)200000, 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) && !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 OptDffWorker::run_constbits() +{ + std::vector obligations = gather_const_obligations(); + + solve_const_obligations(obligations); + + dict> const_bits; + for (auto &ob : obligations) + if (ob.status == ConstObligation::Proven) + commit_const(const_bits, ob); + + for (auto &[cell, drop] : const_bits) + remove_ff_bits(cell, drop); + + return !const_bits.empty(); +} + +YOSYS_NAMESPACE_END diff --git a/passes/opt/dff/eqbits.cc b/passes/opt/dff/eqbits.cc new file mode 100644 index 000000000..86fc917b3 --- /dev/null +++ b/passes/opt/dff/eqbits.cc @@ -0,0 +1,500 @@ +/* + * 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 "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; +} + +PRIVATE_NAMESPACE_END + +YOSYS_NAMESPACE_BEGIN + +struct OptDffWorker::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 OptDffWorker::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 OptDffWorker::EqCandidates { + std::vector bits; + dict ffs; + std::vector> classes; +}; + +OptDffWorker::EqCandidates OptDffWorker::gather_initial_eq_classes() +{ + EqCandidates cand; + 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; + + 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 OptDffWorker::filter_classes_sim(EqCandidates &cand) +{ + BitSim sim(module, sigmap, 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[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 OptDffWorker::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(module)); + cand.classes.clear(); +} + +void OptDffWorker::filter_classes_sat(EqCandidates &cand) +{ + auto &classes = cand.classes; + auto &bits = cand.bits; + QuickConeSat qcsat(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 (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(); + 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(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 = sat_budget.solve(qcsat, 0, modelExprs, modelVals, assumptions); + + if (res == SatEffortBudget::Result::LimitReached) { + 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 OptDffWorker::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]]; + initvals.remove_init(eb.q); + module->connect(eb.q, rep_q); + remove_bits[eb.cell].insert(eb.idx); + } + } + + for (auto &[cell, drop] : remove_bits) + remove_ff_bits(cell, drop); + + return any_change; +} + +bool OptDffWorker::run_eqbits() +{ + if (!opt.sat) + return false; + + 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); +} + +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..1d12327ad --- /dev/null +++ b/passes/opt/dff/opt_dff.cc @@ -0,0 +1,168 @@ +/* + * 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 "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)); + + // 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); + } +} + +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; + 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/passes/opt/dff/opt_dff.h b/passes/opt/dff/opt_dff.h new file mode 100644 index 000000000..34db52d3d --- /dev/null +++ b/passes/opt/dff/opt_dff.h @@ -0,0 +1,156 @@ +/* + * 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" +#include "kernel/ff.h" +#include "kernel/pattern.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; + + // 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); + } + + OptDffWorker(const OptDffOptions &opt, Module *mod); + + void remove_ff_bits(Cell *cell, const pool &drop); + + SigSpec create_not(SigSpec a, bool is_fine); + SigSpec create_and(SigSpec a, SigSpec b, bool is_fine); + void create_mux_to_output(SigSpec a, SigSpec b, SigSpec sel, SigSpec y, bool pol, bool is_fine); + void maybe_simplemap(Cell *c, bool make_gates); + patterns_t find_muxtree_feedback_patterns(RTLIL::SigBit d, RTLIL::SigBit q, pattern_t path); + ctrl_t make_patterns_logic(const patterns_t &patterns, const ctrls_t &ctrls, bool make_gates); + ctrl_t combine_resets(const ctrls_t &ctrls, bool make_gates); + bool signal_all_same(const SigSpec &sig); + bool optimize_sr(FfData &ff, Cell *cell, bool &changed); + bool optimize_aload(FfData &ff, Cell *cell, bool &changed); + bool optimize_arst(FfData &ff, Cell *cell, bool &changed); + void optimize_srst(FfData &ff, Cell *cell, bool &changed); + void optimize_ce(FfData &ff, Cell *cell, bool &changed); + void optimize_const_clk(FfData &ff, Cell *cell, bool &changed); + void optimize_d_equals_q(FfData &ff, Cell *cell, bool &changed); + bool try_merge_srst(FfData &ff, Cell *cell, bool &changed); + bool try_merge_ce(FfData &ff, Cell *cell, bool &changed); + bool run(); + + struct ConstObligation; + struct ConstWatchList; + State combine_const(State a, State b); + State check_constbit(FfData &ff, int i); + void commit_const(dict> &const_bits, const ConstObligation &ob); + bool add_const_target(ConstObligation &ob, SigBit sig); + bool resolve_const_obligation(QuickConeSat &qcsat, int64_t cap, ConstObligation &ob, + const ConstWatchList &watches); + std::vector gather_const_obligations(); + int build_const_batch(QuickConeSat &qcsat, std::vector &obligations, int batch_begin); + void sweep_const_batch(QuickConeSat &qcsat, std::vector &obligations, + int batch_begin, int batch_end, int64_t screen_cap); + void solve_const_obligations(std::vector &obligations); + bool run_constbits(); + + struct EqBit; + struct SigKey; + struct EqCandidates; + EqCandidates gather_initial_eq_classes(); + void filter_classes_sim(EqCandidates &cand); + void drop_all_classes(EqCandidates &cand); + void filter_classes_sat(EqCandidates &cand); + bool apply_eq_merges(const EqCandidates &cand); + 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..69f875866 --- /dev/null +++ b/passes/opt/dff/simple.cc @@ -0,0 +1,715 @@ +/* + * 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 "passes/opt/dff/opt_dff.h" +#include "passes/techmap/simplemap.h" + +USING_YOSYS_NAMESPACE + +YOSYS_NAMESPACE_BEGIN + +SigSpec OptDffWorker::create_not(SigSpec a, bool is_fine) { + if (is_fine) + return module->NotGate(NEW_ID, a); + else + return module->Not(NEW_ID, a); +} + +SigSpec OptDffWorker::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 OptDffWorker::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 OptDffWorker::maybe_simplemap(Cell *c, bool make_gates) { + if (make_gates) { + simplemap(module, c); + module->remove(c); + } +} + +patterns_t OptDffWorker::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 OptDffWorker::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 OptDffWorker::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 OptDffWorker::signal_all_same(const SigSpec &sig) { + for (int i = 1; i < GetSize(sig); i++) + if (sig[i] != sig[0]) + return false; + return true; +} + +bool OptDffWorker::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 OptDffWorker::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 OptDffWorker::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 OptDffWorker::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 OptDffWorker::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 OptDffWorker::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 OptDffWorker::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 OptDffWorker::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 OptDffWorker::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 OptDffWorker::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; +} + +YOSYS_NAMESPACE_END diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc deleted file mode 100644 index 391858bca..000000000 --- a/passes/opt/opt_dff.cc +++ /dev/null @@ -1,1668 +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--; - - // 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; - } -}; - -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); - } - } - - // 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 && !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; - } - - // 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 (!is_inactive(sigmap(ff.sig_clr[i]), ff.pol_clr)) - val = combine_const(val, State::S0); - if (!is_inactive(sigmap(ff.sig_set[i]), ff.pol_set)) - val = combine_const(val, State::S1); - } - - return val; - } - - // 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, const ConstObligation &ob) - { - log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n", - ob.val == State::S1 ? 1 : 0, ob.idx, ob.cell, ob.cell->type.unescape(), module); - initvals.remove_init(ob.q); - module->connect(ob.q, ob.val); - const_bits[ob.cell].insert(ob.idx); - } - - bool add_const_target(ConstObligation &ob, SigBit sig) - { - if (!opt.sat || (ob.val != State::S0 && ob.val != State::S1)) - return false; - if (!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 - 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 = sat_budget.solve(qcsat, cap, watches.exprs, model, assumptions); - - if (res == SatEffortBudget::Result::LimitReached) - return false; - if (res == SatEffortBudget::Result::Unsat) { - ob.status = ConstObligation::Proven; - return true; - } - - watches.drop_disproven(model); - ob.status = ConstObligation::Dropped; - return true; - } - - void 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(); - } - - // fold constant D/AD inputs into the candidate value; bits with remaining - // wire inputs get sat proof targets (only when -sat is in effect), bits - // with none are trivially proven - std::vector gather_const_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; - - bool has_d = ff.has_clk || ff.has_gclk; - SigBit d = has_d ? sigmap(ff.sig_d[i]) : SigBit(); - SigBit ad = ff.has_aload ? sigmap(ff.sig_ad[i]) : SigBit(); - - // fold all const inputs first, so the sat targets are checked - // against the final candidate - if (has_d && !d.wire) - val = combine_const(val, d.data); - if (ff.has_aload && !ad.wire) - val = combine_const(val, ad.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 (has_d && d.wire) - feasible = add_const_target(ob, d); - if (feasible && ff.has_aload && ad.wire) - feasible = add_const_target(ob, ad); - if (!feasible) - continue; - - if (ob.targets.empty()) - ob.status = ConstObligation::Proven; - 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) && !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(); - 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 (warn_if_budget_spent()) - return; - if (!resolve_const_obligation(qcsat, cap, ob, watches)) - all_resolved = false; - } - - if (all_resolved) - return; - } - } - - // sat: prove or drop the still-pending obligations in place - void solve_const_obligations(std::vector &obligations) - { - int64_t num_queries = 0; - for (auto &ob : obligations) - num_queries += (ob.status == ConstObligation::Pending); - if (num_queries == 0) - return; - - ModWalker &modwalker = get_modwalker(); - - // screening cap - int64_t screen_cap = 0; - if (sat_budget.enabled()) { - // scale down when we can't afford a full screening round - screen_cap = max((int64_t)20000, min((int64_t)200000, 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) && !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() - { - std::vector obligations = gather_const_obligations(); - - solve_const_obligations(obligations); - - dict> const_bits; - for (auto &ob : obligations) - if (ob.status == ConstObligation::Proven) - commit_const(const_bits, ob); - - for (auto &[cell, drop] : const_bits) - remove_ff_bits(cell, drop); - - return !const_bits.empty(); - } - - 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; - } - }; - - // concrete 0/1 bit, as opposed to x/z - bool is_def(State s) { - return s == State::S0 || s == State::S1; - } - - 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 : module->selected_cells()) { - if (!cell->is_builtin_ff()) - continue; - - FfData ff(&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(module, sigmap, 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[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(module)); - cand.classes.clear(); - } - - void filter_classes_sat(EqCandidates &cand) - { - auto &classes = cand.classes; - auto &bits = cand.bits; - QuickConeSat qcsat(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 (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(); - 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(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 = sat_budget.solve(qcsat, 0, modelExprs, modelVals, assumptions); - - if (res == SatEffortBudget::Result::LimitReached) { - 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]]; - initvals.remove_init(eb.q); - module->connect(eb.q, rep_q); - remove_bits[eb.cell].insert(eb.idx); - } - } - - for (auto &[cell, drop] : remove_bits) - remove_ff_bits(cell, drop); - - return any_change; - } - - bool run_eqbits() - { - if (!opt.sat) - return false; - - 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); - } -}; - -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 From 60da0e8ef065897d292e9bfee908d84b140a10bf Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 12 Aug 2026 18:44:57 +0200 Subject: [PATCH 14/17] opt_clean: move --- passes/opt/{opt_clean => clean}/CMakeLists.txt | 0 passes/opt/{opt_clean => clean}/cells_all.cc | 2 +- passes/opt/{opt_clean => clean}/cells_temp.cc | 2 +- passes/opt/{opt_clean => clean}/inits.cc | 2 +- passes/opt/{opt_clean => clean}/keep_cache.h | 0 passes/opt/{opt_clean => clean}/opt_clean.cc | 2 +- passes/opt/{opt_clean => clean}/opt_clean.h | 2 +- passes/opt/{opt_clean => clean}/wires.cc | 2 +- 8 files changed, 6 insertions(+), 6 deletions(-) rename passes/opt/{opt_clean => clean}/CMakeLists.txt (100%) rename passes/opt/{opt_clean => clean}/cells_all.cc (99%) rename passes/opt/{opt_clean => clean}/cells_temp.cc (98%) rename passes/opt/{opt_clean => clean}/inits.cc (98%) rename passes/opt/{opt_clean => clean}/keep_cache.h (100%) rename passes/opt/{opt_clean => clean}/opt_clean.cc (99%) rename passes/opt/{opt_clean => clean}/opt_clean.h (98%) rename passes/opt/{opt_clean => clean}/wires.cc (99%) 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 From 0c0b6c2bdd87bccdf8df49d21ae85ec6d5641ad8 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 12 Aug 2026 19:02:29 +0200 Subject: [PATCH 15/17] opt_dff: smaller context structs --- passes/opt/dff/constbits.cc | 500 +++++++------- passes/opt/dff/eqbits.cc | 771 +++++++++++----------- passes/opt/dff/opt_dff.cc | 28 +- passes/opt/dff/opt_dff.h | 57 +- passes/opt/dff/simple.cc | 1245 ++++++++++++++++++----------------- 5 files changed, 1304 insertions(+), 1297 deletions(-) diff --git a/passes/opt/dff/constbits.cc b/passes/opt/dff/constbits.cc index 3639dc809..8fb7a4498 100644 --- a/passes/opt/dff/constbits.cc +++ b/passes/opt/dff/constbits.cc @@ -18,281 +18,301 @@ * */ +#include "kernel/ff.h" #include "passes/opt/dff/opt_dff.h" USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN -YOSYS_NAMESPACE_BEGIN - -// lattice join of candidate constants: Sx is the identity (unless -keepdc -// pins it), equal values join, Sm marks a conflict -State OptDffWorker::combine_const(State a, State b) { - if (a == State::Sx && !opt.keepdc) return b; - if (b == State::Sx && !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 OptDffWorker::check_constbit(FfData &ff, int i) +struct ConstBitsContext { - 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 (!is_inactive(sigmap(ff.sig_clr[i]), ff.pol_clr)) - val = combine_const(val, State::S0); - if (!is_inactive(sigmap(ff.sig_set[i]), ff.pol_set)) - val = combine_const(val, State::S1); + 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; } - return val; -} - -// 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 OptDffWorker::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 OptDffWorker::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; + // 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; } -}; -void OptDffWorker::commit_const(dict> &const_bits, const ConstObligation &ob) -{ - log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n", - ob.val == State::S1 ? 1 : 0, ob.idx, ob.cell, ob.cell->type.unescape(), module); - initvals.remove_init(ob.q); - module->connect(ob.q, ob.val); - const_bits[ob.cell].insert(ob.idx); -} + // 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 }; -bool OptDffWorker::add_const_target(ConstObligation &ob, SigBit sig) -{ - if (!opt.sat || (ob.val != State::S0 && ob.val != State::S1)) - return false; - if (!get_modwalker().has_drivers(sig)) - return false; - ob.targets.push_back(sig); - return true; -} + 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; -// try to decide obligation ob under the given per-query effort cap -bool OptDffWorker::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); + int q_lit = -1; // valid within the current batch + int differ_lit = -1; // some target differs from the candidate value + }; - std::vector model; - auto res = sat_budget.solve(qcsat, cap, watches.exprs, model, assumptions); + // 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; - if (res == SatEffortBudget::Result::LimitReached) - return false; - if (res == SatEffortBudget::Result::Unsat) { - ob.status = ConstObligation::Proven; + 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, const ConstObligation &ob) + { + log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n", + ob.val == State::S1 ? 1 : 0, ob.idx, ob.cell, ob.cell->type.unescape(), worker.module); + worker.initvals.remove_init(ob.q); + worker.module->connect(ob.q, ob.val); + const_bits[ob.cell].insert(ob.idx); + } + + bool add_const_target(ConstObligation &ob, SigBit sig) + { + if (!worker.opt.sat || (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; } - watches.drop_disproven(model); - ob.status = ConstObligation::Dropped; - return true; -} - -// fold constant D/AD inputs into the candidate value; bits with remaining -// wire inputs get sat proof targets (only when -sat is in effect), bits -// with none are trivially proven -std::vector OptDffWorker::gather_const_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; - - bool has_d = ff.has_clk || ff.has_gclk; - SigBit d = has_d ? sigmap(ff.sig_d[i]) : SigBit(); - SigBit ad = ff.has_aload ? sigmap(ff.sig_ad[i]) : SigBit(); - - // fold all const inputs first, so the sat targets are checked - // against the final candidate - if (has_d && !d.wire) - val = combine_const(val, d.data); - if (ff.has_aload && !ad.wire) - val = combine_const(val, ad.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 (has_d && d.wire) - feasible = add_const_target(ob, d); - if (feasible && ff.has_aload && ad.wire) - feasible = add_const_target(ob, ad); - if (!feasible) - continue; - - if (ob.targets.empty()) - ob.status = ConstObligation::Proven; - obligations.push_back(std::move(ob)); - } - } - - return obligations; -} - -int OptDffWorker::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) && !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); + // try to decide obligation ob under the given per-query effort cap + 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 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(); - sat_budget.charge_import(qcsat, cells_charged); - batch_end++; - } + std::vector assumptions; + assumptions.push_back(qcsat.ez->IFF(ob.q_lit, vlit)); + assumptions.push_back(ob.differ_lit); - return batch_end; -} + std::vector model; + auto res = worker.sat_budget.solve(qcsat, cap, watches.exprs, model, assumptions); -// sweep the batch under the cheap screening cap first, then re-sweep the -// still-undecided obligations with the full remaining budget -void OptDffWorker::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); + if (res == SatEffortBudget::Result::LimitReached) + return false; + if (res == SatEffortBudget::Result::Unsat) { + ob.status = ConstObligation::Proven; + return true; } - for (int obi = batch_begin; obi < batch_end; obi++) { - auto &ob = obligations[obi]; - if (ob.status != ConstObligation::Pending) + watches.drop_disproven(model); + ob.status = ConstObligation::Dropped; + return true; + } + + // fold constant D/AD inputs into the candidate value; bits with remaining + // wire inputs get sat proof targets (only when -sat is in effect), bits + // with none are trivially proven + std::vector gather_const_obligations() + { + std::vector obligations; + + for (auto cell : worker.module->selected_cells()) { + if (!cell->is_builtin_ff()) continue; - if (warn_if_budget_spent()) - return; - if (!resolve_const_obligation(qcsat, cap, ob, watches)) - all_resolved = false; + + FfData ff(&worker.initvals, cell); + + for (int i = 0; i < ff.width; i++) { + State val = check_constbit(ff, i); + if (val == State::Sm) + continue; + + 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(); + + // fold all const inputs first, so the sat targets are checked + // against the final candidate + if (has_d && !d.wire) + val = combine_const(val, d.data); + if (ff.has_aload && !ad.wire) + val = combine_const(val, ad.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 (has_d && d.wire) + feasible = add_const_target(ob, d); + if (feasible && ff.has_aload && ad.wire) + feasible = add_const_target(ob, ad); + if (!feasible) + continue; + + if (ob.targets.empty()) + ob.status = ConstObligation::Proven; + obligations.push_back(std::move(ob)); + } } - if (all_resolved) + 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(); + 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; + if (!resolve_const_obligation(qcsat, cap, ob, watches)) + all_resolved = false; + } + + if (all_resolved) + return; + } + } + + // sat: prove or drop the still-pending obligations in place + void solve_const_obligations(std::vector &obligations) + { + int64_t num_queries = 0; + for (auto &ob : obligations) + num_queries += (ob.status == ConstObligation::Pending); + if (num_queries == 0) return; - } -} -// sat: prove or drop the still-pending obligations in place -void OptDffWorker::solve_const_obligations(std::vector &obligations) -{ - int64_t num_queries = 0; - for (auto &ob : obligations) - num_queries += (ob.status == ConstObligation::Pending); - if (num_queries == 0) - return; + ModWalker &modwalker = worker.get_modwalker(); - ModWalker &modwalker = 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))); + } - // screening cap - int64_t screen_cap = 0; - if (sat_budget.enabled()) { - // scale down when we can't afford a full screening round - screen_cap = max((int64_t)20000, min((int64_t)200000, 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; + } } - // 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) && !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() + { + std::vector obligations = gather_const_obligations(); + + solve_const_obligations(obligations); + + dict> const_bits; + for (auto &ob : obligations) + if (ob.status == ConstObligation::Proven) + commit_const(const_bits, ob); + + 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() { - std::vector obligations = gather_const_obligations(); - - solve_const_obligations(obligations); - - dict> const_bits; - for (auto &ob : obligations) - if (ob.status == ConstObligation::Proven) - commit_const(const_bits, ob); - - for (auto &[cell, drop] : const_bits) - remove_ff_bits(cell, drop); - - return !const_bits.empty(); + return ConstBitsContext(*this).run_constbits(); } YOSYS_NAMESPACE_END diff --git a/passes/opt/dff/eqbits.cc b/passes/opt/dff/eqbits.cc index 86fc917b3..864298925 100644 --- a/passes/opt/dff/eqbits.cc +++ b/passes/opt/dff/eqbits.cc @@ -18,6 +18,7 @@ * */ +#include "kernel/ff.h" #include "passes/opt/dff/opt_dff.h" USING_YOSYS_NAMESPACE @@ -110,391 +111,403 @@ 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(); + 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() + { + if (!worker.opt.sat) + return false; + + 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 -struct OptDffWorker::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 OptDffWorker::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 OptDffWorker::EqCandidates { - std::vector bits; - dict ffs; - std::vector> classes; -}; - -OptDffWorker::EqCandidates OptDffWorker::gather_initial_eq_classes() -{ - EqCandidates cand; - 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; - - 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 OptDffWorker::filter_classes_sim(EqCandidates &cand) -{ - BitSim sim(module, sigmap, 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[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 OptDffWorker::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(module)); - cand.classes.clear(); -} - -void OptDffWorker::filter_classes_sat(EqCandidates &cand) -{ - auto &classes = cand.classes; - auto &bits = cand.bits; - QuickConeSat qcsat(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 (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(); - 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(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 = sat_budget.solve(qcsat, 0, modelExprs, modelVals, assumptions); - - if (res == SatEffortBudget::Result::LimitReached) { - 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 OptDffWorker::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]]; - initvals.remove_init(eb.q); - module->connect(eb.q, rep_q); - remove_bits[eb.cell].insert(eb.idx); - } - } - - for (auto &[cell, drop] : remove_bits) - remove_ff_bits(cell, drop); - - return any_change; -} - bool OptDffWorker::run_eqbits() { - if (!opt.sat) - return false; - - 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); + return EqBitsContext(*this).run_eqbits(); } YOSYS_NAMESPACE_END diff --git a/passes/opt/dff/opt_dff.cc b/passes/opt/dff/opt_dff.cc index 1d12327ad..3f1b70647 100644 --- a/passes/opt/dff/opt_dff.cc +++ b/passes/opt/dff/opt_dff.cc @@ -20,6 +20,7 @@ #include "kernel/log.h" #include "kernel/register.h" +#include "kernel/ff.h" #include "passes/opt/dff/opt_dff.h" #include #include @@ -32,33 +33,6 @@ 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)); - - // 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); - } } void OptDffWorker::remove_ff_bits(Cell *cell, const pool &drop) diff --git a/passes/opt/dff/opt_dff.h b/passes/opt/dff/opt_dff.h index 34db52d3d..837c9297d 100644 --- a/passes/opt/dff/opt_dff.h +++ b/passes/opt/dff/opt_dff.h @@ -24,8 +24,6 @@ #include "kernel/modtools.h" #include "kernel/sigtools.h" #include "kernel/ffinit.h" -#include "kernel/ff.h" -#include "kernel/pattern.h" #ifndef OPT_DFF_H #define OPT_DFF_H @@ -46,19 +44,8 @@ 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; @@ -66,6 +53,8 @@ struct OptDffWorker // 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) @@ -102,52 +91,10 @@ struct OptDffWorker return is_inactive(sig, pol) || (!opt.keepdc && sig == State::Sx); } - OptDffWorker(const OptDffOptions &opt, Module *mod); - void remove_ff_bits(Cell *cell, const pool &drop); - SigSpec create_not(SigSpec a, bool is_fine); - SigSpec create_and(SigSpec a, SigSpec b, bool is_fine); - void create_mux_to_output(SigSpec a, SigSpec b, SigSpec sel, SigSpec y, bool pol, bool is_fine); - void maybe_simplemap(Cell *c, bool make_gates); - patterns_t find_muxtree_feedback_patterns(RTLIL::SigBit d, RTLIL::SigBit q, pattern_t path); - ctrl_t make_patterns_logic(const patterns_t &patterns, const ctrls_t &ctrls, bool make_gates); - ctrl_t combine_resets(const ctrls_t &ctrls, bool make_gates); - bool signal_all_same(const SigSpec &sig); - bool optimize_sr(FfData &ff, Cell *cell, bool &changed); - bool optimize_aload(FfData &ff, Cell *cell, bool &changed); - bool optimize_arst(FfData &ff, Cell *cell, bool &changed); - void optimize_srst(FfData &ff, Cell *cell, bool &changed); - void optimize_ce(FfData &ff, Cell *cell, bool &changed); - void optimize_const_clk(FfData &ff, Cell *cell, bool &changed); - void optimize_d_equals_q(FfData &ff, Cell *cell, bool &changed); - bool try_merge_srst(FfData &ff, Cell *cell, bool &changed); - bool try_merge_ce(FfData &ff, Cell *cell, bool &changed); bool run(); - - struct ConstObligation; - struct ConstWatchList; - State combine_const(State a, State b); - State check_constbit(FfData &ff, int i); - void commit_const(dict> &const_bits, const ConstObligation &ob); - bool add_const_target(ConstObligation &ob, SigBit sig); - bool resolve_const_obligation(QuickConeSat &qcsat, int64_t cap, ConstObligation &ob, - const ConstWatchList &watches); - std::vector gather_const_obligations(); - int build_const_batch(QuickConeSat &qcsat, std::vector &obligations, int batch_begin); - void sweep_const_batch(QuickConeSat &qcsat, std::vector &obligations, - int batch_begin, int batch_end, int64_t screen_cap); - void solve_const_obligations(std::vector &obligations); bool run_constbits(); - - struct EqBit; - struct SigKey; - struct EqCandidates; - EqCandidates gather_initial_eq_classes(); - void filter_classes_sim(EqCandidates &cand); - void drop_all_classes(EqCandidates &cand); - void filter_classes_sat(EqCandidates &cand); - bool apply_eq_merges(const EqCandidates &cand); bool run_eqbits(); }; diff --git a/passes/opt/dff/simple.cc b/passes/opt/dff/simple.cc index 69f875866..9d0a6faef 100644 --- a/passes/opt/dff/simple.cc +++ b/passes/opt/dff/simple.cc @@ -18,698 +18,751 @@ * */ +#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 -YOSYS_NAMESPACE_BEGIN - -SigSpec OptDffWorker::create_not(SigSpec a, bool is_fine) { - if (is_fine) - return module->NotGate(NEW_ID, a); - else - return module->Not(NEW_ID, a); -} - -SigSpec OptDffWorker::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 OptDffWorker::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 OptDffWorker::maybe_simplemap(Cell *c, bool make_gates) { - if (make_gates) { - simplemap(module, c); - module->remove(c); - } -} - -patterns_t OptDffWorker::find_muxtree_feedback_patterns(RTLIL::SigBit d, RTLIL::SigBit q, pattern_t path) +struct SimpleContext { - // Find feedback paths D->Q through mux tree, replacing found paths with Sx - patterns_t ret; + OptDffWorker &worker; - if (d == q) { - ret.insert(path); - return ret; // Feedback found + // 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); + } } - if (bit2mux.count(d) == 0 || bitusers[d] > 1) - return ret; // D not driven by MUX / MUX drives multiple loads + 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); + } - 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; + 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); - // 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)) + // Selected when S=0 + for (auto &pat : find_muxtree_feedback_patterns(sig_a[index], q, path_else)) 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 OptDffWorker::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); + if (sig_a[index] == q) { + RTLIL::SigSpec s = mbit.first->getPort(ID::A); + s[index] = RTLIL::Sx; + mbit.first->setPort(ID::A, s); } - 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); + return ret; } - // 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)); - } + 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(); - if (GetSize(or_input) == 0) return ctrl_t(State::S1, true); - if (GetSize(or_input) == 1) return ctrl_t(or_input, true); + RTLIL::SigSpec or_input; - 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); -} + // Build logic for each feedback pattern + for (auto pat : patterns) { + RTLIL::SigSpec s1, s2; -ctrl_t OptDffWorker::combine_resets(const ctrls_t &ctrls, bool make_gates) -{ - if (GetSize(ctrls) == 1) - return *ctrls.begin(); + for (auto it : pat) { + s1.append(it.first); + s2.append(it.second); + } - bool final_pol = false; - for (auto item : ctrls) - if (item.second) - final_pol = true; + 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); + } - 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 OptDffWorker::signal_all_same(const SigSpec &sig) { - for (int i = 1; i < GetSize(sig); i++) - if (sig[i] != sig[0]) - return false; - return true; -} - -bool OptDffWorker::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]); + // Add existing control signals + for (auto item : ctrls) { + if (item.second) + or_input.append(item.first); 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); + 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); } - if (sr_removed) { - if (keep_bits.empty()) { - module->remove(cell); - return true; // FF fully removed + 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)); } - ff = ff.slice(keep_bits); - ff.cell = cell; - changed = true; + + 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); } - // 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(); + bool signal_all_same(const SigSpec &sig) { + for (int i = 1; i < GetSize(sig); i++) + if (sig[i] != sig[0]) + return false; + return true; + } - 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 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; - bool failed = false; - Const::Builder val_arst_builder(ff.width); + // Check for constant Set/Clear inputs 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 (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 (!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; + 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; } - } - return false; -} + // 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; + } + } -bool OptDffWorker::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); + 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; } - return true; + + 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; } - // 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; + 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; } - return false; -} - -bool OptDffWorker::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 OptDffWorker::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 OptDffWorker::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; + 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; - } 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); + } + } + + 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 { + } 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; } - } 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 OptDffWorker::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 OptDffWorker::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 OptDffWorker::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; + 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 { - break; + 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; } - - 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(); + 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 (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]]); + for (int i = 0; i < ff.width; i++) { + ctrls_t resets; + State reset_val = ff.has_srst ? ff.val_srst[i] : State::Sx; - new_ff.val_srst = new_val_srst_builder.build(); + 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; - 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; + 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]; - Cell *new_cell = new_ff.emit(); - if (new_cell) - dff_cells.push_back(new_cell); + if ((a == State::S0 || a == State::S1) && (b == State::S0 || b == State::S1)) + break; - 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)); - } + bool b_const = (b == State::S0 || b == State::S1); + bool a_const = (a == State::S0 || a == State::S1); - if (remaining_indices.empty()) { - module->remove(cell); - return true; - } + 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 (GetSize(remaining_indices) != ff.width) { - ff = ff.slice(remaining_indices); - ff.cell = cell; - changed = true; - } + if (!resets.empty()) { + if (ff.has_srst) + resets.insert(ctrl_t(ff.sig_srst, ff.pol_srst)); - return false; -} - -bool OptDffWorker::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; + groups[resets].push_back(i); } else { - break; + remaining_indices.push_back(i); } + + val_srst_builder.push_back(reset_val); } - patterns_t patterns; - if (!opt.simple_dffe) - patterns = find_muxtree_feedback_patterns(ff.sig_d[i], ff.sig_q[i], pattern_t()); + Const val_srst = val_srst_builder.build(); - 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); + 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]]); - 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.val_srst = new_val_srst_builder.build(); - new_ff.has_ce = true; - new_ff.sig_ce = en.first; - new_ff.pol_ce = en.second; - new_ff.ce_over_srst = false; + 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); + 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 OptDffWorker::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; + 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)); } - // Async control signal opt - if (ff.has_sr && optimize_sr(ff, cell, changed)) { - did_something = true; - continue; + if (remaining_indices.empty()) { + worker.module->remove(cell); + return true; } - 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; + if (GetSize(remaining_indices) != ff.width) { + ff = ff.slice(remaining_indices); + ff.cell = cell; 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 false; } - return did_something; + 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 From d26f1a85733303adabfe9cd662d40effaed6884c Mon Sep 17 00:00:00 2001 From: nella Date: Sun, 16 Aug 2026 00:24:31 +0200 Subject: [PATCH 16/17] Review fixups Co-authored-by: Emil J. Tywoniak --- kernel/qcsat.cc | 4 ++-- kernel/qcsat.h | 4 ++-- passes/opt/dff/constbits.cc | 24 +++++++++++++++++------- passes/opt/dff/eqbits.cc | 5 +---- passes/opt/dff/opt_dff.cc | 4 +++- 5 files changed, 25 insertions(+), 16 deletions(-) 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/dff/constbits.cc b/passes/opt/dff/constbits.cc index 8fb7a4498..9abc77fa3 100644 --- a/passes/opt/dff/constbits.cc +++ b/passes/opt/dff/constbits.cc @@ -111,9 +111,11 @@ struct ConstBitsContext const_bits[ob.cell].insert(ob.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 (!worker.opt.sat || (ob.val != State::S0 && ob.val != State::S1)) + if (ob.val != State::S0 && ob.val != State::S1) return false; if (!worker.get_modwalker().has_drivers(sig)) return false; @@ -121,7 +123,8 @@ struct ConstBitsContext return true; } - // try to decide obligation ob under the given per-query effort cap + // 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) { @@ -137,15 +140,15 @@ struct ConstBitsContext auto res = worker.sat_budget.solve(qcsat, cap, watches.exprs, model, assumptions); if (res == SatEffortBudget::Result::LimitReached) - return false; + return true; if (res == SatEffortBudget::Result::Unsat) { ob.status = ConstObligation::Proven; - return true; + return false; } watches.drop_disproven(model); ob.status = ConstObligation::Dropped; - return true; + return false; } // fold constant D/AD inputs into the candidate value; bits with remaining @@ -179,6 +182,12 @@ struct ConstBitsContext if (val == State::Sm) continue; + // remaining wire inputs need a sat proof, without -sat only + // bits with all-constant inputs are candidates (proven trivially) + bool needs_sat = (has_d && d.wire) || (ff.has_aload && ad.wire); + if (needs_sat && !worker.opt.sat) + continue; + ConstObligation ob; ob.cell = cell; ob.idx = i; @@ -222,7 +231,7 @@ struct ConstBitsContext differ.push_back(qcsat.ez->NOT(qcsat.ez->IFF(qcsat.importSigBit(sig), vlit))); ob.differ_lit = qcsat.ez->expression(ezSAT::OpOr, differ); qcsat.prepare(); - worker.sat_budget.charge_import(qcsat, cells_charged); + cells_charged = worker.sat_budget.charge_import(qcsat, cells_charged); batch_end++; } @@ -251,7 +260,8 @@ struct ConstBitsContext continue; if (worker.warn_if_budget_spent()) return; - if (!resolve_const_obligation(qcsat, cap, ob, watches)) + bool given_up = resolve_const_obligation(qcsat, cap, ob, watches); + if (given_up) all_resolved = false; } diff --git a/passes/opt/dff/eqbits.cc b/passes/opt/dff/eqbits.cc index 864298925..c0b8d8dbe 100644 --- a/passes/opt/dff/eqbits.cc +++ b/passes/opt/dff/eqbits.cc @@ -361,7 +361,7 @@ struct EqBitsContext n_lit[idx] = n; } qcsat.prepare(); - worker.sat_budget.charge_import(qcsat, cells_charged); + 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 @@ -480,9 +480,6 @@ struct EqBitsContext bool run_eqbits() { - if (!worker.opt.sat) - return false; - EqCandidates cand = gather_initial_eq_classes(); if (cand.classes.empty()) return false; diff --git a/passes/opt/dff/opt_dff.cc b/passes/opt/dff/opt_dff.cc index 3f1b70647..4e6d459df 100644 --- a/passes/opt/dff/opt_dff.cc +++ b/passes/opt/dff/opt_dff.cc @@ -128,9 +128,11 @@ struct OptDffPass : public Pass { 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 (worker.run_eqbits()) + if (opt.sat && worker.run_eqbits()) did_something = true; } From e0bf46ebc5ffaf0851a6657ee03ab7c59813edfb Mon Sep 17 00:00:00 2001 From: nella Date: Thu, 27 Aug 2026 19:10:15 +0200 Subject: [PATCH 17/17] Separate non -sat constbits. --- passes/opt/dff/constbits.cc | 115 +++++++++++++++++++------------ tests/opt/opt_dff_const_nosat.ys | 24 +++++++ 2 files changed, 95 insertions(+), 44 deletions(-) create mode 100644 tests/opt/opt_dff_const_nosat.ys diff --git a/passes/opt/dff/constbits.cc b/passes/opt/dff/constbits.cc index 9abc77fa3..4345c17b8 100644 --- a/passes/opt/dff/constbits.cc +++ b/passes/opt/dff/constbits.cc @@ -63,6 +63,15 @@ struct ConstBitsContext 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 { @@ -102,13 +111,13 @@ struct ConstBitsContext } }; - void commit_const(dict> &const_bits, const ConstObligation &ob) + 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", - ob.val == State::S1 ? 1 : 0, ob.idx, ob.cell, ob.cell->type.unescape(), worker.module); - worker.initvals.remove_init(ob.q); - worker.module->connect(ob.q, ob.val); - const_bits[ob.cell].insert(ob.idx); + 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 @@ -151,10 +160,40 @@ struct ConstBitsContext return false; } - // fold constant D/AD inputs into the candidate value; bits with remaining - // wire inputs get sat proof targets (only when -sat is in effect), bits - // with none are trivially proven - std::vector gather_const_obligations() + // 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; @@ -165,45 +204,32 @@ struct ConstBitsContext FfData ff(&worker.initvals, cell); for (int i = 0; i < ff.width; i++) { - State val = check_constbit(ff, i); - if (val == State::Sm) + ConstCandidate cand = fold_const_inputs(ff, i); + if (cand.val == State::Sm) continue; - 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(); - - // fold all const inputs first, so the sat targets are checked - // against the final candidate - if (has_d && !d.wire) - val = combine_const(val, d.data); - if (ff.has_aload && !ad.wire) - val = combine_const(val, ad.data); - if (val == State::Sm) + if (!cand.needs_proof()) { + commit_const(const_bits, cell, i, ff.sig_q[i], cand.val); continue; + } - // remaining wire inputs need a sat proof, without -sat only - // bits with all-constant inputs are candidates (proven trivially) - bool needs_sat = (has_d && d.wire) || (ff.has_aload && ad.wire); - if (needs_sat && !worker.opt.sat) + if (!worker.opt.sat) continue; ConstObligation ob; ob.cell = cell; ob.idx = i; - ob.val = val; + ob.val = cand.val; ob.q = ff.sig_q[i]; bool feasible = true; - if (has_d && d.wire) - feasible = add_const_target(ob, d); - if (feasible && ff.has_aload && ad.wire) - feasible = add_const_target(ob, ad); + 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; - if (ob.targets.empty()) - ob.status = ConstObligation::Proven; obligations.push_back(std::move(ob)); } } @@ -270,12 +296,11 @@ struct ConstBitsContext } } - // sat: prove or drop the still-pending obligations in place + // sat: prove or drop the pending obligations in place void solve_const_obligations(std::vector &obligations) { - int64_t num_queries = 0; - for (auto &ob : obligations) - num_queries += (ob.status == ConstObligation::Pending); + log_assert(worker.opt.sat); + int64_t num_queries = GetSize(obligations); if (num_queries == 0) return; @@ -300,14 +325,16 @@ struct ConstBitsContext bool run_constbits() { - std::vector obligations = gather_const_obligations(); - - solve_const_obligations(obligations); - dict> const_bits; - for (auto &ob : obligations) - if (ob.status == ConstObligation::Proven) - commit_const(const_bits, ob); + + 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); 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 <