diff options
| author | Jannis Harder <me@jix.one> | 2022-08-02 15:49:51 +0200 |
|---|---|---|
| committer | Jannis Harder <me@jix.one> | 2022-08-16 13:37:30 +0200 |
| commit | a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f (patch) | |
| tree | 0c4308ab9831f550d6e6d34a79239b569944c427 | |
| parent | c0063288d699f4f3edf5e0ff6ee1bd5cfa9ac884 (diff) | |
| download | yosys-a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f.tar.gz yosys-a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f.tar.bz2 yosys-a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f.zip | |
formalff: Set new replaced_by_gclk attribute on removed dff's clks
This attribute can be used by formal backends to indicate which clocks
were mapped to the global clock. Update the btor and smt2 backend which
already handle clock inputs to understand this attribute.
| -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; |