From 80b21be65faf30c795d844859b7cb5d31fe66de2 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 20 Jan 2026 13:00:12 +0100 Subject: [PATCH 1/7] clk2fflogic: $dffsr has undef output on S&R --- passes/sat/clk2fflogic.cc | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index dd94dd0d7..b75c8aab1 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -123,10 +123,14 @@ struct Clk2fflogicPass : public Pass { return module->Mux(NEW_ID, a, b, s); } SigSpec bitwise_sr(Module *module, SigSpec a, SigSpec s, SigSpec r, bool is_fine) { - if (is_fine) - return module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r)); - else - return module->And(NEW_ID, module->Or(NEW_ID, a, s), module->Not(NEW_ID, r)); + if (is_fine) { + return module->MuxGate(NEW_ID, module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r)), RTLIL::State::Sx, module->AndGate(NEW_ID, s, r)); + } else { + std::vector y; + for (int i = 0; i < a.size(); i++) + y.push_back(module->MuxGate(NEW_ID, module->AndGate(NEW_ID, module->OrGate(NEW_ID, a[i], s[i]), module->NotGate(NEW_ID, r[i])), RTLIL::State::Sx, module->AndGate(NEW_ID, s[i], r[i]))); + return y; + } } void execute(std::vector args, RTLIL::Design *design) override { From 7ed0da0ef1ccf1ea2579fe61d9a1dde970a99874 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 28 Jan 2026 18:09:16 +0100 Subject: [PATCH 2/7] dfflibmap: test dffsr mapping without assume --- tests/techmap/dfflibmap_formal.ys | 36 +++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/tests/techmap/dfflibmap_formal.ys b/tests/techmap/dfflibmap_formal.ys index 71a52a261..02d4f2f0e 100644 --- a/tests/techmap/dfflibmap_formal.ys +++ b/tests/techmap/dfflibmap_formal.ys @@ -8,6 +8,42 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0])); $_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1])); $_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2])); +$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3])); +$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4])); + +$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5])); + +assign Q[11:6] = ~Q[5:0]; + +endmodule + +EOT + +proc +opt +read_liberty dfflibmap_dffsr.lib + +copy top top_unmapped +dfflibmap -liberty dfflibmap_dffsr.lib top + +async2sync +flatten +opt_clean -purge +equiv_make top top_unmapped equiv +equiv_induct equiv +equiv_status -assert equiv + +################################################################## + +design -reset +read_verilog -sv -icells < Date: Wed, 28 Jan 2026 18:11:55 +0100 Subject: [PATCH 3/7] dfflibmap: test dffsr with either priority liberty file --- tests/techmap/dfflibmap.ys | 4 +- ...libmap_dffsr.lib => dfflibmap_dffsr_r.lib} | 6 +-- tests/techmap/dfflibmap_dffsr_s.lib | 33 +++++++++++++++ tests/techmap/dfflibmap_formal.ys | 40 ++++++++++++++++++- 4 files changed, 76 insertions(+), 7 deletions(-) rename tests/techmap/{dfflibmap_dffsr.lib => dfflibmap_dffsr_r.lib} (92%) create mode 100644 tests/techmap/dfflibmap_dffsr_s.lib diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index 303daee48..b5ba8fe63 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -64,8 +64,8 @@ select -assert-count 1 t:dffe select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i design -load orig -dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib -dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib +dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib +dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib clean select -assert-count 5 t:$_NOT_ diff --git a/tests/techmap/dfflibmap_dffsr.lib b/tests/techmap/dfflibmap_dffsr_r.lib similarity index 92% rename from tests/techmap/dfflibmap_dffsr.lib rename to tests/techmap/dfflibmap_dffsr_r.lib index e735dae1a..f36e200a0 100644 --- a/tests/techmap/dfflibmap_dffsr.lib +++ b/tests/techmap/dfflibmap_dffsr_r.lib @@ -7,8 +7,8 @@ library(test) { clear : "CLEAR"; preset : "PRESET"; clear_preset_var1 : L; - clear_preset_var2 : L; - } + clear_preset_var2 : H; + } pin(D) { direction : input; } @@ -28,6 +28,6 @@ library(test) { pin(QN) { direction: output; function : "IQN"; - } + } } } diff --git a/tests/techmap/dfflibmap_dffsr_s.lib b/tests/techmap/dfflibmap_dffsr_s.lib new file mode 100644 index 000000000..cf930f3c7 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_s.lib @@ -0,0 +1,33 @@ +library(test) { + cell (dffsr) { + area : 6; + ff("IQ", "IQN") { + next_state : "D"; + clocked_on : "CLK"; + clear : "CLEAR"; + preset : "PRESET"; + clear_preset_var1 : H; + clear_preset_var2 : L; + } + pin(D) { + direction : input; + } + pin(CLK) { + direction : input; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +} diff --git a/tests/techmap/dfflibmap_formal.ys b/tests/techmap/dfflibmap_formal.ys index 02d4f2f0e..7cacd4a91 100644 --- a/tests/techmap/dfflibmap_formal.ys +++ b/tests/techmap/dfflibmap_formal.ys @@ -21,10 +21,46 @@ EOT proc opt -read_liberty dfflibmap_dffsr.lib +read_liberty dfflibmap_dffsr_s.lib copy top top_unmapped -dfflibmap -liberty dfflibmap_dffsr.lib top +dfflibmap -liberty dfflibmap_dffsr_s.lib top + +async2sync +flatten +opt_clean -purge +equiv_make top top_unmapped equiv +equiv_induct equiv +equiv_status -assert equiv + +################################################################## + +design -reset +read_verilog -sv -icells < Date: Wed, 28 Jan 2026 18:26:26 +0100 Subject: [PATCH 4/7] dfflibmap: test dffsr and dffsre from proc with equiv --- tests/techmap/dfflibmap_proc_formal.ys | 99 ++++++++++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 tests/techmap/dfflibmap_proc_formal.ys diff --git a/tests/techmap/dfflibmap_proc_formal.ys b/tests/techmap/dfflibmap_proc_formal.ys new file mode 100644 index 000000000..263e3d4f3 --- /dev/null +++ b/tests/techmap/dfflibmap_proc_formal.ys @@ -0,0 +1,99 @@ +################################################################## + +read_verilog -sv -icells < Date: Wed, 28 Jan 2026 18:40:20 +0100 Subject: [PATCH 5/7] liberty: warn if dffsr has clear&preset well defined --- frontends/liberty/liberty.cc | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc index 0aa1cee09..6d762477c 100644 --- a/frontends/liberty/liberty.cc +++ b/frontends/liberty/liberty.cc @@ -210,7 +210,9 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node) auto [iq_sig, iqn_sig] = find_latch_ff_wires(module, node); RTLIL::SigSpec clk_sig, data_sig, clear_sig, preset_sig; bool clk_polarity = true, clear_polarity = true, preset_polarity = true; + const std::string name = RTLIL::unescape_id(module->name); + bool clear_preset_reported = false; for (auto child : node->children) { if (child->id == "clocked_on") clk_sig = parse_func_expr(module, child->value.c_str()); @@ -220,10 +222,21 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node) clear_sig = parse_func_expr(module, child->value.c_str()); if (child->id == "preset") preset_sig = parse_func_expr(module, child->value.c_str()); + // TODO with $priority cell, any pair of clear_preset_var1 clear_preset_var2 + // can be modeled as a pair of flops with different priority + // rather than just having IQN = ~IQ + if (child->id == "clear_preset_var1" || child->id == "clear_preset_var2") { + if (child->value.size() != 1) + log_error("Unexpected length of clear_preset_var* value %s in FF cell %s\n", child->value, name); + if (child->value[0] != 'X' && !clear_preset_reported) { + log_warning("FF cell %s has well-defined clear&preset behavior, but Yosys models it as undefined\n", name); + clear_preset_reported = true; + } + } } if (clk_sig.size() == 0 || data_sig.size() == 0) - log_error("FF cell %s has no next_state and/or clocked_on attribute.\n", RTLIL::unescape_id(module->name)); + log_error("FF cell %s has no next_state and/or clocked_on attribute.\n", name); for (bool rerun_invert_rollback = true; rerun_invert_rollback;) { From 3e84b732ee48c449ffdf65cee154fd36e3d38358 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Thu, 29 Jan 2026 11:53:24 +0100 Subject: [PATCH 6/7] async2sync: $dffsr has undef output on S&R --- passes/sat/async2sync.cc | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index eb3b154b2..e0f9b6a4a 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -172,18 +172,23 @@ struct Async2syncPass : public Pass { sig_clr = module->NotGate(NEW_ID, sig_clr); } + SigSpec set_and_clr = module->AndGate(NEW_ID, sig_set, sig_clr); if (!ff.is_fine) { SigSpec tmp = module->Or(NEW_ID, ff.sig_d, sig_set); - module->addAnd(NEW_ID, tmp, sig_clr, new_d); + tmp = module->And(NEW_ID, tmp, sig_clr); + module->addMux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, new_d); tmp = module->Or(NEW_ID, new_q, sig_set); - module->addAnd(NEW_ID, tmp, sig_clr, ff.sig_q); + tmp = module->And(NEW_ID, tmp, sig_clr); + module->addMux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, ff.sig_q); } else { SigSpec tmp = module->OrGate(NEW_ID, ff.sig_d, sig_set); - module->addAndGate(NEW_ID, tmp, sig_clr, new_d); + tmp = module->AndGate(NEW_ID, tmp, sig_clr); + module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, new_d); tmp = module->OrGate(NEW_ID, new_q, sig_set); - module->addAndGate(NEW_ID, tmp, sig_clr, ff.sig_q); + tmp = module->AndGate(NEW_ID, tmp, sig_clr); + module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, ff.sig_q); } ff.sig_d = new_d; From cbf3407585b59e3acc23a7b371f4ac75b850ad15 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Thu, 29 Jan 2026 18:10:26 +0100 Subject: [PATCH 7/7] fixup! async2sync: $dffsr has undef output on S&R --- passes/sat/async2sync.cc | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index e0f9b6a4a..291ebda33 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -157,6 +157,7 @@ struct Async2syncPass : public Pass { SigSpec sig_set = ff.sig_set; SigSpec sig_clr = ff.sig_clr; + SigSpec sig_clr_inv = ff.sig_clr; if (!ff.pol_set) { if (!ff.is_fine) @@ -166,6 +167,11 @@ struct Async2syncPass : public Pass { } if (ff.pol_clr) { + if (!ff.is_fine) + sig_clr_inv = module->Not(NEW_ID, sig_clr); + else + sig_clr_inv = module->NotGate(NEW_ID, sig_clr); + } else { if (!ff.is_fine) sig_clr = module->Not(NEW_ID, sig_clr); else @@ -175,19 +181,19 @@ struct Async2syncPass : public Pass { SigSpec set_and_clr = module->AndGate(NEW_ID, sig_set, sig_clr); if (!ff.is_fine) { SigSpec tmp = module->Or(NEW_ID, ff.sig_d, sig_set); - tmp = module->And(NEW_ID, tmp, sig_clr); + tmp = module->And(NEW_ID, tmp, sig_clr_inv); module->addMux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, new_d); tmp = module->Or(NEW_ID, new_q, sig_set); - tmp = module->And(NEW_ID, tmp, sig_clr); + tmp = module->And(NEW_ID, tmp, sig_clr_inv); module->addMux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, ff.sig_q); } else { SigSpec tmp = module->OrGate(NEW_ID, ff.sig_d, sig_set); - tmp = module->AndGate(NEW_ID, tmp, sig_clr); + tmp = module->AndGate(NEW_ID, tmp, sig_clr_inv); module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, new_d); tmp = module->OrGate(NEW_ID, new_q, sig_set); - tmp = module->AndGate(NEW_ID, tmp, sig_clr); + tmp = module->AndGate(NEW_ID, tmp, sig_clr_inv); module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, ff.sig_q); }