From 20a465e9f2f637add7128e429f8cc211cf496b71 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 4 Feb 2026 15:38:12 +0100 Subject: [PATCH] satgen: fix flip flop clock undef --- kernel/satgen.cc | 50 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 36 insertions(+), 14 deletions(-) diff --git a/kernel/satgen.cc b/kernel/satgen.cc index efbe177a0..868ca85c7 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -1266,27 +1266,49 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) else std::tie(d, undef_d) = mux(srst, undef_srst, rval, undef_rval, d, undef_d); } - std::vector q = importDefSigSpec(cell->getPort(ID::Q), timestep); - std::vector old_q = importDefSigSpec(cell->getPort(ID::Q), timestep-1); + std::vector q = importDefSigSpec(ff.sig_q, timestep); + std::vector old_q = importDefSigSpec(ff.sig_q, timestep-1); + std::vector undef_old_q; std::vector qq = model_undef ? ez->vec_var(q.size()) : q; + std::vector undef_q; + + int edge_detected = -1; + int undef_edge_detected = -1; + if (ff.has_clk) + { + // Detect the clock edge + int old_clk = importDefSigBit(ff.sig_clk, timestep-1); + int clk = importDefSigBit(ff.sig_clk, timestep); + int clk_active_level = ff.pol_clk ? ez->CONST_TRUE : ez->CONST_FALSE; + int old_clk_active = ez->IFF(old_clk, clk_active_level); + int clk_active = ez->IFF(clk, clk_active_level); + edge_detected = ez->AND(ez->NOT(old_clk_active), clk_active); + undef_edge_detected = -1; + if (model_undef) + { + undef_old_q = importUndefSigSpec(ff.sig_q, timestep-1); + undef_q = importUndefSigSpec(ff.sig_q, timestep); + int undef_old_clk = importUndefSigBit(ff.sig_clk, timestep-1); + int undef_clk = importUndefSigBit(ff.sig_clk, timestep); + undef_edge_detected = ez->OR(undef_clk, undef_old_clk); + } + } else { + // No clk signal -> always clocking + edge_detected = ez->CONST_TRUE; + undef_edge_detected = ez->CONST_FALSE; + } - // Detect the clock edge - int old_clk = importSigBit(ff.sig_clk, timestep-1); - int clk = importSigBit(ff.sig_clk, timestep); - int clk_active_level = ff.pol_clk ? ez->CONST_TRUE : ez->CONST_FALSE; - int old_clk_active = ez->IFF(old_clk, clk_active_level); - int clk_active = ez->IFF(clk, clk_active_level); - int edge_detected = ez->AND(ez->NOT(old_clk_active), clk_active); // If edge, then this Q is this D. Otherwise, it's last Q. - ez->assume(ez->vec_eq(ez->vec_ite(edge_detected, d, old_q), qq)); + { + std::vector mux_out, mux_out_undef; + std::tie(mux_out, mux_out_undef) = mux(edge_detected, undef_edge_detected, old_q, undef_old_q, d, undef_d); + ez->assume(ez->vec_eq(mux_out, qq)); + ez->assume(ez->vec_eq(mux_out_undef, undef_q)); + } if (model_undef) { - std::vector undef_old_q = importUndefSigSpec(cell->getPort(ID::Q), timestep-1); - std::vector undef_q = importUndefSigSpec(cell->getPort(ID::Q), timestep); - - ez->assume(ez->vec_eq(ez->vec_ite(edge_detected, undef_d, undef_old_q), undef_q)); undefGating(q, qq, undef_q); } }