diff options
Diffstat (limited to 'passes/sat/assertpmux.cc')
-rw-r--r-- | passes/sat/assertpmux.cc | 179 |
1 files changed, 158 insertions, 21 deletions
diff --git a/passes/sat/assertpmux.cc b/passes/sat/assertpmux.cc index 3c8928db5..63a907671 100644 --- a/passes/sat/assertpmux.cc +++ b/passes/sat/assertpmux.cc @@ -18,40 +18,166 @@ */ #include "kernel/yosys.h" +#include "kernel/sigtools.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -void assertpmux_worker(Cell *pmux, bool flag_noinit) +struct AssertpmuxWorker { - Module *module = pmux->module; + Module *module; + SigMap sigmap; - log("Adding assert for $pmux cell %s.%s.\n", log_id(module), log_id(pmux)); + bool flag_noinit; + bool flag_always; - int swidth = pmux->getParam("\\S_WIDTH").as_int(); - int cntbits = ceil_log2(swidth+1); + // get<0> ... mux cell + // get<1> ... mux port index + // get<2> ... mux bit index + dict<SigBit, pool<tuple<Cell*, int, int>>> sigbit_muxusers; - SigSpec sel = pmux->getPort("\\S"); - SigSpec cnt(State::S0, cntbits); + dict<SigBit, SigBit> sigbit_actsignals; + dict<SigSpec, SigBit> sigspec_actsignals; + dict<tuple<Cell*, int>, SigBit> muxport_actsignal; - for (int i = 0; i < swidth; i++) - cnt = module->Add(NEW_ID, cnt, sel[i]); + AssertpmuxWorker(Module *module, bool flag_noinit, bool flag_always) : + module(module), sigmap(module), flag_noinit(flag_noinit), flag_always(flag_always) + { + for (auto wire : module->wires()) + { + if (wire->port_output) + for (auto bit : sigmap(wire)) + sigbit_actsignals[bit] = State::S1; + } + + for (auto cell : module->cells()) + { + if (cell->type.in("$mux", "$pmux")) + { + int width = cell->getParam("\\WIDTH").as_int(); + int numports = cell->type == "$mux" ? 2 : cell->getParam("\\S_WIDTH").as_int() + 1; + + SigSpec sig_a = sigmap(cell->getPort("\\A")); + SigSpec sig_b = sigmap(cell->getPort("\\B")); + SigSpec sig_s = sigmap(cell->getPort("\\S")); + + for (int i = 0; i < numports; i++) { + SigSpec bits = i == 0 ? sig_a : sig_b.extract(width*(i-1), width); + for (int k = 0; k < width; k++) { + tuple<Cell*, int, int> muxuser(cell, i, k); + sigbit_muxusers[bits[k]].insert(muxuser); + } + } + } + else + { + for (auto &conn : cell->connections()) { + if (!cell->known() || cell->input(conn.first)) + for (auto bit : sigmap(conn.second)) + sigbit_actsignals[bit] = State::S1; + } + } + } + } + + SigBit get_bit_activation(SigBit bit) + { + sigmap.apply(bit); + + if (sigbit_actsignals.count(bit) == 0) + { + SigSpec output; + + for (auto muxuser : sigbit_muxusers.at(bit)) + { + Cell *cell = std::get<0>(muxuser); + int portidx = std::get<1>(muxuser); + int bitidx = std::get<2>(muxuser); + + tuple<Cell*, int> muxport(cell, portidx); + + if (muxport_actsignal.count(muxport) == 0) { + if (portidx == 0) + muxport_actsignal[muxport] = module->LogicNot(NEW_ID, cell->getPort("\\S")); + else + muxport_actsignal[muxport] = cell->getPort("\\S")[portidx-1]; + } + + output.append(module->LogicAnd(NEW_ID, muxport_actsignal.at(muxport), get_bit_activation(cell->getPort("\\Y")[bitidx]))); + } + + output.sort_and_unify(); + + if (GetSize(output) == 0) + output = State::S0; + else if (GetSize(output) > 1) + output = module->ReduceOr(NEW_ID, output); + + sigbit_actsignals[bit] = output.as_bit(); + } + + return sigbit_actsignals.at(bit); + } + + SigBit get_activation(SigSpec sig) + { + sigmap.apply(sig); + sig.sort_and_unify(); + + if (sigspec_actsignals.count(sig) == 0) + { + SigSpec output; + + for (auto bit : sig) + output.append(get_bit_activation(bit)); - SigSpec assert_a = module->Le(NEW_ID, cnt, SigSpec(1, cntbits)); - SigSpec assert_en = State::S1; + output.sort_and_unify(); - if (flag_noinit) { - Cell *initstate_cell = module->addCell(NEW_ID, "$initstate"); - SigSpec initstate_sig = module->addWire(NEW_ID); - initstate_cell->setPort("\\Y", initstate_sig); - assert_en = module->LogicNot(NEW_ID, initstate_sig); + if (GetSize(output) == 0) + output = State::S0; + else if (GetSize(output) > 1) + output = module->ReduceOr(NEW_ID, output); + + sigspec_actsignals[sig] = output.as_bit(); + } + + return sigspec_actsignals.at(sig); } - Cell *assert_cell = module->addAssert(NEW_ID, assert_a, assert_en); + void run(Cell *pmux) + { + log("Adding assert for $pmux cell %s.%s.\n", log_id(module), log_id(pmux)); + + int swidth = pmux->getParam("\\S_WIDTH").as_int(); + int cntbits = ceil_log2(swidth+1); + + SigSpec sel = pmux->getPort("\\S"); + SigSpec cnt(State::S0, cntbits); - if (pmux->attributes.count("\\src") != 0) - assert_cell->attributes["\\src"] = pmux->attributes.at("\\src"); -} + for (int i = 0; i < swidth; i++) + cnt = module->Add(NEW_ID, cnt, sel[i]); + + SigSpec assert_a = module->Le(NEW_ID, cnt, SigSpec(1, cntbits)); + SigSpec assert_en; + + if (flag_noinit) + assert_en.append(module->LogicNot(NEW_ID, module->Initstate(NEW_ID))); + + if (!flag_always) + assert_en.append(get_activation(pmux->getPort("\\Y"))); + + if (GetSize(assert_en) == 0) + assert_en = State::S1; + + if (GetSize(assert_en) == 2) + assert_en = module->LogicAnd(NEW_ID, assert_en[0], assert_en[1]); + + Cell *assert_cell = module->addAssert(NEW_ID, assert_a, assert_en); + + if (pmux->attributes.count("\\src") != 0) + assert_cell->attributes["\\src"] = pmux->attributes.at("\\src"); + } +}; struct AssertpmuxPass : public Pass { AssertpmuxPass() : Pass("assertpmux", "convert internal signals to module ports") { } @@ -67,10 +193,16 @@ struct AssertpmuxPass : public Pass { log(" -noinit\n"); log(" do not enforce the pmux condition during the init state\n"); log("\n"); + log(" -always\n"); + log(" usually the $pmux condition is only checked when the $pmux output\n"); + log(" is used be the mux tree it drives. this option will deactivate this\n"); + log(" additional constrained and check the $pmux condition always.\n"); + log("\n"); } virtual void execute(std::vector<std::string> args, RTLIL::Design *design) { bool flag_noinit = false; + bool flag_always = false; log_header(design, "Executing ASSERTPMUX pass (add asserts for $pmux cells).\n"); @@ -81,12 +213,17 @@ struct AssertpmuxPass : public Pass { flag_noinit = true; continue; } + if (args[argidx] == "-always") { + flag_always = true; + continue; + } break; } extra_args(args, argidx, design); for (auto module : design->selected_modules()) { + AssertpmuxWorker worker(module, flag_noinit, flag_always); vector<Cell*> pmux_cells; for (auto cell : module->selected_cells()) @@ -94,7 +231,7 @@ struct AssertpmuxPass : public Pass { pmux_cells.push_back(cell); for (auto cell : pmux_cells) - assertpmux_worker(cell, flag_noinit); + worker.run(cell); } } |