diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
index f81d492c8..3ebae4bc4 100644
--- a/passes/sat/formalff.cc
+++ b/passes/sat/formalff.cc
@@ -22,6 +22,7 @@
 #include "kernel/ffinit.h"
 #include "kernel/ff.h"
 #include "kernel/modtools.h"
+#include "kernel/mem.h"
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
@@ -549,6 +550,7 @@ struct FormalFfPass : public Pass {
 		bool flag_setundef = false;
 		bool flag_hierarchy = false;
 		bool flag_assume = false;
+		bool flag_declockgate = false;
 
 		log_header(design, "Executing FORMALFF pass.\n");
 
@@ -583,22 +585,232 @@ struct FormalFfPass : public Pass {
 				flag_assume = true;
 				continue;
 			}
+			if (args[argidx] == "-declockgate") {
+				flag_declockgate = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
 
-		if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume))
+		if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume || flag_declockgate))
 			log_cmd_error("One of the options -clk2ff, -ff2anyinit, -anyinit2ff, -hierarchy or -assume must be specified.\n");
 
 		if (flag_ff2anyinit && flag_anyinit2ff)
 			log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n");
 
+		if (flag_ff2anyinit && flag_declockgate)
+			log_cmd_error("The options -ff2anyinit and -declockgate are exclusive.\n");
+
 		if (flag_fine && !flag_anyinit2ff)
 			log_cmd_error("The option -fine requries the -anyinit2ff option.\n");
 
 		if (flag_fine && flag_clk2ff)
 			log_cmd_error("The options -fine and -clk2ff are exclusive.\n");
 
