mirror of
https://github.com/YosysHQ/yosys
synced 2026-06-27 11:08:48 +00:00
Merge 46cbeab720 into 5d7486115a
This commit is contained in:
nella
GitHub
commit
74b4afeaa1
4 changed files with 795 additions and 0 deletions
|
|
@ -43,6 +43,91 @@ struct OptDffOptions
|
|||
bool keepdc;
|
||||
};
|
||||
|
||||
// Bit-parallel random simulation used as a cheap pre-filter for equivalence
|
||||
struct BitSim {
|
||||
Module *module;
|
||||
SigMap &sigmap;
|
||||
ModWalker &modwalker;
|
||||
dict<SigBit, uint64_t> sim_vals;
|
||||
uint64_t rng_state;
|
||||
int max_depth;
|
||||
int evals_left;
|
||||
|
||||
BitSim(Module *m, SigMap &sm, ModWalker &mw)
|
||||
: module(m), sigmap(sm), modwalker(mw), rng_state(1337)
|
||||
{
|
||||
max_depth = module->design->scratchpad_get_int("opt_dff.sim_depth", 10000);
|
||||
evals_left = module->design->scratchpad_get_int("opt_dff.sim_evals", 1000000);
|
||||
}
|
||||
|
||||
uint64_t next_rand() {
|
||||
uint32_t lo = mkhash_xorshift((uint32_t)rng_state);
|
||||
uint32_t hi = mkhash_xorshift((uint32_t)(rng_state >> 32) ^ lo);
|
||||
rng_state = ((uint64_t)hi << 32) | lo;
|
||||
return rng_state;
|
||||
}
|
||||
|
||||
uint64_t eval_bit(SigBit b, int depth = 0) {
|
||||
SigBit mapped = sigmap(b);
|
||||
if (mapped == State::S0) return 0ULL;
|
||||
if (mapped == State::S1) return ~0ULL;
|
||||
if (mapped == State::Sx || mapped == State::Sz) return 0ULL;
|
||||
|
||||
auto it = sim_vals.find(mapped);
|
||||
if (it != sim_vals.end()) return it->second;
|
||||
|
||||
// Failsafe for huge designs
|
||||
if (depth >= max_depth || evals_left <= 0) {
|
||||
uint64_t r = next_rand();
|
||||
sim_vals[mapped] = r;
|
||||
return r;
|
||||
}
|
||||
evals_left--;
|
||||
|
||||
sim_vals[mapped] = 0;
|
||||
uint64_t res = 0;
|
||||
|
||||
if (!modwalker.has_drivers(mapped)) {
|
||||
res = next_rand();
|
||||
} else {
|
||||
auto &drivers = modwalker.signal_drivers[mapped];
|
||||
if (drivers.empty()) {
|
||||
res = next_rand();
|
||||
} else {
|
||||
auto driver = *drivers.begin();
|
||||
Cell *cell = driver.cell;
|
||||
|
||||
if (cell->is_builtin_ff()) {
|
||||
res = next_rand();
|
||||
} else if (cell->type == ID($_AND_)) {
|
||||
res = eval_bit(cell->getPort(ID::A)[0], depth+1) & eval_bit(cell->getPort(ID::B)[0], depth+1);
|
||||
} else if (cell->type == ID($_OR_)) {
|
||||
res = eval_bit(cell->getPort(ID::A)[0], depth+1) | eval_bit(cell->getPort(ID::B)[0], depth+1);
|
||||
} else if (cell->type == ID($_XOR_)) {
|
||||
res = eval_bit(cell->getPort(ID::A)[0], depth+1) ^ eval_bit(cell->getPort(ID::B)[0], depth+1);
|
||||
} else if (cell->type == ID($_NOT_)) {
|
||||
res = ~eval_bit(cell->getPort(ID::A)[0], depth+1);
|
||||
} else if (cell->type == ID($_MUX_)) {
|
||||
uint64_t s = eval_bit(cell->getPort(ID::S)[0], depth+1);
|
||||
uint64_t a = eval_bit(cell->getPort(ID::A)[0], depth+1);
|
||||
uint64_t b = eval_bit(cell->getPort(ID::B)[0], depth+1);
|
||||
res = (a & ~s) | (b & s);
|
||||
} else if (cell->type == ID($mux)) {
|
||||
uint64_t s = eval_bit(cell->getPort(ID::S)[0], depth+1);
|
||||
uint64_t a = eval_bit(cell->getPort(ID::A)[driver.offset], depth+1);
|
||||
uint64_t b = eval_bit(cell->getPort(ID::B)[driver.offset], depth+1);
|
||||
res = (a & ~s) | (b & s);
|
||||
} else {
|
||||
res = next_rand();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
sim_vals[mapped] = res;
|
||||
return res;
|
||||
}
|
||||
};
|
||||
|
||||
struct OptDffWorker
|
||||
{
|
||||
const OptDffOptions &opt;
|
||||
|
|
@ -919,6 +1004,397 @@ struct OptDffWorker
|
|||
|
||||
return did_something;
|
||||
}
|
||||
|
||||
struct EqBit {
|
||||
Cell *cell;
|
||||
int idx;
|
||||
SigBit q;
|
||||
};
|
||||
|
||||
// NOTE: This intentionally duplicates a subset of FfData, as flattening just the
|
||||
// fields that matter for merging into a single comparable/hashable key is cheaper
|
||||
struct SigKey {
|
||||
enum Flag : uint16_t {
|
||||
InitOne = 1u << 0,
|
||||
InitX = 1u << 1,
|
||||
PolClk = 1u << 2,
|
||||
PolCe = 1u << 3,
|
||||
PolSrst = 1u << 4,
|
||||
PolArst = 1u << 5,
|
||||
PolAload = 1u << 6,
|
||||
PolClr = 1u << 7,
|
||||
PolSet = 1u << 8,
|
||||
CeOverSrst = 1u << 9,
|
||||
};
|
||||
|
||||
SigBit clk, ce, srst, arst, aload, clr, set;
|
||||
IdString cell_type; // for SR
|
||||
uint16_t flags;
|
||||
|
||||
bool operator==(const SigKey &o) const {
|
||||
return flags == o.flags && clk == o.clk && ce == o.ce && srst == o.srst && arst == o.arst
|
||||
&& aload == o.aload && clr == o.clr && set == o.set && cell_type == o.cell_type;
|
||||
}
|
||||
|
||||
Hasher hash_into(Hasher h) const {
|
||||
h.eat(flags);
|
||||
h.eat(clk);
|
||||
h.eat(ce);
|
||||
h.eat(srst);
|
||||
h.eat(arst);
|
||||
h.eat(aload);
|
||||
h.eat(clr);
|
||||
h.eat(set);
|
||||
h.eat(cell_type);
|
||||
return h;
|
||||
}
|
||||
};
|
||||
|
||||
bool is_def(State s) {
|
||||
// Concrete constant bit (0 or 1), as opposed to x/z
|
||||
return s == State::S0 || s == State::S1;
|
||||
}
|
||||
|
||||
std::vector<std::vector<int>> gather_initial_eq_classes(std::vector<EqBit> &bits, dict<Cell *, FfData> &ff_for_cell)
|
||||
{
|
||||
std::vector<SigKey> keys;
|
||||
|
||||
// Collect FF bits eligible for merging
|
||||
for (auto cell : module->selected_cells()) {
|
||||
if (!cell->is_builtin_ff())
|
||||
continue;
|
||||
|
||||
FfData ff(&initvals, cell);
|
||||
if (!ff.has_clk && !ff.has_gclk)
|
||||
continue;
|
||||
|
||||
ff_for_cell.emplace(cell, ff);
|
||||
|
||||
for (int i = 0; i < ff.width; i++) {
|
||||
// Skip bits whose reset drives an undefined (x) value
|
||||
if (ff.has_srst && !is_def(ff.val_srst[i])) continue;
|
||||
if (ff.has_arst && !is_def(ff.val_arst[i])) continue;
|
||||
|
||||
// Class members are assumed equal in the current cycle and proven equal in the next, which needs
|
||||
// a base case anchoring them to a common known value
|
||||
bool def_init = is_def(ff.val_init[i]);
|
||||
if (!def_init && !ff.has_srst && !ff.has_arst)
|
||||
continue;
|
||||
|
||||
SigKey k = {};
|
||||
|
||||
// Flags
|
||||
if (def_init && ff.val_init[i] == State::S1)
|
||||
k.flags |= SigKey::InitOne;
|
||||
else if (!def_init)
|
||||
k.flags |= SigKey::InitX;
|
||||
|
||||
if (ff.has_clk) {
|
||||
k.clk = ff.sig_clk;
|
||||
if (ff.pol_clk) k.flags |= SigKey::PolClk;
|
||||
}
|
||||
if (ff.has_ce) {
|
||||
k.ce = ff.sig_ce;
|
||||
if (ff.pol_ce) k.flags |= SigKey::PolCe;
|
||||
}
|
||||
if (ff.has_srst) {
|
||||
k.srst = ff.sig_srst;
|
||||
if (ff.pol_srst) k.flags |= SigKey::PolSrst;
|
||||
if (ff.ce_over_srst) k.flags |= SigKey::CeOverSrst;
|
||||
}
|
||||
if (ff.has_arst) {
|
||||
k.arst = ff.sig_arst;
|
||||
if (ff.pol_arst) k.flags |= SigKey::PolArst;
|
||||
}
|
||||
if (ff.has_aload) {
|
||||
k.aload = ff.sig_aload;
|
||||
if (ff.pol_aload) k.flags |= SigKey::PolAload;
|
||||
}
|
||||
if (ff.has_sr) {
|
||||
k.clr = ff.sig_clr[i];
|
||||
k.set = ff.sig_set[i];
|
||||
k.cell_type = cell->type;
|
||||
if (ff.pol_clr) k.flags |= SigKey::PolClr;
|
||||
if (ff.pol_set) k.flags |= SigKey::PolSet;
|
||||
}
|
||||
|
||||
bits.push_back({cell, i, ff.sig_q[i]});
|
||||
keys.push_back(k);
|
||||
}
|
||||
}
|
||||
|
||||
dict<SigKey, std::vector<int>> buckets;
|
||||
for (int i = 0; i < GetSize(bits); i++)
|
||||
buckets[keys[i]].push_back(i);
|
||||
|
||||
std::vector<std::vector<int>> classes;
|
||||
for (auto &kv : buckets)
|
||||
if (GetSize(kv.second) >= 2)
|
||||
classes.push_back(std::move(kv.second));
|
||||
|
||||
return classes;
|
||||
}
|
||||
|
||||
std::vector<std::vector<int>> filter_classes_sim(
|
||||
const std::vector<std::vector<int>> &classes,
|
||||
const std::vector<EqBit> &bits,
|
||||
const dict<Cell *, FfData> &ff_for_cell,
|
||||
ModWalker &modwalker
|
||||
) {
|
||||
BitSim sim(module, sigmap, modwalker);
|
||||
|
||||
// Assume same class
|
||||
for (auto &cls : classes) {
|
||||
uint64_t class_q_val = sim.next_rand();
|
||||
for (int idx : cls) {
|
||||
sim.sim_vals[sigmap(bits[idx].q)] = class_q_val;
|
||||
}
|
||||
}
|
||||
|
||||
std::vector<std::vector<int>> refined_classes;
|
||||
for (auto &cls : classes) {
|
||||
dict<uint64_t, std::vector<int>> sim_buckets;
|
||||
for (int idx : cls) {
|
||||
const EqBit &eb = bits[idx];
|
||||
const FfData &ff = ff_for_cell.at(eb.cell);
|
||||
uint64_t n_val = sim.eval_bit(ff.sig_d[eb.idx]);
|
||||
|
||||
if (ff.has_aload) {
|
||||
uint64_t al = sim.eval_bit(ff.sig_aload);
|
||||
if (!ff.pol_aload) al = ~al;
|
||||
uint64_t ad = sim.eval_bit(ff.sig_ad[eb.idx]);
|
||||
n_val = (n_val & ~al) | (ad & al);
|
||||
}
|
||||
if (ff.has_arst) {
|
||||
uint64_t ar = sim.eval_bit(ff.sig_arst);
|
||||
if (!ff.pol_arst) ar = ~ar;
|
||||
uint64_t ar_val = (ff.val_arst[eb.idx] == State::S1) ? ~0ULL : 0ULL;
|
||||
n_val = (n_val & ~ar) | (ar_val & ar);
|
||||
}
|
||||
if (ff.has_sr) {
|
||||
uint64_t clr = sim.eval_bit(ff.sig_clr[eb.idx]);
|
||||
if (!ff.pol_clr) clr = ~clr;
|
||||
uint64_t set = sim.eval_bit(ff.sig_set[eb.idx]);
|
||||
if (!ff.pol_set) set = ~set;
|
||||
n_val = ~clr & (set | n_val);
|
||||
}
|
||||
if (ff.has_srst) {
|
||||
uint64_t srst = sim.eval_bit(ff.sig_srst);
|
||||
if (!ff.pol_srst) srst = ~srst;
|
||||
uint64_t srst_val = (ff.val_srst[eb.idx] == State::S1) ? ~0ULL : 0ULL;
|
||||
n_val = (n_val & ~srst) | (srst_val & srst);
|
||||
}
|
||||
|
||||
sim_buckets[n_val].push_back(idx);
|
||||
}
|
||||
|
||||
for (auto &kv : sim_buckets)
|
||||
if (GetSize(kv.second) >= 2)
|
||||
refined_classes.push_back(std::move(kv.second));
|
||||
}
|
||||
|
||||
return refined_classes;
|
||||
}
|
||||
|
||||
std::vector<std::vector<int>> filter_classes_sat(
|
||||
std::vector<std::vector<int>> classes,
|
||||
const std::vector<EqBit> &bits,
|
||||
const dict<Cell *, FfData> &ff_for_cell,
|
||||
ModWalker &modwalker
|
||||
) {
|
||||
QuickConeSat qcsat(modwalker);
|
||||
std::vector<int> q_lit(bits.size(), -1);
|
||||
std::vector<int> 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)
|
||||
|
||||
// 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) {
|
||||
for (int idx : cls) {
|
||||
const EqBit &eb = bits[idx];
|
||||
const FfData &ff = ff_for_cell.at(eb.cell);
|
||||
q_lit[idx] = qcsat.importSigBit(eb.q);
|
||||
int n = qcsat.importSigBit(ff.sig_d[eb.idx]);
|
||||
|
||||
if (ff.has_aload) {
|
||||
int al = qcsat.importSigBit(ff.sig_aload);
|
||||
if (!ff.pol_aload) al = qcsat.ez->NOT(al);
|
||||
n = qcsat.ez->ITE(al, qcsat.importSigBit(ff.sig_ad[eb.idx]), n);
|
||||
}
|
||||
if (ff.has_arst) {
|
||||
int ar = qcsat.importSigBit(ff.sig_arst);
|
||||
if (!ff.pol_arst) ar = qcsat.ez->NOT(ar);
|
||||
n = qcsat.ez->ITE(ar, qcsat.ez->value(ff.val_arst[eb.idx] == State::S1), n);
|
||||
}
|
||||
if (ff.has_sr) {
|
||||
int clr = qcsat.importSigBit(ff.sig_clr[eb.idx]);
|
||||
if (!ff.pol_clr) clr = qcsat.ez->NOT(clr);
|
||||
int set = qcsat.importSigBit(ff.sig_set[eb.idx]);
|
||||
if (!ff.pol_set) set = qcsat.ez->NOT(set);
|
||||
n = qcsat.ez->AND(qcsat.ez->NOT(clr), qcsat.ez->OR(set, n));
|
||||
}
|
||||
if (ff.has_srst) {
|
||||
int srst = qcsat.importSigBit(ff.sig_srst);
|
||||
if (!ff.pol_srst) srst = qcsat.ez->NOT(srst);
|
||||
n = qcsat.ez->ITE(srst, qcsat.ez->value(ff.val_srst[eb.idx] == State::S1), n);
|
||||
}
|
||||
|
||||
n_lit[idx] = n;
|
||||
}
|
||||
}
|
||||
|
||||
qcsat.prepare();
|
||||
|
||||
// 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<int> worklist;
|
||||
std::vector<bool> 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<int> 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;
|
||||
|
||||
// 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<int> modelExprs;
|
||||
for (int b : cls)
|
||||
modelExprs.push_back(n_lit[b]);
|
||||
|
||||
std::vector<bool> modelVals;
|
||||
assumptions.push_back(query);
|
||||
|
||||
if (qcsat.ez->solve(modelExprs, modelVals, assumptions)) {
|
||||
// SAT -> partition entire class
|
||||
std::vector<int> sub0;
|
||||
std::vector<int> sub1;
|
||||
|
||||
for (size_t b_idx = 0; b_idx < cls.size(); b_idx++) {
|
||||
if (modelVals[b_idx])
|
||||
sub1.push_back(cls[b_idx]);
|
||||
else
|
||||
sub0.push_back(cls[b_idx]);
|
||||
}
|
||||
|
||||
classes[cls_idx] = std::move(sub0);
|
||||
classes.push_back(std::move(sub1));
|
||||
in_worklist.push_back(false);
|
||||
|
||||
// Partition was split -> the induction hypo weakened
|
||||
for (int j = 0; j < GetSize(classes); j++) {
|
||||
if (GetSize(classes[j]) >= 2 && !in_worklist[j]) {
|
||||
worklist.push_back(j);
|
||||
in_worklist[j] = true;
|
||||
}
|
||||
}
|
||||
|
||||
break; // Process new splits
|
||||
}
|
||||
|
||||
assumptions.pop_back(); // Remove query for the next pairwise check if UNSAT
|
||||
}
|
||||
}
|
||||
|
||||
return classes;
|
||||
}
|
||||
|
||||
bool apply_eq_merges(const std::vector<std::vector<int>> &classes, const std::vector<EqBit> &bits, dict<Cell *, FfData> &ff_for_cell)
|
||||
{
|
||||
bool any_change = false;
|
||||
dict<Cell *, std::set<int>> remove_bits;
|
||||
|
||||
// Drive every non-rep Q from its class rep, drop merged bits from their FFs
|
||||
for (auto &cls : classes) {
|
||||
if (GetSize(cls) < 2)
|
||||
continue;
|
||||
SigBit rep_q = bits[cls[0]].q;
|
||||
any_change = true;
|
||||
for (int k = 1; k < GetSize(cls); k++) {
|
||||
const EqBit &eb = bits[cls[k]];
|
||||
initvals.remove_init(eb.q);
|
||||
module->connect(eb.q, rep_q);
|
||||
remove_bits[eb.cell].insert(eb.idx);
|
||||
}
|
||||
}
|
||||
|
||||
for (auto &kv : remove_bits) {
|
||||
Cell *cell = kv.first;
|
||||
const std::set<int> &drop = kv.second;
|
||||
FfData &ff = ff_for_cell.at(cell);
|
||||
std::vector<int> keep;
|
||||
|
||||
for (int i = 0; i < ff.width; i++)
|
||||
if (!drop.count(i))
|
||||
keep.push_back(i);
|
||||
|
||||
if (keep.empty()) {
|
||||
module->remove(cell);
|
||||
} else {
|
||||
FfData new_ff = ff.slice(keep);
|
||||
new_ff.cell = cell;
|
||||
new_ff.emit();
|
||||
}
|
||||
}
|
||||
|
||||
return any_change;
|
||||
}
|
||||
|
||||
bool run_eqbits()
|
||||
{
|
||||
if (!opt.sat)
|
||||
return false;
|
||||
|
||||
std::vector<EqBit> bits;
|
||||
dict<Cell *, FfData> ff_for_cell;
|
||||
|
||||
std::vector<std::vector<int>> classes = gather_initial_eq_classes(bits, ff_for_cell);
|
||||
if (classes.empty())
|
||||
return false;
|
||||
|
||||
ModWalker modwalker(module->design, module);
|
||||
|
||||
// Simulation prepass
|
||||
classes = filter_classes_sim(classes, bits, ff_for_cell, modwalker);
|
||||
if (classes.empty())
|
||||
return false;
|
||||
|
||||
// SAT prove
|
||||
classes = filter_classes_sat(std::move(classes), bits, ff_for_cell, modwalker);
|
||||
if (classes.empty())
|
||||
return false;
|
||||
|
||||
return apply_eq_merges(classes, bits, ff_for_cell);
|
||||
}
|
||||
};
|
||||
|
||||
struct OptDffPass : public Pass {
|
||||
|
|
@ -987,6 +1463,8 @@ struct OptDffPass : public Pass {
|
|||
did_something = true;
|
||||
if (worker.run_constbits())
|
||||
did_something = true;
|
||||
if (worker.run_eqbits())
|
||||
did_something = true;
|
||||
}
|
||||
|
||||
if (did_something)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue