diff options
| -rw-r--r-- | backends/btor/btor.cc | 10 | ||||
| -rw-r--r-- | backends/smt2/smt2.cc | 11 | ||||
| -rw-r--r-- | kernel/constids.inc | 1 | ||||
| -rw-r--r-- | passes/sat/formalff.cc | 22 |
4 files changed, 44 insertions, 0 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 831a3ada2..6dae7156a 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1112,6 +1112,16 @@ struct BtorWorker btorf("%d input %d%s\n", nid, sid, getinfo(wire).c_str()); add_nid_sig(nid, sig); + + if (!info_filename.empty()) { + auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk); + if (gclk_attr != wire->attributes.end()) { + if (gclk_attr->second == State::S1) + info_clocks[nid] |= 1; + else if (gclk_attr->second == State::S0) + info_clocks[nid] |= 2; + } + } } btorf_pop("inputs"); diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index f6c3560c1..126ee1175 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -241,6 +241,17 @@ struct Smt2Worker for (auto wire : module->wires()) { + auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk); + if (gclk_attr != wire->attributes.end()) { + if (gclk_attr->second == State::S1) + clock_posedge.insert(sigmap(wire)); + else if (gclk_attr->second == State::S0) + clock_negedge.insert(sigmap(wire)); + } + } + + for (auto wire : module->wires()) + { if (!wire->port_input || GetSize(wire) != 1) continue; SigBit bit = sigmap(wire); diff --git a/kernel/constids.inc b/kernel/constids.inc index 0f6dfc29b..239381f85 100644 --- a/kernel/constids.inc +++ b/kernel/constids.inc @@ -171,6 +171,7 @@ X(RD_TRANSPARENCY_MASK) X(RD_TRANSPARENT) X(RD_WIDE_CONTINUATION) X(reg) +X(replaced_by_gclk) X(reprocess_after) X(rom_block) X(rom_style) diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc index fe6f98c16..0c85c3442 100644 --- a/passes/sat/formalff.cc +++ b/passes/sat/formalff.cc @@ -145,6 +145,28 @@ struct FormalFfPass : public Pass { log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n", log_id(cell), log_id(cell->type), log_id(module)); + auto clk_wire = ff.sig_clk.is_wire() ? ff.sig_clk.as_wire() : nullptr; + + if (clk_wire == nullptr) { + clk_wire = module->addWire(NEW_ID); + module->connect(RTLIL::SigBit(clk_wire), ff.sig_clk); + } + + auto clk_polarity = ff.pol_clk ? State::S1 : State::S0; + + std::string attribute = clk_wire->get_string_attribute(ID::replaced_by_gclk); + + auto &attr = clk_wire->attributes[ID::replaced_by_gclk]; + + if (!attr.empty() && attr != clk_polarity) + log_error("CLK %s on %s (%s) from module %s also used with opposite polarity, run clk2fflogic instead.\n", + log_id(clk_wire), log_id(cell), log_id(cell->type), log_id(module)); + + attr = clk_polarity; + clk_wire->set_bool_attribute(ID::keep); + + // TODO propagate the replaced_by_gclk attribute upwards throughout the hierarchy + ff.unmap_ce_srst(); ff.has_clk = false; ff.has_gclk = true; |