From e36c71b5b743e578f3a965cda9926a426cd5c295 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 25 May 2023 12:48:02 +0200 Subject: [PATCH] Use clk2fflogic attr on cells to track original FF names in witnesses This makes clk2fflogic add an attr to $ff cells that carry the state of the emulated async FF. The $ff output doesn't have any async updates that happened in the current cycle, but the $ff input does, so the $ff input corresponds to the async FF's output in the original design. Hence this patch also makes the following changes to passes besides clk2fflogic (but only for FFs with the clk2fflogic attr set): * opt_clean treats the input as a register name (instead of the output) * rename -witness ensures that the input has a public name * the formal backends (smt2, btor, aiger) will use the input's name for the initial state of the FF in witness files * when sim reads a yw witness that assigns an initial value to the input signal, the state update is redirected to the output This ensures that yosys witness files for clk2fflogic designs have useful and stable public signal names. It also makes it possible to simulate a clk2fflogic witness on the original design (with some limitations when the original design is already using $ff cells). It might seem like setting the output of a clk2fflogic FF to update the input's initial value might not work in general, but it works fine for these reasons: * Witnesses for FFs are only present in the initial cycle, so we do not care about any later cycles. * The logic that clk2fflogic generates loops the output of the genreated FF back to the input, with muxes in between to apply any edge or level sensitive updates. So when there are no active updates in the current gclk cycle, there is a combinational path from the output back to the input. * The logic clk2fflogic generates makes sure that an edge sensitive update cannot be active in the first cycle (i.e. the past initial value is assumed to be whatever it needs to be to avoid an edge). * When a level sensitive update is active in the first gclk cycle, it is actively driving the output for the whole gclk cycle, so ignoring any witness initialization is the correct behavior. --- backends/aiger/aiger.cc | 3 +++ backends/btor/btor.cc | 5 ++++- backends/smt2/smt2.cc | 3 ++- passes/cmds/rename.cc | 12 ++++++++++-- passes/opt/opt_clean.cc | 6 ++++-- passes/sat/clk2fflogic.cc | 20 ++++++++++++++++---- passes/sat/sim.cc | 10 ++++++++++ 7 files changed, 49 insertions(+), 10 deletions(-) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 97acf937c..e39e17715 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -733,6 +733,9 @@ struct AigerWriter auto sig_qy = cell->getPort(cell->type.in(ID($anyconst), ID($anyseq)) ? ID::Y : ID::Q); SigSpec sig = sigmap(sig_qy); + if (cell->get_bool_attribute(ID(clk2fflogic))) + sig_qy = cell->getPort(ID::D); // For a clk2fflogic $_FF_ the named signal is the D input not the Q output + for (int i = 0; i < GetSize(sig_qy); i++) { if (sig_qy[i].wire == nullptr || sig[i].wire == nullptr) continue; diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 4c43e91e7..9cfd967e5 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -728,7 +728,10 @@ struct BtorWorker else btorf("%d state %d %s\n", nid, sid, log_id(symbol)); - ywmap_state(sig_q); + if (cell->get_bool_attribute(ID(clk2fflogic))) + ywmap_state(cell->getPort(ID::D)); // For a clk2fflogic FF the named signal is the D input not the Q output + else + ywmap_state(sig_q); if (nid_init_val >= 0) { int nid_init = next_nid++; diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 0ca3fbcac..7b48be299 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -626,8 +626,9 @@ struct Smt2Worker } bool init_only = cell->type.in(ID($anyconst), ID($anyinit), ID($allconst)); + bool clk2fflogic = cell->type == ID($anyinit) && cell->get_bool_attribute(ID(clk2fflogic)); int smtoffset = 0; - for (auto chunk : cell->getPort(QY).chunks()) { + for (auto chunk : cell->getPort(clk2fflogic ? ID::D : QY).chunks()) { if (chunk.is_wire()) decls.push_back(witness_signal(init_only ? "init" : "seq", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset)); smtoffset += chunk.width; diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index 6bd317ed0..da4ba2f17 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -139,7 +139,12 @@ static bool rename_witness(RTLIL::Design *design, dict &ca if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) { has_witness_signals = true; - auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y; + IdString QY; + bool clk2fflogic = false; + if (cell->type == ID($anyinit)) + QY = (clk2fflogic = cell->get_bool_attribute(ID(clk2fflogic))) ? ID::D : ID::Q; + else + QY = ID::Y; auto sig_out = cell->getPort(QY); for (auto chunk : sig_out.chunks()) { @@ -151,7 +156,10 @@ static bool rename_witness(RTLIL::Design *design, dict &ca auto new_id = module->uniquify("\\_witness_." + name); auto new_wire = module->addWire(new_id, GetSize(sig_out)); new_wire->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); - module->connect({sig_out, new_wire}); + if (clk2fflogic) + module->connect({new_wire, sig_out}); + else + module->connect({sig_out, new_wire}); cell->setPort(QY, new_wire); break; } diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index dde7c5299..cb2490dc7 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -292,10 +292,12 @@ bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos if (!purge_mode) for (auto &it : module->cells_) { RTLIL::Cell *cell = it.second; - if (ct_reg.cell_known(cell->type)) + if (ct_reg.cell_known(cell->type)) { + bool clk2fflogic = cell->get_bool_attribute(ID(clk2fflogic)); for (auto &it2 : cell->connections()) - if (ct_reg.cell_output(cell->type, it2.first)) + if (clk2fflogic ? it2.first == ID::D : ct_reg.cell_output(cell->type, it2.first)) register_signals.add(it2.second); + } for (auto &it2 : cell->connections()) connected_signals.add(it2.second); } diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index bba2cbbec..3dc96ecce 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -80,15 +80,27 @@ struct Clk2fflogicPass : public Pass { return module->Eqx(NEW_ID, {sampled_sig, sig}, polarity ? SigSpec {State::S0, State::S1} : SigSpec {State::S1, State::S0}); } // Sampled and current value of a data signal. - SampledSig sample_data(Module *module, SigSpec sig, RTLIL::Const init, bool is_fine) { + SampledSig sample_data(Module *module, SigSpec sig, RTLIL::Const init, bool is_fine, bool set_attribute = false) { std::string sig_str = log_signal(sig); sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end()); + + Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig)); sampled_sig->attributes[ID::init] = init; + + Cell *cell; if (is_fine) - module->addFfGate(NEW_ID, sig, sampled_sig); + cell = module->addFfGate(NEW_ID, sig, sampled_sig); else - module->addFf(NEW_ID, sig, sampled_sig); + cell = module->addFf(NEW_ID, sig, sampled_sig); + + if (set_attribute) { + for (auto &chunk : sig.chunks()) + if (chunk.wire != nullptr) + chunk.wire->set_bool_attribute(ID::keep); + cell->set_bool_attribute(ID(clk2fflogic)); + } + return {sampled_sig, sig}; } SigSpec mux(Module *module, SigSpec a, SigSpec b, SigSpec s, bool is_fine) { @@ -213,7 +225,7 @@ struct Clk2fflogicPass : public Pass { if (ff.has_clk) ff.unmap_ce_srst(); - auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine).sampled; + auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine, true).sampled; if (ff.has_clk) { // The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index b970ee568..2f353672b 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -140,6 +140,7 @@ struct SimInstance dict> upd_outports; dict in_parent_drivers; + dict clk2fflogic_drivers; pool dirty_bits; pool dirty_cells; @@ -270,6 +271,11 @@ struct SimInstance ff.past_srst = State::Sx; ff.data = ff_data; ff_database[cell] = ff; + + if (cell->get_bool_attribute(ID(clk2fflogic))) { + for (int i = 0; i < ff_data.width; i++) + clk2fflogic_drivers.emplace(sigmap(ff_data.sig_d[i]), sigmap(ff_data.sig_q[i])); + } } if (cell->is_mem_cell()) @@ -389,6 +395,10 @@ struct SimInstance auto sigbit = sig[i]; auto sigval = value[i]; + auto clk2fflogic_driver = clk2fflogic_drivers.find(sigbit); + if (clk2fflogic_driver != clk2fflogic_drivers.end()) + sigbit = clk2fflogic_driver->second; + auto in_parent_driver = in_parent_drivers.find(sigbit); if (in_parent_driver == in_parent_drivers.end()) set_state(sigbit, sigval);