+		if (flag_declockgate)
+		{
+			for (auto module : design->selected_modules())
+			{
+				ModWalker modwalker(design);
+				modwalker.setup(module);
+				SigMap &sigmap = modwalker.sigmap;
+				FfInitVals initvals(&modwalker.sigmap, module);
+
+				dict<IdString, Mem> memories;
+
+				for (auto mem : Mem::get_selected_memories(module)) {
+					if (!mem.packed)
+						continue;
+					memories.emplace(mem.cell->name, std::move(mem));
+				}
+
+				dict<pair<SigBit, bool>, vector<Cell *>> clk_bits;
+				pool<SigBit> input_bits;
+				pool<pair<SigBit, bool>> input_clk_bits;
+				for (auto cell : module->selected_cells()) {
+					if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
+						FfData ff(&initvals, cell);
+						if (!ff.has_clk)
+							continue;
+						SigBit clk = sigmap(ff.sig_clk);
+						clk_bits[{clk, ff.pol_clk}].push_back(cell);
+					} else if (cell->type == ID($mem_v2)) {
+						auto const &mem = memories.at(cell->name);
+						for (auto &rd_port : mem.rd_ports)
+							if (rd_port.clk_enable)
+								clk_bits[{rd_port.clk, rd_port.clk_polarity}].push_back(mem.cell);
+						for (auto &wr_port : mem.wr_ports)
+							if (wr_port.clk_enable)
+								clk_bits[{wr_port.clk, wr_port.clk_polarity}].push_back(mem.cell);
+					}
+					// XXX $check $print
+				}
+
+				log_debug("%s has %d clk bits\n", log_id(module), GetSize(clk_bits));
+
+				for (auto port : module->ports) {
+					Wire *wire = module->wire(port);
+					if (!wire->port_input)
+						continue;
+					for (auto bit : SigSpec(wire)) {
+						input_bits.insert(bit);
+						for (bool pol : {false, true}) {
+							if (clk_bits.count({bit, pol})) {
+								input_clk_bits.insert({bit, pol});
+								clk_bits.erase({bit, pol});
+							}
+						}
+					}
+				}
+				log_debug("%s has %d non-input clk bits\n", log_id(module), GetSize(clk_bits));
+
+				if (clk_bits.empty())
+					continue;
+
+				for (auto &clk_bit : clk_bits)
+				{
+					SigBit clk = clk_bit.first.first;
+					bool pol_clk = clk_bit.first.second;
+					vector<Cell *> &clocked_cells = clk_bit.second;
+
+					if (!clk.is_wire()) {
+						log_debug("constant clk bit %s.%s\n", log_id(module), log_signal(SigSpec(clk)));
+						continue;
+					}
+					if (input_bits.count(clk)) {
+						log_debug("input clk bit %s.%s\n", log_id(module), log_signal(SigSpec(clk)));
+						continue;
+					}
+					auto found = modwalker.signal_drivers.find(clk);
+					if (found == modwalker.signal_drivers.end() || found->second.empty()) {
+						log_debug("undriven clk bit %s.%s\n", log_id(module), log_signal(SigSpec(clk)));
+						continue;
+					}
+
+					if (found->second.size() > 1) {
+						log_debug("multiple drivers for clk bit %s.%s\n", log_id(module), log_signal(SigSpec(clk)));
+						continue;
+					}
+
+					auto driver = *found->second.begin();
+
+					bool is_gate =
+					  pol_clk ? driver.cell->type.in(ID($and), ID($_AND_)) : driver.cell->type.in(ID($or), ID($_OR_));
+
+					if (!is_gate) {
+						log_debug("unsupported gating logic %s.%s (%s) for clock %s %s.%s\n", log_id(module),
+							  log_id(driver.cell), log_id(driver.cell->type), pol_clk ? "posedge" : "negedge",
+							  log_id(module), log_signal(SigSpec(clk)));
+
+						continue;
+					}
+					SigBit gate_clock = sigmap(driver.cell->getPort(ID::A)[driver.offset]);
+					SigBit gate_enable = sigmap(driver.cell->getPort(ID::B)[driver.offset]);
+
+					std::swap(gate_clock, gate_enable);
+					for (int i = 0; i < 2; i++) {
+						std::swap(gate_clock, gate_enable);
+
+						log_debug("clock %s.%s for gated clk bit %s.%s\n", log_id(module), log_signal(SigSpec(gate_clock)),
+							  log_id(module), log_signal(SigSpec(clk)));
+						log_debug("enable %s.%s for gated clk bit %s.%s\n", log_id(module), log_signal(SigSpec(gate_enable)),
+							  log_id(module), log_signal(SigSpec(clk)));
+
+						found = modwalker.signal_drivers.find(gate_enable);
+						if (found == modwalker.signal_drivers.end() || found->second.empty()) {
+							log_debug("undriven gate enable %s.%s of gated clk bit %s.%s\n", log_id(module),
+								  log_signal(SigSpec(gate_enable)), log_id(module), log_signal(SigSpec(clk)));
+							continue;
+						}
+						if (found->second.size() > 1) {
+							log_debug("multiple drivers for gate enable %s.%s of gated clk bit %s.%s\n", log_id(module),
+								  log_signal(SigSpec(gate_enable)), log_id(module), log_signal(SigSpec(clk)));
+							continue;
+						}
+
+						auto gate_driver = *found->second.begin();
+
+						if (!RTLIL::builtin_ff_cell_types().count(gate_driver.cell->type)) {
+							log_debug("non FF driver for gate enable %s.%s of gated clk bit %s.%s\n", log_id(module),
+								  log_signal(SigSpec(gate_enable)), log_id(module), log_signal(SigSpec(clk)));
+							continue;
+						}
+
+						FfData ff(&initvals, gate_driver.cell);
+						if (ff.has_gclk || ff.has_ce || ff.has_sr || ff.has_srst || ff.has_arst || (ff.has_aload && ff.has_clk)) {
+							log_debug(
+							  "FF driver for gate enable %s.%s of gated clk bit %s.%s has incompatible type: %s\n",
+							  log_id(module), log_signal(SigSpec(gate_enable)), log_id(module), log_signal(SigSpec(clk)),
+							  log_id(gate_driver.cell->type));
+							continue;
+						}
+
+						if (ff.has_aload) {
+							// this ff is intentionally not emitted!
+							ff.has_aload = false;
+							ff.has_clk = true;
+							ff.pol_clk = !ff.pol_arst;
+							ff.sig_clk = ff.sig_aload;
+							ff.sig_d = ff.sig_ad;
+						}
+
+						if (!ff.has_clk || sigmap(ff.sig_clk) != gate_clock || ff.pol_clk != pol_clk) {
+							log_debug("FF driver for gate enable %s.%s of gated clk bit %s.%s has incompatible clocking: "
+								  "%s %s.%s\n",
+								  log_id(module), log_signal(SigSpec(gate_enable)), log_id(module),
+								  log_signal(SigSpec(clk)), ff.pol_clk ? "posedge" : "negedge", log_id(module),
+								  log_signal(SigSpec(ff.sig_clk)));
+							continue;
+						}
+
+						SigBit sig_gate = ff.sig_d[gate_driver.offset];
+
+						log_debug("found clock gate, rewriting %d cells\n", GetSize(clocked_cells));
+
+						for (auto clocked_cell : clocked_cells) {
+							log_debug("rewriting cell %s.%s (%s)\n", log_id(module), log_id(clocked_cell),
+								  log_id(clocked_cell->type));
+
+							if (RTLIL::builtin_ff_cell_types().count(clocked_cell->type)) {
+
+								FfData ff(&initvals, clocked_cell);
+								log_assert(ff.has_clk);
+								ff.unmap_ce();
+								ff.pol_ce = pol_clk;
+								ff.sig_ce = sig_gate;
+								ff.has_ce = true;
+								ff.sig_clk = gate_clock;
+								ff.emit();
+							} else if (clocked_cell->type == ID($mem_v2)) {
+								auto &mem = memories.at(clocked_cell->name);
+								for (auto &rd_port : mem.rd_ports) {
+									if (rd_port.clk_enable && rd_port.clk == clk && rd_port.clk_polarity == pol_clk) {
+										log_warning("patching rd port\n");
+										rd_port.clk = gate_clock;
+										SigBit en_bit = pol_clk ? sig_gate : SigBit(module->Not(NEW_ID, sig_gate));
+										SigSpec en_mask = SigSpec(en_bit, GetSize(rd_port.en));
+										rd_port.en = module->And(NEW_ID, rd_port.en, en_mask);
+									}
+								}
+								for (auto &wr_port : mem.wr_ports) {
+									if (wr_port.clk_enable && wr_port.clk == clk && wr_port.clk_polarity == pol_clk) {
+										log_warning("patching wr port\n");
+										wr_port.clk = gate_clock;
+										SigBit en_bit = pol_clk ? sig_gate : SigBit(module->Not(NEW_ID, sig_gate));
+										SigSpec en_mask = SigSpec(en_bit, GetSize(wr_port.en));
+										wr_port.en = module->And(NEW_ID, wr_port.en, en_mask);
+									}
+								}
+							}
+						}
+
+						break;
+					}
+				}
+			}
+		}
+
 		for (auto module : design->selected_modules())
 		{
 			if (flag_setundef)
diff --git a/tests/various/formalff_declockgate.ys b/tests/various/formalff_declockgate.ys
new file mode 100644
index 000000000..30067b9d5
--- /dev/null
+++ b/tests/various/formalff_declockgate.ys
@@ -0,0 +1,79 @@
+# based on the peepopt_formal.ys test
+read_verilog -sv <<EOT
+module peepopt_formal_clockgateff_0(
+	input  logic clk_i,
+	input  logic ena_i,
+	input  logic enb_i,
+	input  logic enc_i,
+	input  logic d_0_i,
+	input  logic d_1_i,
+	output logic clk_o,
+	output logic d_0_o,
+	output logic d_1_o,
+    output logic d_2_o
+);
+
+logic en_latched;
+initial d_0_o = '0;
+initial d_1_o = '0;
+initial en_latched = '0;
+initial d_2_o = '0;
+
+reg mem [4];
+
+initial begin
+    mem[0] = 0;
+    mem[1] = 0;
+    mem[2] = 0;
+    mem[3] = 0;
+end
+reg [1:0] counter = 0;
+
+always_latch
+	if (!clk_i)
+		en_latched <= ena_i | enb_i;
+
+assign clk_o = en_latched & clk_i;
+
+always @(posedge clk_o)
+	d_0_o <= d_0_i;
+
+always @(posedge clk_o)
+	if (enc_i)
+		d_1_o <= d_1_i;
+
+
+always @(posedge clk_o) begin
+    counter <= counter + 1;
+    mem[counter] <= mem[counter] + 1;
+    d_2_o <= mem[counter] + 1;
+end;
+
+
+
+endmodule
+EOT
+
+# Check original design has latch
+prep -auto-top
+opt_dff
+select -assert-count 1 t:$dlatch
+select -assert-count 1 t:$dff
+select -assert-count 1 t:$dffe
+
+# Manually execute equiv_opt like pattern so clk2fflogic is called with
+# -nopeepopt, otherwise this doesn't test everything
+design -save preopt
+check -assert
+formalff -declockgate
+check -assert
+design -stash postopt
+
+# Create miter and clk2fflogic without peepopt
+design -copy-from preopt -as gold A:top
+design -copy-from postopt -as gate A:top
+clk2fflogic -nopeepopt
+
+miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
+memory_map -formal
+sat -prove-asserts -seq 16 -show-public -verify equiv