diff options
Diffstat (limited to 'passes/sat')
| -rw-r--r-- | passes/sat/assertpmux.cc | 4 | ||||
| -rw-r--r-- | passes/sat/async2sync.cc | 306 | ||||
| -rw-r--r-- | passes/sat/clk2fflogic.cc | 446 | ||||
| -rw-r--r-- | passes/sat/cutpoint.cc | 23 | ||||
| -rw-r--r-- | passes/sat/eval.cc | 4 | ||||
| -rw-r--r-- | passes/sat/expose.cc | 34 | ||||
| -rw-r--r-- | passes/sat/fmcombine.cc | 7 | ||||
| -rw-r--r-- | passes/sat/fminit.cc | 4 | ||||
| -rw-r--r-- | passes/sat/freduce.cc | 4 | ||||
| -rw-r--r-- | passes/sat/miter.cc | 4 | ||||
| -rw-r--r-- | passes/sat/mutate.cc | 10 | ||||
| -rw-r--r-- | passes/sat/qbfsat.cc | 439 | ||||
| -rw-r--r-- | passes/sat/qbfsat.h | 253 | ||||
| -rw-r--r-- | passes/sat/sat.cc | 14 | ||||
| -rw-r--r-- | passes/sat/sim.cc | 219 | ||||
| -rw-r--r-- | passes/sat/supercover.cc | 4 |
16 files changed, 906 insertions, 869 deletions
diff --git a/passes/sat/assertpmux.cc b/passes/sat/assertpmux.cc index 5bf2296ab..e9a10465e 100644 --- a/passes/sat/assertpmux.cc +++ b/passes/sat/assertpmux.cc @@ -181,7 +181,7 @@ struct AssertpmuxWorker struct AssertpmuxPass : public Pass { AssertpmuxPass() : Pass("assertpmux", "adds asserts for parallel muxes") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -199,7 +199,7 @@ struct AssertpmuxPass : public Pass { log(" additional constraint and check the $pmux condition always.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { bool flag_noinit = false; bool flag_always = false; diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index e344e2b5b..3fa5a614c 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -19,13 +19,15 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" +#include "kernel/ffinit.h" +#include "kernel/ff.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN struct Async2syncPass : public Pass { Async2syncPass() : Pass("async2sync", "convert async FF inputs to sync circuits") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -42,7 +44,7 @@ struct Async2syncPass : public Pass { log("Currently only $adff, $dffsr, and $dlatch cells are supported by this pass.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { // bool flag_noinit = false; @@ -62,169 +64,183 @@ struct Async2syncPass : public Pass { for (auto module : design->selected_modules()) { SigMap sigmap(module); - dict<SigBit, State> initbits; - pool<SigBit> del_initbits; - - for (auto wire : module->wires()) - if (wire->attributes.count(ID::init) > 0) - { - Const initval = wire->attributes.at(ID::init); - SigSpec initsig = sigmap(wire); - - for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++) - if (initval[i] == State::S0 || initval[i] == State::S1) - initbits[initsig[i]] = initval[i]; - } + FfInitVals initvals(&sigmap, module); for (auto cell : vector<Cell*>(module->selected_cells())) { - if (cell->type.in(ID($adff))) - { - // bool clk_pol = cell->parameters[ID::CLK_POLARITY].as_bool(); - bool arst_pol = cell->parameters[ID::ARST_POLARITY].as_bool(); - Const arst_val = cell->parameters[ID::ARST_VALUE]; - - // SigSpec sig_clk = cell->getPort(ID::CLK); - SigSpec sig_arst = cell->getPort(ID::ARST); - SigSpec sig_d = cell->getPort(ID::D); - SigSpec sig_q = cell->getPort(ID::Q); - - log("Replacing %s.%s (%s): ARST=%s, D=%s, Q=%s\n", - log_id(module), log_id(cell), log_id(cell->type), - log_signal(sig_arst), log_signal(sig_d), log_signal(sig_q)); - - Const init_val; - for (int i = 0; i < GetSize(sig_q); i++) { - SigBit bit = sigmap(sig_q[i]); - init_val.bits.push_back(initbits.count(bit) ? initbits.at(bit) : State::Sx); - del_initbits.insert(bit); - } + if (!RTLIL::builtin_ff_cell_types().count(cell->type)) + continue; - Wire *new_d = module->addWire(NEW_ID, GetSize(sig_d)); - Wire *new_q = module->addWire(NEW_ID, GetSize(sig_q)); - new_q->attributes[ID::init] = init_val; + FfData ff(&initvals, cell); - if (arst_pol) { - module->addMux(NEW_ID, sig_d, arst_val, sig_arst, new_d); - module->addMux(NEW_ID, new_q, arst_val, sig_arst, sig_q); - } else { - module->addMux(NEW_ID, arst_val, sig_d, sig_arst, new_d); - module->addMux(NEW_ID, arst_val, new_q, sig_arst, sig_q); - } - - cell->setPort(ID::D, new_d); - cell->setPort(ID::Q, new_q); - cell->unsetPort(ID::ARST); - cell->unsetParam(ID::ARST_POLARITY); - cell->unsetParam(ID::ARST_VALUE); - cell->type = ID($dff); + // Skip for $_FF_ and $ff cells. + if (ff.has_d && !ff.has_clk && !ff.has_en) continue; - } - if (cell->type.in(ID($dffsr))) + if (ff.has_clk) { - // bool clk_pol = cell->parameters[ID::CLK_POLARITY].as_bool(); - bool set_pol = cell->parameters[ID::SET_POLARITY].as_bool(); - bool clr_pol = cell->parameters[ID::CLR_POLARITY].as_bool(); - - // SigSpec sig_clk = cell->getPort(ID::CLK); - SigSpec sig_set = cell->getPort(ID::SET); - SigSpec sig_clr = cell->getPort(ID::CLR); - SigSpec sig_d = cell->getPort(ID::D); - SigSpec sig_q = cell->getPort(ID::Q); - - log("Replacing %s.%s (%s): SET=%s, CLR=%s, D=%s, Q=%s\n", - log_id(module), log_id(cell), log_id(cell->type), - log_signal(sig_set), log_signal(sig_clr), log_signal(sig_d), log_signal(sig_q)); - - Const init_val; - for (int i = 0; i < GetSize(sig_q); i++) { - SigBit bit = sigmap(sig_q[i]); - init_val.bits.push_back(initbits.count(bit) ? initbits.at(bit) : State::Sx); - del_initbits.insert(bit); + if (!ff.has_sr && !ff.has_arst) + continue; + + if (ff.has_sr) { + ff.unmap_ce_srst(module); + + log("Replacing %s.%s (%s): SET=%s, CLR=%s, D=%s, Q=%s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_signal(ff.sig_set), log_signal(ff.sig_clr), log_signal(ff.sig_d), log_signal(ff.sig_q)); + + initvals.remove_init(ff.sig_q); + + Wire *new_d = module->addWire(NEW_ID, ff.width); + Wire *new_q = module->addWire(NEW_ID, ff.width); + + SigSpec sig_set = ff.sig_set; + SigSpec sig_clr = ff.sig_clr; + + if (!ff.pol_set) { + if (!ff.is_fine) + sig_set = module->Not(NEW_ID, sig_set); + else + sig_set = module->NotGate(NEW_ID, sig_set); + } + + if (ff.pol_clr) { + if (!ff.is_fine) + sig_clr = module->Not(NEW_ID, sig_clr); + else + sig_clr = module->NotGate(NEW_ID, sig_clr); + } + + if (!ff.is_fine) { + SigSpec tmp = module->Or(NEW_ID, ff.sig_d, sig_set); + module->addAnd(NEW_ID, tmp, sig_clr, new_d); + + tmp = module->Or(NEW_ID, new_q, sig_set); + module->addAnd(NEW_ID, tmp, sig_clr, ff.sig_q); + } else { + SigSpec tmp = module->OrGate(NEW_ID, ff.sig_d, sig_set); + module->addAndGate(NEW_ID, tmp, sig_clr, new_d); + + tmp = module->OrGate(NEW_ID, new_q, sig_set); + module->addAndGate(NEW_ID, tmp, sig_clr, ff.sig_q); + } + + ff.sig_d = new_d; + ff.sig_q = new_q; + ff.has_sr = false; + } else if (ff.has_arst) { + ff.unmap_srst(module); + + log("Replacing %s.%s (%s): ARST=%s, D=%s, Q=%s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_signal(ff.sig_arst), log_signal(ff.sig_d), log_signal(ff.sig_q)); + + initvals.remove_init(ff.sig_q); + + Wire *new_q = module->addWire(NEW_ID, ff.width); + + if (ff.pol_arst) { + if (!ff.is_fine) + module->addMux(NEW_ID, new_q, ff.val_arst, ff.sig_arst, ff.sig_q); + else + module->addMuxGate(NEW_ID, new_q, ff.val_arst[0], ff.sig_arst, ff.sig_q); + } else { + if (!ff.is_fine) + module->addMux(NEW_ID, ff.val_arst, new_q, ff.sig_arst, ff.sig_q); + else + module->addMuxGate(NEW_ID, ff.val_arst[0], new_q, ff.sig_arst, ff.sig_q); + } + + ff.sig_q = new_q; + ff.has_arst = false; + ff.has_srst = true; + ff.val_srst = ff.val_arst; + ff.sig_srst = ff.sig_arst; + ff.pol_srst = ff.pol_arst; } - - Wire *new_d = module->addWire(NEW_ID, GetSize(sig_d)); - Wire *new_q = module->addWire(NEW_ID, GetSize(sig_q)); - new_q->attributes[ID::init] = init_val; - - if (!set_pol) - sig_set = module->Not(NEW_ID, sig_set); - - if (clr_pol) - sig_clr = module->Not(NEW_ID, sig_clr); - - SigSpec tmp = module->Or(NEW_ID, sig_d, sig_set); - module->addAnd(NEW_ID, tmp, sig_clr, new_d); - - tmp = module->Or(NEW_ID, new_q, sig_set); - module->addAnd(NEW_ID, tmp, sig_clr, sig_q); - - cell->setPort(ID::D, new_d); - cell->setPort(ID::Q, new_q); - cell->unsetPort(ID::SET); - cell->unsetPort(ID::CLR); - cell->unsetParam(ID::SET_POLARITY); - cell->unsetParam(ID::CLR_POLARITY); - cell->type = ID($dff); - continue; } - - if (cell->type.in(ID($dlatch))) + else { - bool en_pol = cell->parameters[ID::EN_POLARITY].as_bool(); - - SigSpec sig_en = cell->getPort(ID::EN); - SigSpec sig_d = cell->getPort(ID::D); - SigSpec sig_q = cell->getPort(ID::Q); - + // Latch. log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n", log_id(module), log_id(cell), log_id(cell->type), - log_signal(sig_en), log_signal(sig_d), log_signal(sig_q)); - - Const init_val; - for (int i = 0; i < GetSize(sig_q); i++) { - SigBit bit = sigmap(sig_q[i]); - init_val.bits.push_back(initbits.count(bit) ? initbits.at(bit) : State::Sx); - del_initbits.insert(bit); + log_signal(ff.sig_en), log_signal(ff.sig_d), log_signal(ff.sig_q)); + + initvals.remove_init(ff.sig_q); + + Wire *new_q = module->addWire(NEW_ID, ff.width); + Wire *new_d; + + if (ff.has_d) { + new_d = module->addWire(NEW_ID, ff.width); + if (ff.pol_en) { + if (!ff.is_fine) + module->addMux(NEW_ID, new_q, ff.sig_d, ff.sig_en, new_d); + else + module->addMuxGate(NEW_ID, new_q, ff.sig_d, ff.sig_en, new_d); + } else { + if (!ff.is_fine) + module->addMux(NEW_ID, ff.sig_d, new_q, ff.sig_en, new_d); + else + module->addMuxGate(NEW_ID, ff.sig_d, new_q, ff.sig_en, new_d); + } + } else { + new_d = new_q; } - Wire *new_q = module->addWire(NEW_ID, GetSize(sig_q)); - new_q->attributes[ID::init] = init_val; - - if (en_pol) { - module->addMux(NEW_ID, new_q, sig_d, sig_en, sig_q); + if (ff.has_sr) { + SigSpec sig_set = ff.sig_set; + SigSpec sig_clr = ff.sig_clr; + + if (!ff.pol_set) { + if (!ff.is_fine) + sig_set = module->Not(NEW_ID, sig_set); + else + sig_set = module->NotGate(NEW_ID, sig_set); + } + + if (ff.pol_clr) { + if (!ff.is_fine) + sig_clr = module->Not(NEW_ID, sig_clr); + else + sig_clr = module->NotGate(NEW_ID, sig_clr); + } + + if (!ff.is_fine) { + SigSpec tmp = module->Or(NEW_ID, new_d, sig_set); + module->addAnd(NEW_ID, tmp, sig_clr, ff.sig_q); + } else { + SigSpec tmp = module->OrGate(NEW_ID, new_d, sig_set); + module->addAndGate(NEW_ID, tmp, sig_clr, ff.sig_q); + } + } else if (ff.has_arst) { + if (ff.pol_arst) { + if (!ff.is_fine) + module->addMux(NEW_ID, new_d, ff.val_arst, ff.sig_arst, ff.sig_q); + else + module->addMuxGate(NEW_ID, new_d, ff.val_arst[0], ff.sig_arst, ff.sig_q); + } else { + if (!ff.is_fine) + module->addMux(NEW_ID, ff.val_arst, new_d, ff.sig_arst, ff.sig_q); + else + module->addMuxGate(NEW_ID, ff.val_arst[0], new_d, ff.sig_arst, ff.sig_q); + } } else { - module->addMux(NEW_ID, sig_d, new_q, sig_en, sig_q); + module->connect(ff.sig_q, new_d); } - cell->setPort(ID::D, sig_q); - cell->setPort(ID::Q, new_q); - cell->unsetPort(ID::EN); - cell->unsetParam(ID::EN_POLARITY); - cell->type = ID($ff); - continue; + ff.sig_d = new_d; + ff.sig_q = new_q; + ff.has_en = false; + ff.has_arst = false; + ff.has_sr = false; + ff.has_d = true; } - } - for (auto wire : module->wires()) - if (wire->attributes.count(ID::init) > 0) - { - bool delete_initattr = true; - Const initval = wire->attributes.at(ID::init); - SigSpec initsig = sigmap(wire); - - for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++) - if (del_initbits.count(initsig[i]) > 0) - initval[i] = State::Sx; - else if (initval[i] != State::Sx) - delete_initattr = false; - - if (delete_initattr) - wire->attributes.erase(ID::init); - else - wire->attributes.at(ID::init) = initval; - } + IdString name = cell->name; + module->remove(cell); + ff.emit(module, name); + } } } } Async2syncPass; diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index 1e155e52c..cbf7c5435 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -19,13 +19,16 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" +#include "kernel/ffinit.h" +#include "kernel/ff.h" +#include "kernel/mem.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN struct Clk2fflogicPass : public Pass { Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -36,7 +39,31 @@ struct Clk2fflogicPass : public Pass { log("multiple clocks.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity) { + Wire *past_sig = module->addWire(NEW_ID, GetSize(sig)); + module->addFf(NEW_ID, sig, past_sig); + if (polarity) + sig = module->Or(NEW_ID, sig, past_sig); + else + sig = module->And(NEW_ID, sig, past_sig); + if (polarity) + return sig; + else + return module->Not(NEW_ID, sig); + } + SigSpec wrap_async_control_gate(Module *module, SigSpec sig, bool polarity) { + Wire *past_sig = module->addWire(NEW_ID); + module->addFfGate(NEW_ID, sig, past_sig); + if (polarity) + sig = module->OrGate(NEW_ID, sig, past_sig); + else + sig = module->AndGate(NEW_ID, sig, past_sig); + if (polarity) + return sig; + else + return module->NotGate(NEW_ID, sig); + } + void execute(std::vector<std::string> args, RTLIL::Design *design) override { // bool flag_noinit = false; @@ -56,348 +83,173 @@ struct Clk2fflogicPass : public Pass { for (auto module : design->selected_modules()) { SigMap sigmap(module); - dict<SigBit, State> initbits; - pool<SigBit> del_initbits; - - for (auto wire : module->wires()) - if (wire->attributes.count(ID::init) > 0) - { - Const initval = wire->attributes.at(ID::init); - SigSpec initsig = sigmap(wire); + FfInitVals initvals(&sigmap, module); - for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++) - if (initval[i] == State::S0 || initval[i] == State::S1) - initbits[initsig[i]] = initval[i]; + for (auto &mem : Mem::get_selected_memories(module)) + { + for (int i = 0; i < GetSize(mem.rd_ports); i++) { + auto &port = mem.rd_ports[i]; + if (port.clk_enable) + log_error("Read port %d of memory %s.%s is clocked. This is not supported by \"clk2fflogic\"! " + "Call \"memory\" with -nordff to avoid this error.\n", i, log_id(mem.memid), log_id(module)); } - for (auto cell : vector<Cell*>(module->selected_cells())) - { - if (cell->type.in(ID($mem))) + for (int i = 0; i < GetSize(mem.wr_ports); i++) { - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - int rd_ports = cell->getParam(ID::RD_PORTS).as_int(); - int wr_ports = cell->getParam(ID::WR_PORTS).as_int(); - - for (int i = 0; i < rd_ports; i++) { - if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool()) - log_error("Read port %d of memory %s.%s is clocked. This is not supported by \"clk2fflogic\"! " - "Call \"memory\" with -nordff to avoid this error.\n", i, log_id(cell), log_id(module)); - } - - Const wr_clk_en_param = cell->getParam(ID::WR_CLK_ENABLE); - Const wr_clk_pol_param = cell->getParam(ID::WR_CLK_POLARITY); - - SigSpec wr_clk_port = cell->getPort(ID::WR_CLK); - SigSpec wr_en_port = cell->getPort(ID::WR_EN); - SigSpec wr_addr_port = cell->getPort(ID::WR_ADDR); - SigSpec wr_data_port = cell->getPort(ID::WR_DATA); - - for (int wport = 0; wport < wr_ports; wport++) - { - bool clken = wr_clk_en_param[wport] == State::S1; - bool clkpol = wr_clk_pol_param[wport] == State::S1; - - if (!clken) - continue; + auto &port = mem.wr_ports[i]; - SigBit clk = wr_clk_port[wport]; - SigSpec en = wr_en_port.extract(wport*width, width); - SigSpec addr = wr_addr_port.extract(wport*abits, abits); - SigSpec data = wr_data_port.extract(wport*width, width); - - log("Modifying write port %d on memory %s.%s: CLK=%s, A=%s, D=%s\n", - wport, log_id(module), log_id(cell), log_signal(clk), - log_signal(addr), log_signal(data)); - - Wire *past_clk = module->addWire(NEW_ID); - past_clk->attributes[ID::init] = clkpol ? State::S1 : State::S0; - module->addFf(NEW_ID, clk, past_clk); - - SigSpec clock_edge_pattern; - - if (clkpol) { - clock_edge_pattern.append(State::S0); - clock_edge_pattern.append(State::S1); - } else { - clock_edge_pattern.append(State::S1); - clock_edge_pattern.append(State::S0); - } + if (!port.clk_enable) + continue; - SigSpec clock_edge = module->Eqx(NEW_ID, {clk, SigSpec(past_clk)}, clock_edge_pattern); + log("Modifying write port %d on memory %s.%s: CLK=%s, A=%s, D=%s\n", + i, log_id(module), log_id(mem.memid), log_signal(port.clk), + log_signal(port.addr), log_signal(port.data)); - SigSpec en_q = module->addWire(NEW_ID, GetSize(en)); - module->addFf(NEW_ID, en, en_q); - - SigSpec addr_q = module->addWire(NEW_ID, GetSize(addr)); - module->addFf(NEW_ID, addr, addr_q); - - SigSpec data_q = module->addWire(NEW_ID, GetSize(data)); - module->addFf(NEW_ID, data, data_q); + Wire *past_clk = module->addWire(NEW_ID); + past_clk->attributes[ID::init] = port.clk_polarity ? State::S1 : State::S0; + module->addFf(NEW_ID, port.clk, past_clk); - wr_clk_port[wport] = State::S0; - wr_en_port.replace(wport*width, module->Mux(NEW_ID, Const(0, GetSize(en_q)), en_q, clock_edge)); - wr_addr_port.replace(wport*abits, addr_q); - wr_data_port.replace(wport*width, data_q); + SigSpec clock_edge_pattern; - wr_clk_en_param[wport] = State::S0; - wr_clk_pol_param[wport] = State::S0; + if (port.clk_polarity) { + clock_edge_pattern.append(State::S0); + clock_edge_pattern.append(State::S1); + } else { + clock_edge_pattern.append(State::S1); + clock_edge_pattern.append(State::S0); } - cell->setParam(ID::WR_CLK_ENABLE, wr_clk_en_param); - cell->setParam(ID::WR_CLK_POLARITY, wr_clk_pol_param); + SigSpec clock_edge = module->Eqx(NEW_ID, {port.clk, SigSpec(past_clk)}, clock_edge_pattern); - cell->setPort(ID::WR_CLK, wr_clk_port); - cell->setPort(ID::WR_EN, wr_en_port); - cell->setPort(ID::WR_ADDR, wr_addr_port); - cell->setPort(ID::WR_DATA, wr_data_port); - } - - if (cell->type.in(ID($dlatch), ID($dlatchsr))) - { - bool enpol = cell->parameters[ID::EN_POLARITY].as_bool(); + SigSpec en_q = module->addWire(NEW_ID, GetSize(port.en)); + module->addFf(NEW_ID, port.en, en_q); - SigSpec sig_en = cell->getPort(ID::EN); - SigSpec sig_d = cell->getPort(ID::D); - SigSpec sig_q = cell->getPort(ID::Q); + SigSpec addr_q = module->addWire(NEW_ID, GetSize(port.addr)); + module->addFf(NEW_ID, port.addr, addr_q); - log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n", - log_id(module), log_id(cell), log_id(cell->type), - log_signal(sig_en), log_signal(sig_d), log_signal(sig_q)); + SigSpec data_q = module->addWire(NEW_ID, GetSize(port.data)); + module->addFf(NEW_ID, port.data, data_q); - Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q)); - module->addFf(NEW_ID, sig_q, past_q); + port.clk = State::S0; + port.en = module->Mux(NEW_ID, Const(0, GetSize(en_q)), en_q, clock_edge); + port.addr = addr_q; + port.data = data_q; - if (cell->type == ID($dlatch)) - { - if (enpol) - module->addMux(NEW_ID, past_q, sig_d, sig_en, sig_q); - else - module->addMux(NEW_ID, sig_d, past_q, sig_en, sig_q); - } - else - { - SigSpec t; - if (enpol) - t = module->Mux(NEW_ID, past_q, sig_d, sig_en); - else - t = module->Mux(NEW_ID, sig_d, past_q, sig_en); + port.clk_enable = false; + port.clk_polarity = false; + } - SigSpec s = cell->getPort(ID::SET); - if (!cell->parameters[ID::SET_POLARITY].as_bool()) - s = module->Not(NEW_ID, s); - t = module->Or(NEW_ID, t, s); + mem.emit(); + } - SigSpec c = cell->getPort(ID::CLR); - if (cell->parameters[ID::CLR_POLARITY].as_bool()) - c = module->Not(NEW_ID, c); - module->addAnd(NEW_ID, t, c, sig_q); - } + for (auto cell : vector<Cell*>(module->selected_cells())) + { + SigSpec qval; + if (RTLIL::builtin_ff_cell_types().count(cell->type)) { + FfData ff(&initvals, cell); - Const initval; - bool assign_initval = false; - for (int i = 0; i < GetSize(sig_d); i++) { - SigBit qbit = sigmap(sig_q[i]); - if (initbits.count(qbit)) { - initval.bits.push_back(initbits.at(qbit)); - del_initbits.insert(qbit); - } else - initval.bits.push_back(State::Sx); - if (initval.bits.back() != State::Sx) - assign_initval = true; + if (ff.has_d && !ff.has_clk && !ff.has_en) { + // Already a $ff or $_FF_ cell. + continue; } - if (assign_initval) - past_q->attributes[ID::init] = initval; - - module->remove(cell); - continue; - } - - bool word_dff = cell->type.in(ID($dff), ID($adff), ID($dffsr)); - if (word_dff || cell->type.in(ID($_DFF_N_), ID($_DFF_P_), - ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_), - ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_), - ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_), - ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_))) - { - bool clkpol; - SigSpec clk; - if (word_dff) { - clkpol = cell->parameters[ID::CLK_POLARITY].as_bool(); - clk = cell->getPort(ID::CLK); - } - else { - if (cell->type.in(ID($_DFF_P_), ID($_DFF_N_), - ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_), - ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_))) - clkpol = cell->type[6] == 'P'; - else if (cell->type.in(ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_), - ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_))) - clkpol = cell->type[8] == 'P'; - else log_abort(); - clk = cell->getPort(ID::C); + Wire *past_q = module->addWire(NEW_ID, ff.width); + if (!ff.is_fine) { + module->addFf(NEW_ID, ff.sig_q, past_q); + } else { + module->addFfGate(NEW_ID, ff.sig_q, past_q); } + if (!ff.val_init.is_fully_undef()) + initvals.set_init(past_q, ff.val_init); - Wire *past_clk = module->addWire(NEW_ID); - past_clk->attributes[ID::init] = clkpol ? State::S1 : State::S0; - - if (word_dff) - module->addFf(NEW_ID, clk, past_clk); - else - module->addFfGate(NEW_ID, clk, past_clk); + if (ff.has_clk) { + ff.unmap_ce_srst(module); - SigSpec sig_d = cell->getPort(ID::D); - SigSpec sig_q = cell->getPort(ID::Q); + Wire *past_clk = module->addWire(NEW_ID); + initvals.set_init(past_clk, ff.pol_clk ? State::S1 : State::S0); - log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n", - log_id(module), log_id(cell), log_id(cell->type), - log_signal(clk), log_signal(sig_d), log_signal(sig_q)); + if (!ff.is_fine) + module->addFf(NEW_ID, ff.sig_clk, past_clk); + else + module->addFfGate(NEW_ID, ff.sig_clk, past_clk); - SigSpec clock_edge_pattern; + log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_signal(ff.sig_clk), log_signal(ff.sig_d), log_signal(ff.sig_q)); - if (clkpol) { - clock_edge_pattern.append(State::S0); - clock_edge_pattern.append(State::S1); - } else { - clock_edge_pattern.append(State::S1); - clock_edge_pattern.append(State::S0); - } - - SigSpec clock_edge = module->Eqx(NEW_ID, {clk, SigSpec(past_clk)}, clock_edge_pattern); + SigSpec clock_edge_pattern; - Wire *past_d = module->addWire(NEW_ID, GetSize(sig_d)); - Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q)); - if (word_dff) { - module->addFf(NEW_ID, sig_d, past_d); - module->addFf(NEW_ID, sig_q, past_q); - } - else { - module->addFfGate(NEW_ID, sig_d, past_d); - module->addFfGate(NEW_ID, sig_q, past_q); - } + if (ff.pol_clk) { + clock_edge_pattern.append(State::S0); + clock_edge_pattern.append(State::S1); + } else { + clock_edge_pattern.append(State::S1); + clock_edge_pattern.append(State::S0); + } - if (cell->type == ID($adff)) - { - SigSpec arst = cell->getPort(ID::ARST); - SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge); - Const rstval = cell->parameters[ID::ARST_VALUE]; + SigSpec clock_edge = module->Eqx(NEW_ID, {ff.sig_clk, SigSpec(past_clk)}, clock_edge_pattern); - Wire *past_arst = module->addWire(NEW_ID); - module->addFf(NEW_ID, arst, past_arst); - if (cell->parameters[ID::ARST_POLARITY].as_bool()) - arst = module->LogicOr(NEW_ID, arst, past_arst); + Wire *past_d = module->addWire(NEW_ID, ff.width); + if (!ff.is_fine) + module->addFf(NEW_ID, ff.sig_d, past_d); else - arst = module->LogicAnd(NEW_ID, arst, past_arst); + module->addFfGate(NEW_ID, ff.sig_d, past_d); - if (cell->parameters[ID::ARST_POLARITY].as_bool()) - module->addMux(NEW_ID, qval, rstval, arst, sig_q); - else - module->addMux(NEW_ID, rstval, qval, arst, sig_q); - } - else - if (cell->type.in(ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_), - ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_))) - { - SigSpec arst = cell->getPort(ID::R); - SigSpec qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge); - SigBit rstval = (cell->type[8] == '1'); - - Wire *past_arst = module->addWire(NEW_ID); - module->addFfGate(NEW_ID, arst, past_arst); - if (cell->type[7] == 'P') - arst = module->OrGate(NEW_ID, arst, past_arst); - else - arst = module->AndGate(NEW_ID, arst, past_arst); + if (!ff.val_init.is_fully_undef()) + initvals.set_init(past_d, ff.val_init); - if (cell->type[7] == 'P') - module->addMuxGate(NEW_ID, qval, rstval, arst, sig_q); + if (!ff.is_fine) + qval = module->Mux(NEW_ID, past_q, past_d, clock_edge); else - module->addMuxGate(NEW_ID, rstval, qval, arst, sig_q); - } - else - if (cell->type == ID($dffsr)) - { - SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge); - SigSpec setval = cell->getPort(ID::SET); - SigSpec clrval = cell->getPort(ID::CLR); + qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge); + } else if (ff.has_d) { - if (!cell->parameters[ID::SET_POLARITY].as_bool()) - setval = module->Not(NEW_ID, setval); + log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_signal(ff.sig_en), log_signal(ff.sig_d), log_signal(ff.sig_q)); - if (cell->parameters[ID::CLR_POLARITY].as_bool()) - clrval = module->Not(NEW_ID, clrval); + SigSpec sig_en = wrap_async_control(module, ff.sig_en, ff.pol_en); - qval = module->Or(NEW_ID, qval, setval); - module->addAnd(NEW_ID, qval, clrval, sig_q); - } - else - if (cell->type.in(ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_), - ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_))) - { - SigSpec qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge); - SigSpec setval = cell->getPort(ID::S); - SigSpec clrval = cell->getPort(ID::R); - - if (cell->type[9] != 'P') - setval = module->Not(NEW_ID, setval); - - if (cell->type[10] == 'P') - clrval = module->Not(NEW_ID, clrval); + if (!ff.is_fine) + qval = module->Mux(NEW_ID, past_q, ff.sig_d, sig_en); + else + qval = module->MuxGate(NEW_ID, past_q, ff.sig_d, sig_en); + } else { - qval = module->OrGate(NEW_ID, qval, setval); - module->addAndGate(NEW_ID, qval, clrval, sig_q); - } - else if (cell->type == ID($dff)) - { - module->addMux(NEW_ID, past_q, past_d, clock_edge, sig_q); - } - else - { - module->addMuxGate(NEW_ID, past_q, past_d, clock_edge, sig_q); - } + log("Replacing %s.%s (%s): SET=%s, CLR=%s, Q=%s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_signal(ff.sig_set), log_signal(ff.sig_clr), log_signal(ff.sig_q)); - Const initval; - bool assign_initval = false; - for (int i = 0; i < GetSize(sig_d); i++) { - SigBit qbit = sigmap(sig_q[i]); - if (initbits.count(qbit)) { - initval.bits.push_back(initbits.at(qbit)); - del_initbits.insert(qbit); - } else - initval.bits.push_back(State::Sx); - if (initval.bits.back() != State::Sx) - assign_initval = true; + qval = past_q; } - if (assign_initval) { - past_d->attributes[ID::init] = initval; - past_q->attributes[ID::init] = initval; + if (ff.has_sr) { + SigSpec setval = wrap_async_control(module, ff.sig_set, ff.pol_set); + SigSpec clrval = wrap_async_control(module, ff.sig_clr, ff.pol_clr); + if (!ff.is_fine) { + clrval = module->Not(NEW_ID, clrval); + qval = module->Or(NEW_ID, qval, setval); + module->addAnd(NEW_ID, qval, clrval, ff.sig_q); + } else { + clrval = module->NotGate(NEW_ID, clrval); + qval = module->OrGate(NEW_ID, qval, setval); + module->addAndGate(NEW_ID, qval, clrval, ff.sig_q); + } + } else if (ff.has_arst) { + SigSpec arst = wrap_async_control(module, ff.sig_arst, ff.pol_arst); + if (!ff.is_fine) + module->addMux(NEW_ID, qval, ff.val_arst, arst, ff.sig_q); + else + module->addMuxGate(NEW_ID, qval, ff.val_arst[0], arst, ff.sig_q); + } else { + module->connect(ff.sig_q, qval); } + initvals.remove_init(ff.sig_q); module->remove(cell); continue; } } - - for (auto wire : module->wires()) - if (wire->attributes.count(ID::init) > 0) - { - bool delete_initattr = true; - Const initval = wire->attributes.at(ID::init); - SigSpec initsig = sigmap(wire); - - for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++) - if (del_initbits.count(initsig[i]) > 0) - initval[i] = State::Sx; - else if (initval[i] != State::Sx) - delete_initattr = false; - - if (delete_initattr) - wire->attributes.erase(ID::init); - else - wire->attributes.at(ID::init) = initval; - } } } diff --git a/passes/sat/cutpoint.cc b/passes/sat/cutpoint.cc index 26cc69211..6fc267d51 100644 --- a/passes/sat/cutpoint.cc +++ b/passes/sat/cutpoint.cc @@ -25,7 +25,7 @@ PRIVATE_NAMESPACE_BEGIN struct CutpointPass : public Pass { CutpointPass() : Pass("cutpoint", "adds formal cut points to the design") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -38,7 +38,7 @@ struct CutpointPass : public Pass { log(" $anyseq cell and drive the cutpoint net from that\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { bool flag_undef = false; @@ -126,15 +126,16 @@ struct CutpointPass : public Pass { } vector<Wire*> rewrite_wires; - for (auto wire : module->wires()) { - if (!wire->port_input) - continue; - int bit_count = 0; - for (auto &bit : sigmap(wire)) - if (cutpoint_bits.count(bit)) - bit_count++; - if (bit_count) - rewrite_wires.push_back(wire); + for (auto id : module->ports) { + RTLIL::Wire *wire = module->wire(id); + if (wire->port_input) { + int bit_count = 0; + for (auto &bit : sigmap(wire)) + if (cutpoint_bits.count(bit)) + bit_count++; + if (bit_count) + rewrite_wires.push_back(wire); + } } for (auto wire : rewrite_wires) { diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc index f910ea80d..085e7c5b8 100644 --- a/passes/sat/eval.cc +++ b/passes/sat/eval.cc @@ -359,7 +359,7 @@ struct VlogHammerReporter struct EvalPass : public Pass { EvalPass() : Pass("eval", "evaluate the circuit given an input") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -382,7 +382,7 @@ struct EvalPass : public Pass { log(" then all output ports of the current module are used.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { std::vector<std::pair<std::string, std::string>> sets; std::vector<std::string> shows, tables; diff --git a/passes/sat/expose.cc b/passes/sat/expose.cc index 80ab82cd5..2c65821cf 100644 --- a/passes/sat/expose.cc +++ b/passes/sat/expose.cc @@ -217,7 +217,7 @@ RTLIL::Wire *add_new_wire(RTLIL::Module *module, RTLIL::IdString name, int width struct ExposePass : public Pass { ExposePass() : Pass("expose", "convert internal signals to module ports") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -254,7 +254,7 @@ struct ExposePass : public Pass { log(" designator for the exposed signal.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { bool flag_shared = false; bool flag_evert = false; @@ -281,11 +281,15 @@ struct ExposePass : public Pass { flag_dff = true; continue; } - if (args[argidx] == "-cut" && !flag_input) { + if (args[argidx] == "-cut") { + if (flag_input) + log_cmd_error("Options -cut and -input are mutually exclusive.\n"); flag_cut = true; continue; } - if (args[argidx] == "-input" && !flag_cut) { + if (args[argidx] == "-input") { + if (flag_cut) + log_cmd_error("Options -cut and -input are mutually exclusive.\n"); flag_input = true; continue; } @@ -445,6 +449,8 @@ struct ExposePass : public Pass { SigMap out_to_in_map; + std::map<RTLIL::Wire*, RTLIL::IdString> wire_map; + for (auto w : module->wires()) { if (flag_shared) { @@ -462,8 +468,7 @@ struct ExposePass : public Pass { if (!w->port_input) { w->port_input = true; log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(w->name)); - RTLIL::Wire *in_wire = module->addWire(NEW_ID, GetSize(w)); - out_to_in_map.add(w, in_wire); + wire_map[w] = NEW_ID; } } else @@ -474,15 +479,19 @@ struct ExposePass : public Pass { } if (flag_cut) { - RTLIL::Wire *in_wire = add_new_wire(module, w->name.str() + sep + "i", w->width); - in_wire->port_input = true; - out_to_in_map.add(sigmap(w), in_wire); + wire_map[w] = w->name.str() + sep + "i"; } } } if (flag_input) { + for (auto &wm : wire_map) + { + RTLIL::Wire *in_wire = module->addWire(wm.second, GetSize(wm.first)); + out_to_in_map.add(wm.first, in_wire); + } + for (auto cell : module->cells()) { if (!ct.cell_known(cell->type)) continue; @@ -497,6 +506,13 @@ struct ExposePass : public Pass { if (flag_cut) { + for (auto &wm : wire_map) + { + RTLIL::Wire *in_wire = add_new_wire(module, wm.second, wm.first->width); + in_wire->port_input = true; + out_to_in_map.add(sigmap(wm.first), in_wire); + } + for (auto cell : module->cells()) { if (!ct.cell_known(cell->type)) continue; diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc index 5066485aa..cb49edac3 100644 --- a/passes/sat/fmcombine.cc +++ b/passes/sat/fmcombine.cc @@ -114,8 +114,7 @@ struct FmcombineWorker Cell *gold = import_prim_cell(cell, "_gold"); Cell *gate = import_prim_cell(cell, "_gate"); if (opts.initeq) { - if (cell->type.in(ID($ff), ID($dff), ID($dffe), - ID($dffsr), ID($adff), ID($dlatch), ID($dlatchsr))) { + if (RTLIL::builtin_ff_cell_types().count(cell->type)) { SigSpec gold_q = gold->getPort(ID::Q); SigSpec gate_q = gate->getPort(ID::Q); SigSpec en = module->Initstate(NEW_ID); @@ -235,7 +234,7 @@ struct FmcombineWorker struct FmcombinePass : public Pass { FmcombinePass() : Pass("fmcombine", "combine two instances of a cell into one") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -272,7 +271,7 @@ struct FmcombinePass : public Pass { log("If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { opts_t opts; Module *module = nullptr; diff --git a/passes/sat/fminit.cc b/passes/sat/fminit.cc index 555a28dc6..c72e62548 100644 --- a/passes/sat/fminit.cc +++ b/passes/sat/fminit.cc @@ -25,7 +25,7 @@ PRIVATE_NAMESPACE_BEGIN struct FminitPass : public Pass { FminitPass() : Pass("fminit", "set init values/sequences for formal") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -47,7 +47,7 @@ struct FminitPass : public Pass { log(" Set clock for init sequences\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { vector<pair<string, vector<string>>> initdata; vector<pair<string, string>> setdata; diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc index 5dfd7bd3f..762edfdfb 100644 --- a/passes/sat/freduce.cc +++ b/passes/sat/freduce.cc @@ -760,7 +760,7 @@ struct FreduceWorker struct FreducePass : public Pass { FreducePass() : Pass("freduce", "perform functional reduction") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -791,7 +791,7 @@ struct FreducePass : public Pass { log("circuit that is analyzed.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { reduce_counter = 0; reduce_stop_at = 0; diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc index aeece9b94..fe4a819f3 100644 --- a/passes/sat/miter.cc +++ b/passes/sat/miter.cc @@ -354,7 +354,7 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL struct MiterPass : public Pass { MiterPass() : Pass("miter", "automatically create a miter circuit") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -398,7 +398,7 @@ struct MiterPass : public Pass { log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { if (args.size() > 1 && args[1] == "-equiv") { create_miter_equiv(this, args, design); diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index af8ffca9e..95e0e0944 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -439,7 +439,7 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena dict<SigBit, int> bit_user_cnt; for (auto wire : module->wires()) { - if (wire->name[0] == '\\' && wire->attributes.count(ID::src)) + if (wire->name.isPublic() && wire->attributes.count(ID::src)) sigmap.add(wire); } @@ -468,7 +468,7 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena } if (!bit.wire->name[0] != !sigbit.wire->name[0]) { - if (bit.wire->name[0] == '\\') + if (bit.wire->name.isPublic()) sigmap.add(bit); continue; } @@ -493,7 +493,7 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena entry.src.insert(s); SigBit bit = sigmap(conn.second[i]); - if (bit.wire && bit.wire->name[0] == '\\' && (cell->output(conn.first) || bit_user_cnt[bit] == 1)) { + if (bit.wire && bit.wire->name.isPublic() && (cell->output(conn.first) || bit_user_cnt[bit] == 1)) { for (auto &s : bit.wire->get_strpool_attribute(ID::src)) entry.src.insert(s); entry.wire = bit.wire->name; @@ -726,7 +726,7 @@ void mutate_cnot(Design *design, const mutate_opts_t &opts, bool one) struct MutatePass : public Pass { MutatePass() : Pass("mutate", "generate or apply design mutations") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -790,7 +790,7 @@ struct MutatePass : public Pass { log(" Ignored. (They are generated by -list for documentation purposes.)\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { mutate_opts_t opts; string filename; diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index d6dbf8ef4..6db7d4b64 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -1,4 +1,4 @@ -/* +/* -*- c++ -*- * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2020 Alberto Gonzalez <boqwxp@airmail.cc> @@ -18,137 +18,20 @@ */ #include "kernel/yosys.h" -#include "kernel/celltypes.h" #include "kernel/consteval.h" -#include "kernel/log.h" -#include "kernel/rtlil.h" -#include "kernel/register.h" -#include <algorithm> +#include "qbfsat.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct QbfSolutionType { - std::vector<std::string> stdout_lines; - dict<std::string, std::string> hole_to_value; - bool sat; - bool unknown; //true if neither 'sat' nor 'unsat' - - QbfSolutionType() : sat(false), unknown(true) {} -}; - -struct QbfSolveOptions { - bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg; - bool nooptimize, nobisection; - bool sat, unsat, show_smtbmc; - enum Solver{Z3, Yices, CVC4} solver; - int timeout; - std::string specialize_soln_file; - std::string write_soln_soln_file; - std::string dump_final_smt2_file; - size_t argidx; - QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false), - nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false), - nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false), - solver(Yices), timeout(0), argidx(0) {}; -}; - -std::string get_solver_name(const QbfSolveOptions &opt) { - if (opt.solver == opt.Solver::Z3) - return "z3"; - else if (opt.solver == opt.Solver::Yices) - return "yices"; - else if (opt.solver == opt.Solver::CVC4) - return "cvc4"; +static inline unsigned int difference(unsigned int a, unsigned int b) { + if (a < b) + return b - a; else - log_cmd_error("unknown solver specified.\n"); - return ""; + return a - b; } -void recover_solution(QbfSolutionType &sol) { - YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED"); - YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available"); - YS_REGEX_TYPE unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED"); - YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)"); - YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)"); - YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)"); - YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver"); - YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\""); - YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)"); -#ifndef NDEBUG - YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+"); - YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+"); -#endif - YS_REGEX_MATCH_TYPE m; - bool sat_regex_found = false; - bool unsat_regex_found = false; - dict<std::string, bool> hole_value_recovered; - for (const std::string &x : sol.stdout_lines) { - if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) { - std::string loc = m[1].str(); - std::string val = m[2].str(); -#ifndef NDEBUG - log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex)); - log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex)); -#endif - sol.hole_to_value[loc] = val; - } - else if (YS_REGEX_NS::regex_search(x, sat_regex)) { - sat_regex_found = true; - sol.sat = true; - sol.unknown = false; - } - else if (YS_REGEX_NS::regex_search(x, unsat_regex)) { - unsat_regex_found = true; - sol.sat = false; - sol.unknown = false; - } - else if (YS_REGEX_NS::regex_search(x, memout_regex)) { - sol.unknown = true; - log_warning("solver ran out of memory\n"); - } - else if (YS_REGEX_NS::regex_search(x, timeout_regex)) { - sol.unknown = true; - log_warning("solver timed out\n"); - } - else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) { - sol.unknown = true; - log_warning("solver timed out\n"); - } - else if (YS_REGEX_NS::regex_search(x, unknown_regex)) { - sol.unknown = true; - log_warning("solver returned \"unknown\"\n"); - } - else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) { - unsat_regex_found = true; - sol.sat = false; - sol.unknown = false; - } - else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) { - sol.unknown = true; - } - } -#ifndef NDEBUG - log_assert(!sol.unknown && sol.sat? sat_regex_found : true); - log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true); -#endif -} - -dict<std::string, std::string> get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) { - dict<std::string, std::string> hole_loc_to_name; - for (auto cell : module->cells()) { - std::string cell_src = cell->get_src_attribute(); - auto pos = sol.hole_to_value.find(cell_src); - if (pos != sol.hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) { - log_assert(hole_loc_to_name.find(pos->first) == hole_loc_to_name.end()); - hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str(); - } - } - - return hole_loc_to_name; -} - -pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) { +pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, bool assume_outputs) { bool found_input = false; bool found_hole = false; bool found_1bit_output = false; @@ -176,133 +59,108 @@ pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const Qb log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n"); if (!found_1bit_output && !found_assert_assume) log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n"); - if (!found_assert_assume && !opt.assume_outputs) + if (!found_assert_assume && !assume_outputs) log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n"); return input_wires; } -void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) { - std::ofstream fout(file.c_str()); - if (!fout) - log_cmd_error("could not open solution file for writing.\n"); +void specialize_from_file(RTLIL::Module *module, const std::string &file) { + YS_REGEX_TYPE hole_bit_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$"); + YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified + YS_REGEX_MATCH_TYPE bit_m, m; + dict<pool<std::string>, RTLIL::Cell*> anyconst_loc_to_cell; + dict<RTLIL::SigBit, RTLIL::State> hole_assignments; - dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol); - for(auto &x : sol.hole_to_value) - fout << hole_loc_to_name[x.first] << "=" << x.second << std::endl; -} + for (auto cell : module->cells()) + if (cell->type == "$anyconst") + anyconst_loc_to_cell[cell->get_strpool_attribute(ID::src)] = cell; -void specialize_from_file(RTLIL::Module *module, const std::string &file) { - YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.*)=([01]+)$"); - YS_REGEX_MATCH_TYPE m; - pool<RTLIL::Cell *> anyconsts_to_remove; - dict<std::string, std::string> hole_name_to_value; std::ifstream fin(file.c_str()); if (!fin) log_cmd_error("could not read solution file.\n"); std::string buf; while (std::getline(fin, buf)) { - log_assert(YS_REGEX_NS::regex_search(buf, m, hole_assn_regex)); - std::string hole_name = m[1].str(); - std::string hole_value = m[2].str(); - hole_name_to_value[hole_name] = hole_value; + bool bit_assn = true; + if (!YS_REGEX_NS::regex_search(buf, bit_m, hole_bit_assn_regex)) { + bit_assn = false; + if (!YS_REGEX_NS::regex_search(buf, m, hole_assn_regex)) + log_cmd_error("solution file is not formatted correctly: \"%s\"\n", buf.c_str()); + } + + std::string hole_loc = bit_assn? bit_m[1].str() : m[1].str(); + unsigned int hole_bit = bit_assn? atoi(bit_m[2].str().c_str()) : atoi(m[2].str().c_str()); + std::string hole_name = bit_assn? bit_m[3].str() : m[3].str(); + unsigned int hole_offset = bit_assn? atoi(bit_m[4].str().c_str()) : 0; + RTLIL::State hole_value = bit_assn? (atoi(bit_m[5].str().c_str()) == 1? RTLIL::State::S1 : RTLIL::State::S0) + : (atoi(m[4].str().c_str()) == 1? RTLIL::State::S1 : RTLIL::State::S0); + + //We have two options to identify holes. First, try to match wire names. If we can't find a matching wire, + //then try to find a cell with a matching location. + RTLIL::SigBit hole_sigbit; + if (module->wire(hole_name) != nullptr) { + RTLIL::Wire *hole_wire = module->wire(hole_name); + hole_sigbit = RTLIL::SigSpec(hole_wire)[hole_offset]; + } else { + auto locs = split_tokens(hole_loc, "|"); + pool<std::string> hole_loc_pool(locs.begin(), locs.end()); + auto hole_cell_it = anyconst_loc_to_cell.find(hole_loc_pool); + if (hole_cell_it == anyconst_loc_to_cell.end()) + log_cmd_error("cannot find matching wire name or $anyconst cell location for hole spec \"%s\"\n", buf.c_str()); + + RTLIL::Cell *hole_cell = hole_cell_it->second; + hole_sigbit = hole_cell->getPort(ID::Y)[hole_bit]; + } + hole_assignments[hole_sigbit] = hole_value; } - for (auto cell : module->cells()) - if (cell->type == "$anyconst") { - auto anyconst_port_y = cell->getPort(ID::Y).as_wire(); - if (anyconst_port_y == nullptr) - continue; - if (hole_name_to_value.find(anyconst_port_y->name.str()) != hole_name_to_value.end()) - anyconsts_to_remove.insert(cell); - } - for (auto cell : anyconsts_to_remove) - module->remove(cell); + for (auto &it : anyconst_loc_to_cell) + module->remove(it.second); - for (auto &it : hole_name_to_value) { - std::string hole_name = it.first; - std::string hole_value = it.second; - RTLIL::Wire *wire = module->wire(hole_name); -#ifndef NDEBUG - log_assert(wire != nullptr); - log_assert(wire->width > 0 && GetSize(hole_value) == wire->width); -#endif - - log("Specializing %s from file with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str()); - std::vector<RTLIL::SigBit> value_bv; - value_bv.reserve(wire->width); - for (char c : hole_value) - value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0); - std::reverse(value_bv.begin(), value_bv.end()); - module->connect(wire, value_bv); + for (auto &it : hole_assignments) { + RTLIL::SigSpec lhs(it.first); + RTLIL::SigSpec rhs(it.second); + log("Specializing %s from file with %s = %d.\n", module->name.c_str(), log_signal(it.first), it.second == RTLIL::State::S1? 1 : 0); + module->connect(lhs, rhs); } } void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = false) { - dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol); + auto hole_loc_idx_to_sigbit = sol.get_hole_loc_idx_sigbit_map(module); pool<RTLIL::Cell *> anyconsts_to_remove; for (auto cell : module->cells()) if (cell->type == "$anyconst") - if (hole_loc_to_name.find(cell->get_src_attribute()) != hole_loc_to_name.end()) + if (hole_loc_idx_to_sigbit.find(std::make_pair(cell->get_strpool_attribute(ID::src), 0)) != hole_loc_idx_to_sigbit.end()) anyconsts_to_remove.insert(cell); for (auto cell : anyconsts_to_remove) module->remove(cell); for (auto &it : sol.hole_to_value) { - std::string hole_loc = it.first; - std::string hole_value = it.second; - -#ifndef NDEBUG - auto pos = hole_loc_to_name.find(hole_loc); - log_assert(pos != hole_loc_to_name.end()); -#endif - - std::string hole_name = hole_loc_to_name[hole_loc]; - RTLIL::Wire *wire = module->wire(hole_name); -#ifndef NDEBUG - log_assert(wire != nullptr); - log_assert(wire->width > 0 && GetSize(hole_value) == wire->width); -#endif - - if (!quiet) - log("Specializing %s with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str()); - std::vector<RTLIL::SigBit> value_bv; - value_bv.reserve(wire->width); - for (char c : hole_value) - value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0); - std::reverse(value_bv.begin(), value_bv.end()); - module->connect(wire, value_bv); - } -} - -void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) { - log("Satisfiable model:\n"); - dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol); - for (auto &it : sol.hole_to_value) { - std::string hole_loc = it.first; + pool<std::string> hole_loc = it.first; std::string hole_value = it.second; -#ifndef NDEBUG - auto pos = hole_loc_to_name.find(hole_loc); - log_assert(pos != hole_loc_to_name.end()); -#endif - - std::string hole_name = hole_loc_to_name[hole_loc]; - log("\t%s = %lu'b%s\n", hole_name.c_str(), hole_value.size(), hole_value.c_str()); - std::vector<RTLIL::SigBit> value_bv; - value_bv.reserve(hole_value.size()); - for (char c : hole_value) - value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0); - std::reverse(value_bv.begin(), value_bv.end()); + for (unsigned int i = 0; i < hole_value.size(); ++i) { + int bit_idx = GetSize(hole_value) - 1 - i; + auto it = hole_loc_idx_to_sigbit.find(std::make_pair(hole_loc, i)); + log_assert(it != hole_loc_idx_to_sigbit.end()); + + RTLIL::SigBit hole_sigbit = it->second; + log_assert(hole_sigbit.wire != nullptr); + log_assert(hole_value[bit_idx] == '0' || hole_value[bit_idx] == '1'); + RTLIL::SigSpec lhs(hole_sigbit.wire, hole_sigbit.offset, 1); + RTLIL::State hole_bit_val = hole_value[bit_idx] == '1'? RTLIL::State::S1 : RTLIL::State::S0; + if (!quiet) + log("Specializing %s with %s = %d.\n", module->name.c_str(), log_signal(hole_sigbit), hole_bit_val == RTLIL::State::S0? 0 : 1) +; + module->connect(lhs, hole_bit_val); + } } } void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wires) { for (auto &n : input_wires) { RTLIL::Wire *input = module->wire(n); -#ifndef NDEBUG log_assert(input != nullptr); -#endif RTLIL::Cell *allconst = module->addCell("$allconst$" + n, "$allconst"); allconst->setParam(ID(WIDTH), input->width); @@ -314,7 +172,7 @@ void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wi module->fixup_ports(); } -void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) { +void assume_miter_outputs(RTLIL::Module *module, bool assume_neg) { std::vector<RTLIL::Wire *> wires_to_assume; for (auto w : module->wires()) if (w->port_output && w->width == 1) @@ -329,7 +187,7 @@ void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) { log("\n"); } - if (opt.assume_neg) { + if (assume_neg) { for (unsigned int i = 0; i < wires_to_assume.size(); ++i) { RTLIL::SigSpec n_wire = module->LogicNot(wires_to_assume[i]->name.str() + "__n__qbfsat", wires_to_assume[i], false, wires_to_assume[i]->get_src_attribute()); wires_to_assume[i] = n_wire.as_wire(); @@ -349,9 +207,7 @@ void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) { wires_to_assume.swap(buf); } -#ifndef NDEBUG log_assert(wires_to_assume.size() == 1); -#endif module->addAssume("$assume_qbfsat_miter_outputs", wires_to_assume[0], RTLIL::S1); } @@ -359,10 +215,17 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]` QbfSolutionType ret; const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; - const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2"; const std::string smtbmc_warning = "z3: WARNING:"; - const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s " + (get_solver_name(opt)) + (opt.timeout != 0? stringf(" --timeout %d", opt.timeout) : "") + " -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1"; - + const std::string smtbmc_cmd = stringf("%s -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1", + yosys_smtbmc_exe.c_str(), opt.get_solver_name().c_str(), + (opt.timeout != 0? stringf("--timeout %d", opt.timeout) : "").c_str(), + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file : "").c_str(), + tempdir_name.c_str(), iter_num); + + std::string smt2_command = "write_smt2 -stbv -wires "; + for (auto &solver_opt : opt.solver_options) + smt2_command += stringf("-solver-option %s %s ", solver_opt.first.c_str(), solver_opt.second.c_str()); + smt2_command += stringf("%s/problem%d.smt2", tempdir_name.c_str(), iter_num); Pass::call(mod->design, smt2_command); auto process_line = [&ret, &smtbmc_warning, &opt, &quiet](const std::string &line) { @@ -376,45 +239,59 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, }; log_header(mod->design, "Solving QBF-SAT problem.\n"); if (!quiet) log("Launching \"%s\".\n", smtbmc_cmd.c_str()); + int64_t begin = PerformanceTimer::query(); run_command(smtbmc_cmd, process_line); + int64_t end = PerformanceTimer::query(); + ret.solver_time = (end - begin) / 1e9f; + if (!quiet) log("Solver finished in %.3f seconds.\n", ret.solver_time); - recover_solution(ret); + ret.recover_solution(); return ret; } QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { QbfSolutionType ret, best_soln; - const std::string tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX"); + const std::string tempdir_name = make_temp_dir("/tmp/yosys-qbfsat-XXXXXX"); RTLIL::Module *module = mod; RTLIL::Design *design = module->design; std::string module_name = module->name.str(); - RTLIL::Wire *wire_to_optimize = nullptr; - RTLIL::IdString wire_to_optimize_name; + RTLIL::IdString wire_to_optimize_name = ""; bool maximize = false; log_assert(module->design != nullptr); Pass::call(design, "design -push-copy"); //Replace input wires with wires assigned $allconst cells: - pool<std::string> input_wires = validate_design_and_get_inputs(module, opt); + pool<std::string> input_wires = validate_design_and_get_inputs(module, opt.assume_outputs); allconstify_inputs(module, input_wires); if (opt.assume_outputs) - assume_miter_outputs(module, opt); + assume_miter_outputs(module, opt.assume_neg); //Find the wire to be optimized, if any: - for (auto wire : module->wires()) - if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize")) - wire_to_optimize = wire; - if (wire_to_optimize != nullptr) { - wire_to_optimize_name = wire_to_optimize->name; - maximize = wire_to_optimize->get_bool_attribute("\\maximize"); + for (auto wire : module->wires()) { + if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize")) { + wire_to_optimize_name = wire->name; + maximize = wire->get_bool_attribute("\\maximize"); + if (opt.nooptimize) { + if (maximize) + wire->set_bool_attribute("\\maximize", false); + else + wire->set_bool_attribute("\\minimize", false); + } + } } - if (opt.nobisection || opt.nooptimize) { - if (wire_to_optimize != nullptr && opt.nooptimize) { - wire_to_optimize->set_bool_attribute("\\maximize", false); - wire_to_optimize->set_bool_attribute("\\minimize", false); - } + //If -O1 or -O2 was specified, use ABC to simplify the problem: + if (opt.oflag == opt.OptimizationLevel::O1) + Pass::call(module->design, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;fraig;print_stats;refactor,-N,10,-lz;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod->name.str()); + else if (opt.oflag == opt.OptimizationLevel::O2) + Pass::call(module->design, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;dch,-S,1000000,-C,100000,-p;print_stats;fraig;print_stats;refactor,-N,15,-lz;print_stats;dc2,-pbl;print_stats;drwsat;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod->name.str()); + if (opt.oflag != opt.OptimizationLevel::O0) { + Pass::call(module->design, "techmap"); + Pass::call(module->design, "opt"); + } + + if (opt.nobisection || opt.nooptimize || wire_to_optimize_name == "") { ret = call_qbf_solver(module, opt, tempdir_name, false, 0); } else { //Do the iterated bisection method: @@ -423,11 +300,12 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { unsigned int failure = 0; unsigned int cur_thresh = 0; - log_assert(wire_to_optimize != nullptr); - log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), log_signal(wire_to_optimize)); + log_assert(wire_to_optimize_name != ""); + log_assert(module->wire(wire_to_optimize_name) != nullptr); + log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), wire_to_optimize_name.c_str()); //If maximizing, grow until we get a failure. Then bisect success and failure. - while (failure == 0 || success - failure > 1) { + while (failure == 0 || difference(success, failure) > 1) { Pass::call(design, "design -push-copy"); log_header(design, "Preparing QBF-SAT problem.\n"); @@ -465,8 +343,9 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { //sometimes this happens if we get an 'unknown' or timeout if (!maximize && success < failure) break; - else if (maximize && success > failure) + else if (maximize && failure != 0 && success > failure) break; + } else { //Treat 'unknown' as UNSAT failure = cur_thresh; @@ -479,8 +358,12 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { } iter_num++; - cur_thresh = (maximize && failure == 0)? 2 * success //growth - : (success + failure) / 2; //bisection + if (maximize && failure == 0 && success == 0) + cur_thresh = 2; + else if (maximize && failure == 0) + cur_thresh = 2 * success; //growth + else //if (!maximize || failure != 0) + cur_thresh = (success + failure) / 2; //bisection } if (success != 0 || failure != 0) { log("Wire %s is %s at %d.\n", wire_to_optimize_name.c_str(), (maximize? "maximized" : "minimized"), success); @@ -539,6 +422,13 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { } continue; } + else if (args[opt.argidx] == "-solver-option") { + if (args.size() <= opt.argidx + 2) + log_cmd_error("solver option name and value not fully specified.\n"); + opt.solver_options.emplace(args[opt.argidx+1], args[opt.argidx+2]); + opt.argidx += 2; + continue; + } else if (args[opt.argidx] == "-timeout") { if (args.size() <= opt.argidx + 1) log_cmd_error("timeout not specified.\n"); @@ -552,6 +442,22 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { } continue; } + else if (args[opt.argidx].substr(0, 2) == "-O" && args[opt.argidx].size() == 3) { + switch (args[opt.argidx][2]) { + case '0': + opt.oflag = opt.OptimizationLevel::O0; + break; + case '1': + opt.oflag = opt.OptimizationLevel::O1; + break; + case '2': + opt.oflag = opt.OptimizationLevel::O2; + break; + default: + log_cmd_error("unknown argument %s\n", args[opt.argidx].c_str()); + } + continue; + } else if (args[opt.argidx] == "-sat") { opt.sat = true; continue; @@ -594,36 +500,9 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { return opt; } -void print_proof_failed() -{ - log("\n"); - log(" ______ ___ ___ _ _ _ _ \n"); - log(" (_____ \\ / __) / __) (_) | | | |\n"); - log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n"); - log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n"); - log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n"); - log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n"); - log("\n"); -} - -void print_qed() -{ - log("\n"); - log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n"); - log(" /$$__ $$ | $$_____/ | $$__ $$ \n"); - log(" | $$ \\ $$ | $$ | $$ \\ $$ \n"); - log(" | $$ | $$ | $$$$$ | $$ | $$ \n"); - log(" | $$ | $$ | $$__/ | $$ | $$ \n"); - log(" | $$/$$ $$ | $$ | $$ | $$ \n"); - log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n"); - log(" \\____ $$$|__/|________/|__/|_______/|__/\n"); - log(" \\__/ \n"); - log("\n"); -} - struct QbfSatPass : public Pass { QbfSatPass() : Pass("qbfsat", "solve a 2QBF-SAT problem in the circuit") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -662,9 +541,17 @@ struct QbfSatPass : public Pass { log("\n"); log(" -solver <solver>\n"); log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n"); + log(" (default: yices)\n"); + log("\n"); + log(" -solver-option <name> <value>\n"); + log(" Set the specified solver option in the SMT-LIBv2 problem file.\n"); log("\n"); log(" -timeout <value>\n"); log(" Set the per-iteration timeout in seconds.\n"); + log(" (default: no timeout)\n"); + log("\n"); + log(" -O0, -O1, -O2\n"); + log(" Control the use of ABC to simplify the QBF-SAT problem before solving.\n"); log("\n"); log(" -sat\n"); log(" Generate an error if the solver does not return \"sat\".\n"); @@ -690,7 +577,7 @@ struct QbfSatPass : public Pass { log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { log_header(design, "Executing QBFSAT pass (solving QBF-SAT problems in the circuit).\n"); QbfSolveOptions opt = parse_args(args); @@ -719,12 +606,12 @@ struct QbfSatPass : public Pass { else if (ret.sat) { print_qed(); if (opt.write_solution) { - write_solution(module, ret, opt.write_soln_soln_file); + ret.write_solution(module, opt.write_soln_soln_file); } if (opt.specialize) { specialize(module, ret); } else { - dump_model(module, ret); + ret.dump_model(module); } if (opt.unsat) log_cmd_error("expected problem to be UNSAT\n"); diff --git a/passes/sat/qbfsat.h b/passes/sat/qbfsat.h new file mode 100644 index 000000000..c96c6f818 --- /dev/null +++ b/passes/sat/qbfsat.h @@ -0,0 +1,253 @@ +/* -*- c++ -*- + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2020 Alberto Gonzalez <boqwxp@airmail.cc> + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#ifndef QBFSAT_H +#define QBFSAT_H + +#include "kernel/yosys.h" +#include <numeric> + +YOSYS_NAMESPACE_BEGIN + +struct QbfSolveOptions { + bool specialize = false, specialize_from_file = false, write_solution = false, nocleanup = false; + bool dump_final_smt2 = false, assume_outputs = false, assume_neg = false, nooptimize = false; + bool nobisection = false, sat = false, unsat = false, show_smtbmc = false; + enum Solver{Z3, Yices, CVC4} solver = Yices; + enum OptimizationLevel{O0, O1, O2} oflag = O0; + dict<std::string, std::string> solver_options; + int timeout = 0; + std::string specialize_soln_file = ""; + std::string write_soln_soln_file = ""; + std::string dump_final_smt2_file = ""; + size_t argidx = 0; + + std::string get_solver_name() const { + if (solver == Solver::Z3) + return "z3"; + else if (solver == Solver::Yices) + return "yices"; + else if (solver == Solver::CVC4) + return "cvc4"; + + log_cmd_error("unknown solver specified.\n"); + return ""; + } +}; + +struct QbfSolutionType { + std::vector<std::string> stdout_lines = {}; + dict<pool<std::string>, std::string> hole_to_value = {}; + double solver_time = 0; + bool sat = false; + bool unknown = true; //true if neither 'sat' nor 'unsat' + + dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module) const { + dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit; + pool<RTLIL::SigBit> anyconst_sigbits; + dict<RTLIL::SigBit, RTLIL::SigBit> anyconst_sigbit_to_wire_sigbit; + + for (auto cell : module->cells()) { + pool<std::string> cell_src = cell->get_strpool_attribute(ID::src); + auto pos = hole_to_value.find(cell_src); + if (pos != hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) { + RTLIL::SigSpec port_y = cell->getPort(ID::Y); + for (int i = GetSize(port_y) - 1; i >= 0; --i) { + hole_loc_idx_to_sigbit[std::make_pair(pos->first, i)] = port_y[i]; + anyconst_sigbits.insert(port_y[i]); + } + } + } + + for (auto &conn : module->connections()) { + auto lhs = conn.first; + auto rhs = conn.second; + for (auto i = 0; i < GetSize(rhs); ++i) { + if (anyconst_sigbits[rhs[i]]) { + auto pos = anyconst_sigbit_to_wire_sigbit.find(rhs[i]); + if (pos != anyconst_sigbit_to_wire_sigbit.end()) + log_cmd_error("conflicting names for hole $anyconst sigbit %s\n", log_signal(rhs[i])); + anyconst_sigbit_to_wire_sigbit[rhs[i]] = lhs[i]; + } + } + } + + for (auto &it : hole_loc_idx_to_sigbit) { + auto pos = anyconst_sigbit_to_wire_sigbit.find(it.second); + if (pos != anyconst_sigbit_to_wire_sigbit.end()) + it.second = pos->second; + } + + return hole_loc_idx_to_sigbit; + } + + void dump_model(RTLIL::Module *module) const { + log("Satisfiable model:\n"); + auto hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module); + for (auto &it : hole_to_value) { + pool<std::string> hole_loc = it.first; + std::string hole_value = it.second; + + for (unsigned int i = 0; i < hole_value.size(); ++i) { + int bit_idx = GetSize(hole_value) - 1 - i; + auto it = hole_loc_idx_to_sigbit.find(std::make_pair(hole_loc, i)); + log_assert(it != hole_loc_idx_to_sigbit.end()); + + RTLIL::SigBit hole_sigbit = it->second; + log("\t%s = 1'b%c\n", log_signal(hole_sigbit), hole_value[bit_idx]); + } + } + } + + void write_solution(RTLIL::Module *module, const std::string &file) const { + std::ofstream fout(file.c_str()); + if (!fout) + log_cmd_error("could not open solution file for writing.\n"); + + //There is a question here: How exactly shall we identify holes? + //There are at least two reasonable options: + //1. By the source location of the $anyconst cells + //2. By the name(s) of the wire(s) connected to each SigBit of the $anyconst cell->getPort(ID::Y) SigSpec. + // + //Option 1 has the benefit of being very precise. There is very limited potential for confusion, as long + //as the source attribute has been set. However, if the source attribute is not set, this won't work. + //More importantly, we want to have the ability to port hole assignments to other modules with compatible + //hole names and widths. Obviously in those cases source locations of the $anyconst cells will not match. + // + //Option 2 has the benefits previously described, but wire names can be changed automatically by + //optimization or techmapping passes, especially when (ex/im)porting from BLIF for optimization with ABC. + // + //The approach taken here is to allow both options. We write the assignment information for each bit of + //the solution on a separate line. Each line is of one of two forms: + // + //location bit name = value + //location bit name [offset] = value + // + //where '[', ']', and '=' are literal symbols, "location" is the $anyconst cell source location attribute, + //"bit" is the index of the $anyconst cell, "name" is the `wire->name` field of the SigBit corresponding + //to the current bit of the $anyconst cell->getPort(ID::Y), "offset" is the `offset` field of that same + //SigBit, and "value", which is either '0' or '1', represents the assignment for that bit. + auto hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module); + for (auto &x : hole_to_value) { + std::string src_as_str = std::accumulate(x.first.begin(), x.first.end(), std::string(), [](const std::string &a, const std::string &b){return a + "|" + b;}); + for (auto i = 0; i < GetSize(x.second); ++i) + fout << src_as_str.c_str() << " " << i << " " << log_signal(hole_loc_idx_to_sigbit[std::make_pair(x.first, i)]) << " = " << x.second[GetSize(x.second) - 1 - i] << std::endl; + } + } + + void recover_solution() { + YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED"); + YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available"); + YS_REGEX_TYPE unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED"); + YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)"); + YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)"); + YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)"); + YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver"); + YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\""); + YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)"); +#ifndef NDEBUG + YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+"); + YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+"); +#endif + YS_REGEX_MATCH_TYPE m; + bool sat_regex_found = false; + bool unsat_regex_found = false; + dict<std::string, bool> hole_value_recovered; + for (const std::string &x : stdout_lines) { + if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) { + std::string loc = m[1].str(); + std::string val = m[2].str(); +#ifndef NDEBUG + log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex)); + log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex)); +#endif + auto locs = split_tokens(loc, "|"); + pool<std::string> loc_pool(locs.begin(), locs.end()); + hole_to_value[loc_pool] = val; + } + else if (YS_REGEX_NS::regex_search(x, sat_regex)) { + sat_regex_found = true; + sat = true; + unknown = false; + } + else if (YS_REGEX_NS::regex_search(x, unsat_regex)) { + unsat_regex_found = true; + sat = false; + unknown = false; + } + else if (YS_REGEX_NS::regex_search(x, memout_regex)) { + unknown = true; + log_warning("solver ran out of memory\n"); + } + else if (YS_REGEX_NS::regex_search(x, timeout_regex)) { + unknown = true; + log_warning("solver timed out\n"); + } + else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) { + unknown = true; + log_warning("solver timed out\n"); + } + else if (YS_REGEX_NS::regex_search(x, unknown_regex)) { + unknown = true; + log_warning("solver returned \"unknown\"\n"); + } + else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) { + unsat_regex_found = true; + sat = false; + unknown = false; + } + else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) { + unknown = true; + } + } + log_assert(!unknown && sat? sat_regex_found : true); + log_assert(!unknown && !sat? unsat_regex_found : true); + } +}; + +void print_proof_failed() +{ + log("\n"); + log(" ______ ___ ___ _ _ _ _ \n"); + log(" (_____ \\ / __) / __) (_) | | | |\n"); + log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n"); + log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n"); + log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n"); + log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n"); + log("\n"); +} + +void print_qed() +{ + log("\n"); + log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n"); + log(" /$$__ $$ | $$_____/ | $$__ $$ \n"); + log(" | $$ \\ $$ | $$ | $$ \\ $$ \n"); + log(" | $$ | $$ | $$$$$ | $$ | $$ \n"); + log(" | $$ | $$ | $$__/ | $$ | $$ \n"); + log(" | $$/$$ $$ | $$ | $$ | $$ \n"); + log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n"); + log(" \\____ $$$|__/|________/|__/|_______/|__/\n"); + log(" \\__/ \n"); + log("\n"); +} + +YOSYS_NAMESPACE_END + +#endif diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 6acdbc800..9fdac6147 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -256,13 +256,13 @@ struct SatHelper { RTLIL::SigSpec big_lhs, big_rhs; - for (auto &it : module->wires_) + for (auto wire : module->wires()) { - if (it.second->attributes.count(ID::init) == 0) + if (wire->attributes.count(ID::init) == 0) continue; - RTLIL::SigSpec lhs = sigmap(it.second); - RTLIL::SigSpec rhs = it.second->attributes.at(ID::init); + RTLIL::SigSpec lhs = sigmap(wire); + RTLIL::SigSpec rhs = wire->attributes.at(ID::init); log_assert(lhs.size() == rhs.size()); RTLIL::SigSpec removed_bits; @@ -893,7 +893,7 @@ void print_qed() struct SatPass : public Pass { SatPass() : Pass("sat", "solve a SAT problem in the circuit") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -1060,7 +1060,7 @@ struct SatPass : public Pass { log(" Like -falsify but do not return an error for timeouts.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { std::vector<std::pair<std::string, std::string>> sets, sets_init, prove, prove_x; std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at; @@ -1365,7 +1365,7 @@ struct SatPass : public Pass { if (show_public) { for (auto wire : module->wires()) - if (wire->name[0] == '\\') + if (wire->name.isPublic()) shows.push_back(wire->name.str()); } diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 03ca42cf3..3ba66bd33 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -20,6 +20,9 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" #include "kernel/celltypes.h" +#include "kernel/mem.h" + +#include <ctime> USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -62,6 +65,7 @@ struct SimInstance pool<SigBit> dirty_bits; pool<Cell*> dirty_cells; + pool<IdString> dirty_memories; pool<SimInstance*, hash_ptr_ops> dirty_children; struct ff_state_t @@ -72,16 +76,20 @@ struct SimInstance struct mem_state_t { - Const past_wr_clk; - Const past_wr_en; - Const past_wr_addr; - Const past_wr_data; + Mem *mem; + std::vector<Const> past_wr_clk; + std::vector<Const> past_wr_en; + std::vector<Const> past_wr_addr; + std::vector<Const> past_wr_data; Const data; }; dict<Cell*, ff_state_t> ff_database; - dict<Cell*, mem_state_t> mem_database; + dict<IdString, mem_state_t> mem_database; pool<Cell*> formal_database; + dict<Cell*, IdString> mem_cells; + + std::vector<Mem> memories; dict<Wire*, pair<int, Const>> vcd_database; @@ -118,6 +126,19 @@ struct SimInstance } } + memories = Mem::get_all_memories(module); + for (auto &mem : memories) { + auto &mdb = mem_database[mem.memid]; + mdb.mem = &mem; + for (auto &port : mem.wr_ports) { + mdb.past_wr_clk.push_back(Const(State::Sx)); + mdb.past_wr_en.push_back(Const(State::Sx, GetSize(port.en))); + mdb.past_wr_addr.push_back(Const(State::Sx, GetSize(port.addr))); + mdb.past_wr_data.push_back(Const(State::Sx, GetSize(port.data))); + } + mdb.data = mem.get_init_data(); + } + for (auto cell : module->cells()) { Module *mod = module->design->module(cell->type); @@ -143,27 +164,10 @@ struct SimInstance ff_database[cell] = ff; } - if (cell->type == ID($mem)) + if (cell->type.in(ID($mem), ID($meminit), ID($memwr), ID($memrd))) { - mem_state_t mem; - - mem.past_wr_clk = Const(State::Sx, GetSize(cell->getPort(ID::WR_CLK))); - mem.past_wr_en = Const(State::Sx, GetSize(cell->getPort(ID::WR_EN))); - mem.past_wr_addr = Const(State::Sx, GetSize(cell->getPort(ID::WR_ADDR))); - mem.past_wr_data = Const(State::Sx, GetSize(cell->getPort(ID::WR_DATA))); - - mem.data = cell->getParam(ID::INIT); - int sz = cell->getParam(ID::SIZE).as_int() * cell->getParam(ID::WIDTH).as_int(); - - if (GetSize(mem.data) > sz) - mem.data.bits.resize(sz); - - while (GetSize(mem.data) < sz) - mem.data.bits.push_back(State::Sx); - - mem_database[cell] = mem; + mem_cells[cell] = cell->parameters.at(ID::MEMID).decode_string(); } - if (cell->type.in(ID($assert), ID($cover), ID($assume))) { formal_database.insert(cell); } @@ -185,7 +189,8 @@ struct SimInstance for (auto &it : mem_database) { mem_state_t &mem = it.second; - zinit(mem.past_wr_en); + for (auto &val : mem.past_wr_en) + zinit(val); zinit(mem.data); } } @@ -256,37 +261,9 @@ struct SimInstance if (formal_database.count(cell)) return; - if (mem_database.count(cell)) + if (mem_cells.count(cell)) { - mem_state_t &mem = mem_database.at(cell); - - int num_rd_ports = cell->getParam(ID::RD_PORTS).as_int(); - - int size = cell->getParam(ID::SIZE).as_int(); - int offset = cell->getParam(ID::OFFSET).as_int(); - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - - if (cell->getParam(ID::RD_CLK_ENABLE).as_bool()) - log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(cell)); - - SigSpec rd_addr_sig = cell->getPort(ID::RD_ADDR); - SigSpec rd_data_sig = cell->getPort(ID::RD_DATA); - - for (int port_idx = 0; port_idx < num_rd_ports; port_idx++) - { - Const addr = get_state(rd_addr_sig.extract(port_idx*abits, abits)); - Const data = Const(State::Sx, width); - - if (addr.is_fully_def()) { - int index = addr.as_int() - offset; - if (index >= 0 && index < size) - data = mem.data.extract(index*width, width); - } - - set_state(rd_data_sig.extract(port_idx*width, width), data); - } - + dirty_memories.insert(mem_cells[cell]); return; } @@ -349,6 +326,29 @@ struct SimInstance log_error("Unsupported cell type: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell)); } + void update_memory(IdString id) { + auto &mdb = mem_database[id]; + auto &mem = *mdb.mem; + + for (int port_idx = 0; port_idx < GetSize(mem.rd_ports); port_idx++) + { + auto &port = mem.rd_ports[port_idx]; + Const addr = get_state(port.addr); + Const data = Const(State::Sx, mem.width); + + if (port.clk_enable) + log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(mem.memid)); + + if (addr.is_fully_def()) { + int index = addr.as_int() - mem.start_offset; + if (index >= 0 && index < mem.size) + data = mdb.data.extract(index*mem.width, mem.width); + } + + set_state(port.data, data); + } + } + void update_ph1() { pool<Cell*> queue_cells; @@ -380,6 +380,10 @@ struct SimInstance continue; } + for (auto &memid : dirty_memories) + update_memory(memid); + dirty_memories.clear(); + for (auto wire : queue_outports) if (instance->hasPort(wire->name)) { Const value = get_state(wire); @@ -423,50 +427,40 @@ struct SimInstance for (auto &it : mem_database) { - Cell *cell = it.first; - mem_state_t &mem = it.second; - - int num_wr_ports = cell->getParam(ID::WR_PORTS).as_int(); + mem_state_t &mdb = it.second; + auto &mem = *mdb.mem; - int size = cell->getParam(ID::SIZE).as_int(); - int offset = cell->getParam(ID::OFFSET).as_int(); - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - - Const wr_clk_enable = cell->getParam(ID::WR_CLK_ENABLE); - Const wr_clk_polarity = cell->getParam(ID::WR_CLK_POLARITY); - Const current_wr_clk = get_state(cell->getPort(ID::WR_CLK)); - - for (int port_idx = 0; port_idx < num_wr_ports; port_idx++) + for (int port_idx = 0; port_idx < GetSize(mem.wr_ports); port_idx++) { + auto &port = mem.wr_ports[port_idx]; Const addr, data, enable; - if (wr_clk_enable[port_idx] == State::S0) + if (!port.clk_enable) { - addr = get_state(cell->getPort(ID::WR_ADDR).extract(port_idx*abits, abits)); - data = get_state(cell->getPort(ID::WR_DATA).extract(port_idx*width, width)); - enable = get_state(cell->getPort(ID::WR_EN).extract(port_idx*width, width)); + addr = get_state(port.addr); + data = get_state(port.data); + enable = get_state(port.en); } else { - if (wr_clk_polarity[port_idx] == State::S1 ? - (mem.past_wr_clk[port_idx] == State::S1 || current_wr_clk[port_idx] != State::S1) : - (mem.past_wr_clk[port_idx] == State::S0 || current_wr_clk[port_idx] != State::S0)) + if (port.clk_polarity ? + (mdb.past_wr_clk[port_idx] == State::S1 || get_state(port.clk) != State::S1) : + (mdb.past_wr_clk[port_idx] == State::S0 || get_state(port.clk) != State::S0)) continue; - addr = mem.past_wr_addr.extract(port_idx*abits, abits); - data = mem.past_wr_data.extract(port_idx*width, width); - enable = mem.past_wr_en.extract(port_idx*width, width); + addr = mdb.past_wr_addr[port_idx]; + data = mdb.past_wr_data[port_idx]; + enable = mdb.past_wr_en[port_idx]; } if (addr.is_fully_def()) { - int index = addr.as_int() - offset; - if (index >= 0 && index < size) - for (int i = 0; i < width; i++) - if (enable[i] == State::S1 && mem.data.bits.at(index*width+i) != data[i]) { - mem.data.bits.at(index*width+i) = data[i]; - dirty_cells.insert(cell); + int index = addr.as_int() - mem.start_offset; + if (index >= 0 && index < mem.size) + for (int i = 0; i < mem.width; i++) + if (enable[i] == State::S1 && mdb.data.bits.at(index*mem.width+i) != data[i]) { + mdb.data.bits.at(index*mem.width+i) = data[i]; + dirty_memories.insert(mem.memid); did_something = true; } } @@ -497,13 +491,15 @@ struct SimInstance for (auto &it : mem_database) { - Cell *cell = it.first; mem_state_t &mem = it.second; - mem.past_wr_clk = get_state(cell->getPort(ID::WR_CLK)); - mem.past_wr_en = get_state(cell->getPort(ID::WR_EN)); - mem.past_wr_addr = get_state(cell->getPort(ID::WR_ADDR)); - mem.past_wr_data = get_state(cell->getPort(ID::WR_DATA)); + for (int i = 0; i < GetSize(mem.mem->wr_ports); i++) { + auto &port = mem.mem->wr_ports[i]; + mem.past_wr_clk[i] = get_state(port.clk); + mem.past_wr_en[i] = get_state(port.en); + mem.past_wr_addr[i] = get_state(port.addr); + mem.past_wr_data[i] = get_state(port.data); + } } for (auto cell : formal_database) @@ -558,17 +554,13 @@ struct SimInstance for (auto &it : mem_database) { - Cell *cell = it.first; mem_state_t &mem = it.second; - Const initval = mem.data; - - while (GetSize(initval) >= 2) { - if (initval[GetSize(initval)-1] != State::Sx) break; - if (initval[GetSize(initval)-2] != State::Sx) break; - initval.bits.pop_back(); - } - - cell->setParam(ID::INIT, initval); + mem.mem->clear_inits(); + MemInit minit; + minit.addr = mem.mem->start_offset; + minit.data = mem.data; + mem.mem->inits.push_back(minit); + mem.mem->emit(); } for (auto it : children) @@ -630,6 +622,7 @@ struct SimWorker : SimShared SimInstance *top = nullptr; std::ofstream vcdfile; pool<IdString> clock, clockn, reset, resetn; + std::string timescale; ~SimWorker() { @@ -641,6 +634,17 @@ struct SimWorker : SimShared if (!vcdfile.is_open()) return; + vcdfile << stringf("$version %s $end\n", yosys_version_str); + + std::time_t t = std::time(nullptr); + char mbstr[255]; + if (std::strftime(mbstr, sizeof(mbstr), "%c", std::localtime(&t))) { + vcdfile << stringf("$date ") << mbstr << stringf(" $end\n"); + } + + if (!timescale.empty()) + vcdfile << stringf("$timescale %s $end\n", timescale.c_str()); + int id = 1; top->write_vcd_header(vcdfile, id); @@ -751,7 +755,7 @@ struct SimWorker : SimShared struct SimPass : public Pass { SimPass() : Pass("sim", "simulate the circuit") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -780,6 +784,9 @@ struct SimPass : public Pass { log(" -zinit\n"); log(" zero-initialize all uninitialized regs and memories\n"); log("\n"); + log(" -timescale <string>\n"); + log(" include the specified timescale declaration in the vcd\n"); + log("\n"); log(" -n <integer>\n"); log(" number of cycles to simulate (default: 20)\n"); log("\n"); @@ -793,7 +800,7 @@ struct SimPass : public Pass { log(" enable debug output\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { SimWorker worker; int numcycles = 20; @@ -803,7 +810,9 @@ struct SimPass : public Pass { size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { if (args[argidx] == "-vcd" && argidx+1 < args.size()) { - worker.vcdfile.open(args[++argidx].c_str()); + std::string vcd_filename = args[++argidx]; + rewrite_filename(vcd_filename); + worker.vcdfile.open(vcd_filename.c_str()); continue; } if (args[argidx] == "-n" && argidx+1 < args.size()) { @@ -830,6 +839,10 @@ struct SimPass : public Pass { worker.resetn.insert(RTLIL::escape_id(args[++argidx])); continue; } + if (args[argidx] == "-timescale" && argidx+1 < args.size()) { + worker.timescale = args[++argidx]; + continue; + } if (args[argidx] == "-a") { worker.hide_internal = false; continue; diff --git a/passes/sat/supercover.cc b/passes/sat/supercover.cc index ba44f02d8..aacc044fb 100644 --- a/passes/sat/supercover.cc +++ b/passes/sat/supercover.cc @@ -25,7 +25,7 @@ PRIVATE_NAMESPACE_BEGIN struct SupercoverPass : public Pass { SupercoverPass() : Pass("supercover", "add hi/lo cover cells for each wire bit") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -35,7 +35,7 @@ struct SupercoverPass : public Pass { log("checking for a hi signal level and one checking for lo level.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { // bool flag_noinit = false; |