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
@@ -239,6 +239,17 @@ struct Smt2Worker
 			clock_negedge.erase(bit);
 		}
 
+		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)
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;