From a53104379dbe107c406d401afd3c02d95fbb63ee Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 20 Jan 2026 13:00:12 +0100 Subject: [PATCH 01/16] 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 ffb76a34864ef4b6bf1ee36a7a94a8a6370a68fa Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 28 Jan 2026 18:09:16 +0100 Subject: [PATCH 02/16] 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 03/16] 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 04/16] 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 05/16] 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 6f74c54c021dfffecb3b40fe6219af7360587ee4 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Thu, 29 Jan 2026 11:53:24 +0100 Subject: [PATCH 06/16] async2sync: $dffsr has undef output on S&R --- passes/sat/async2sync.cc | 28 ++++++++++++++++++++++------ 1 file changed, 22 insertions(+), 6 deletions(-) diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index eb3b154b2..19fd029d9 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -157,33 +157,49 @@ 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) + if (!ff.is_fine || sig_set.size() > 1) sig_set = module->Not(NEW_ID, sig_set); else sig_set = module->NotGate(NEW_ID, sig_set); } if (ff.pol_clr) { - if (!ff.is_fine) + if (!ff.is_fine || sig_clr.size() > 1) + 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.size() > 1) sig_clr = module->Not(NEW_ID, sig_clr); else sig_clr = module->NotGate(NEW_ID, sig_clr); } + SigSpec set_and_clr; + if (!ff.is_fine || sig_clr.size() > 1 || sig_set.size() > 1) + set_and_clr = module->And(NEW_ID, sig_set, sig_clr); + else + 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_inv); + module->addBwmux(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_inv); + module->addBwmux(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_inv); + 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_inv); + module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, ff.sig_q); } ff.sig_d = new_d; From 024408004a8c4dcc1c9e375a820f0f39a01bd4a6 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Fri, 27 Feb 2026 20:05:53 +0100 Subject: [PATCH 07/16] dfflibmap: allow formal dffsr mapping tests with clk2fflogic --- tests/techmap/dfflibmap_formal.ys | 44 +++++++++++++------------- tests/techmap/dfflibmap_proc_formal.ys | 4 +-- 2 files changed, 24 insertions(+), 24 deletions(-) diff --git a/tests/techmap/dfflibmap_formal.ys b/tests/techmap/dfflibmap_formal.ys index 7cacd4a91..3e57f2bbc 100644 --- a/tests/techmap/dfflibmap_formal.ys +++ b/tests/techmap/dfflibmap_formal.ys @@ -26,11 +26,11 @@ read_liberty dfflibmap_dffsr_s.lib copy top top_unmapped dfflibmap -liberty dfflibmap_dffsr_s.lib top -async2sync +clk2fflogic flatten opt_clean -purge equiv_make top top_unmapped equiv -equiv_induct equiv +equiv_induct -set-assumes equiv equiv_status -assert equiv ################################################################## @@ -62,11 +62,11 @@ read_liberty dfflibmap_dffsr_r.lib copy top top_unmapped dfflibmap -liberty dfflibmap_dffsr_r.lib top -async2sync +clk2fflogic flatten opt_clean -purge equiv_make top top_unmapped equiv -equiv_induct equiv +equiv_induct -set-assumes equiv equiv_status -assert equiv ################################################################## @@ -81,12 +81,12 @@ $_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1])); $_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2])); // Formal checking of directly instantiated DFFSR doesn't work at the moment -// likely due to an equiv_induct assume bug #5196 +// likely due to an equiv_induct -set-assumes assume bug #5196 -// // Workaround for DFFSR bug #5194 -// assume property (~R || ~S); -// $_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])); +// Workaround for DFFSR bug #5194 +assume property (~R || ~S); +$_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])); @@ -104,11 +104,11 @@ read_liberty dfflibmap_dffsr_not_next.lib copy top top_unmapped dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top -async2sync +clk2fflogic flatten opt_clean -purge equiv_make top top_unmapped equiv -equiv_induct equiv +equiv_induct -set-assumes equiv equiv_status -assert equiv ################################################################## @@ -123,12 +123,12 @@ $_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1])); $_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2])); // Formal checking of directly instantiated DFFSR doesn't work at the moment -// likely due to an equiv_induct assume bug #5196 +// likely due to an equiv_induct -set-assumes assume bug #5196 -// // Workaround for DFFSR bug #5194 -// assume property (~R || ~S); -// $_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])); +// Workaround for DFFSR inconsistency #5194 +assume property (~R || ~S); +$_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])); @@ -145,11 +145,11 @@ read_liberty dfflibmap_dffr_not_next.lib copy top top_unmapped dfflibmap -liberty dfflibmap_dffr_not_next.lib top -async2sync +clk2fflogic flatten opt_clean -purge equiv_make top top_unmapped equiv -equiv_induct equiv +equiv_induct -set-assumes equiv equiv_status -assert equiv ################################################################## @@ -180,11 +180,11 @@ copy top top_unmapped simplemap top dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top -async2sync +clk2fflogic flatten opt_clean -purge equiv_make top top_unmapped equiv -equiv_induct equiv +equiv_induct -set-assumes equiv equiv_status -assert equiv ################################################################## @@ -211,9 +211,9 @@ copy top top_unmapped simplemap top dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dff_not_next.lib top -async2sync +clk2fflogic flatten opt_clean -purge equiv_make top top_unmapped equiv -equiv_induct equiv +equiv_induct -set-assumes equiv equiv_status -assert equiv \ No newline at end of file diff --git a/tests/techmap/dfflibmap_proc_formal.ys b/tests/techmap/dfflibmap_proc_formal.ys index 263e3d4f3..cbc0f6c16 100644 --- a/tests/techmap/dfflibmap_proc_formal.ys +++ b/tests/techmap/dfflibmap_proc_formal.ys @@ -49,7 +49,7 @@ read_liberty dfflibmap_dffsr_s.lib copy top top_unmapped dfflibmap -liberty dfflibmap_dffsr_s.lib top -async2sync +clk2fflogic flatten opt_clean -purge equiv_make top top_unmapped equiv @@ -63,7 +63,7 @@ delete top equiv copy top_unmapped top dfflibmap -liberty dfflibmap_dffsr_r.lib top -async2sync +clk2fflogic flatten opt_clean -purge equiv_make top top_unmapped equiv From 22916aaab10d1f0703832274aa167cc8e5f48d7d Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Mon, 2 Mar 2026 22:39:21 +0100 Subject: [PATCH 08/16] read_liberty: model clear_preset_variable correctly --- frontends/liberty/liberty.cc | 105 +++++++++++++++++++++++------------ 1 file changed, 69 insertions(+), 36 deletions(-) diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc index 6d762477c..3d4e99310 100644 --- a/frontends/liberty/liberty.cc +++ b/frontends/liberty/liberty.cc @@ -213,6 +213,8 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node) const std::string name = RTLIL::unescape_id(module->name); bool clear_preset_reported = false; + std::optional clear_preset_var1; + std::optional clear_preset_var2; for (auto child : node->children) { if (child->id == "clocked_on") clk_sig = parse_func_expr(module, child->value.c_str()); @@ -222,16 +224,19 @@ 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; + + for (auto& [id, var] : {pair{"clear_preset_var1", &clear_preset_var1}, {"clear_preset_var2", &clear_preset_var2}}) + if (child->id == id) { + if (child->value.size() != 1) + log_error("Unexpected length of clear_preset_var* value %s in FF cell %s\n", child->value, name); + *var = child->value[0]; } + + } + if (clear_preset_var1 == 'X' || clear_preset_var2 == 'X') { + if (!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; } } @@ -261,36 +266,64 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node) } } - RTLIL::Cell *cell = module->addCell(NEW_ID, ID($_NOT_)); - cell->setPort(ID::A, iq_sig); - cell->setPort(ID::Y, iqn_sig); + for (auto& [out_sig, cp_var, neg] : {tuple{iq_sig, clear_preset_var1, false}, {iqn_sig, clear_preset_var2, true}}) { + SigSpec q_sig = out_sig; + if (neg) { + q_sig = module->addWire(NEW_ID, out_sig.as_wire()); + module->addNotGate(NEW_ID, q_sig, out_sig); + } - cell = module->addCell(NEW_ID, ""); - cell->setPort(ID::D, data_sig); - cell->setPort(ID::Q, iq_sig); - cell->setPort(ID::C, clk_sig); + RTLIL::Cell* cell = module->addCell(NEW_ID, ""); + cell->setPort(ID::D, data_sig); + cell->setPort(ID::Q, q_sig); + cell->setPort(ID::C, clk_sig); - if (clear_sig.size() == 0 && preset_sig.size() == 0) { - cell->type = stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N'); + if (clear_sig.size() == 0 && preset_sig.size() == 0) { + cell->type = stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N'); + } + + if (clear_sig.size() == 1 && preset_sig.size() == 0) { + cell->type = stringf("$_DFF_%c%c0_", clk_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N'); + cell->setPort(ID::R, clear_sig); + } + + if (clear_sig.size() == 0 && preset_sig.size() == 1) { + cell->type = stringf("$_DFF_%c%c1_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N'); + cell->setPort(ID::R, preset_sig); + } + + if (clear_sig.size() == 1 && preset_sig.size() == 1) { + cell->type = stringf("$_DFFSR_%c%c%c_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N'); + + SigBit s_sig = preset_sig; + SigBit r_sig = clear_sig; + if (cp_var && *cp_var != 'X') { + // Either set or reset dominates + bool set_dominates; + if (*cp_var == 'L') { + set_dominates = neg; + } else if (*cp_var == 'H') { + set_dominates = not neg; + } else { + log_error("FF cell %s has unsupported clear&preset behavior \'%c\'.\n", name, *cp_var); + } + log_debug("cell %s variable %d cp_var %c set dominates? %d\n", name, (int)neg + 1, *cp_var, set_dominates); + // S&R priority is well-defined now + if (set_dominates) { + r_sig = module->AndnotGate(NEW_ID, r_sig, s_sig); + } else { + s_sig = module->AndnotGate(NEW_ID, s_sig, r_sig); + } + } else { + log_debug("cell %s variable %d undef c&p behavior\n", name, (int)neg + 1); + } + + cell->setPort(ID::S, s_sig); + cell->setPort(ID::R, r_sig); + } + + log_assert(!cell->type.empty()); } - - if (clear_sig.size() == 1 && preset_sig.size() == 0) { - cell->type = stringf("$_DFF_%c%c0_", clk_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N'); - cell->setPort(ID::R, clear_sig); - } - - if (clear_sig.size() == 0 && preset_sig.size() == 1) { - cell->type = stringf("$_DFF_%c%c1_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N'); - cell->setPort(ID::R, preset_sig); - } - - if (clear_sig.size() == 1 && preset_sig.size() == 1) { - cell->type = stringf("$_DFFSR_%c%c%c_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N'); - cell->setPort(ID::S, preset_sig); - cell->setPort(ID::R, clear_sig); - } - - log_assert(!cell->type.empty()); } static bool create_latch(RTLIL::Module *module, const LibertyAst *node, bool flag_ignore_miss_data_latch) From 5b4603c54fbd1b3dc570b81ffffd5e67d39183f9 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Mar 2026 01:19:22 +0100 Subject: [PATCH 09/16] dfflibmap: fix formal $dffsr tests with sat, prove "no s&r" assumption only needed when appropriate --- ...ext.lib => dfflibmap_dffsr_not_next_l.lib} | 0 tests/techmap/dfflibmap_dffsr_x.lib | 33 +++++++ tests/techmap/dfflibmap_formal.ys | 89 ++++++++++++++----- tests/techmap/dfflibmap_proc_formal.ys | 37 ++++---- 4 files changed, 121 insertions(+), 38 deletions(-) rename tests/techmap/{dfflibmap_dffr_not_next.lib => dfflibmap_dffsr_not_next_l.lib} (100%) create mode 100644 tests/techmap/dfflibmap_dffsr_x.lib diff --git a/tests/techmap/dfflibmap_dffr_not_next.lib b/tests/techmap/dfflibmap_dffsr_not_next_l.lib similarity index 100% rename from tests/techmap/dfflibmap_dffr_not_next.lib rename to tests/techmap/dfflibmap_dffsr_not_next_l.lib diff --git a/tests/techmap/dfflibmap_dffsr_x.lib b/tests/techmap/dfflibmap_dffsr_x.lib new file mode 100644 index 000000000..91d702412 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_x.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 : X; + clear_preset_var2 : X; + } + 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 3e57f2bbc..e5e61cd62 100644 --- a/tests/techmap/dfflibmap_formal.ys +++ b/tests/techmap/dfflibmap_formal.ys @@ -8,6 +8,7 @@ $_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])); +assume property (~R || ~S); $_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])); @@ -29,9 +30,12 @@ dfflibmap -liberty dfflibmap_dffsr_s.lib top clk2fflogic flatten opt_clean -purge -equiv_make top top_unmapped equiv -equiv_induct -set-assumes equiv -equiv_status -assert equiv +miter -equiv -make_assert -flatten top_unmapped top miter +hierarchy -top miter +# Prove that this is equivalent with the assumption +sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter +# Prove that this is NOT equivalent WITHOUT the assumption +sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter ################################################################## @@ -44,6 +48,7 @@ $_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])); +assume property (~R || ~S); $_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])); @@ -65,9 +70,52 @@ dfflibmap -liberty dfflibmap_dffsr_r.lib top clk2fflogic flatten opt_clean -purge -equiv_make top top_unmapped equiv -equiv_induct -set-assumes equiv -equiv_status -assert equiv +miter -equiv -make_assert -flatten top_unmapped top miter +hierarchy -top miter +# Prove that this is equivalent with the assumption +sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter +# Prove that this is NOT equivalent WITHOUT the assumption +sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter + +################################################################## + +design -reset +read_verilog -sv -icells < Date: Tue, 3 Mar 2026 17:34:58 +0100 Subject: [PATCH 10/16] read_liberty: fix for msvc --- frontends/liberty/liberty.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc index 3d4e99310..04d5fd423 100644 --- a/frontends/liberty/liberty.cc +++ b/frontends/liberty/liberty.cc @@ -20,6 +20,7 @@ #include "passes/techmap/libparse.h" #include "kernel/register.h" #include "kernel/log.h" +#include YOSYS_NAMESPACE_BEGIN @@ -303,7 +304,7 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node) if (*cp_var == 'L') { set_dominates = neg; } else if (*cp_var == 'H') { - set_dominates = not neg; + set_dominates = !neg; } else { log_error("FF cell %s has unsupported clear&preset behavior \'%c\'.\n", name, *cp_var); } From 39343f5f33223e4f6482ae554133b4acb6d6bf40 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 4 Mar 2026 19:39:41 +0100 Subject: [PATCH 11/16] docs: document S&R undefined for $dffsr and $dffsre --- docs/source/cell/gate_reg_ff.rst | 8 ++++++++ docs/source/cell/word_reg.rst | 1 + 2 files changed, 9 insertions(+) diff --git a/docs/source/cell/gate_reg_ff.rst b/docs/source/cell/gate_reg_ff.rst index 2a31a3f09..2689c9def 100644 --- a/docs/source/cell/gate_reg_ff.rst +++ b/docs/source/cell/gate_reg_ff.rst @@ -154,6 +154,10 @@ to the following Verilog code template, where ``RST_EDGE`` is ``posedge`` if ``RST_LVL`` if ``1``, ``negedge`` otherwise, and ``SET_EDGE`` is ``posedge`` if ``SET_LVL`` if ``1``, ``negedge`` otherwise. +When both set and reset are active, the state and output is undefined. The Verilog +code model does not correspond to this due to limitations +of synthesizable Verilog. + .. code-block:: verilog :force: @@ -187,6 +191,10 @@ types relate to the following Verilog code template, where ``RST_EDGE`` is ``posedge`` if ``RST_LVL`` if ``1``, ``negedge`` otherwise, and ``SET_EDGE`` is ``posedge`` if ``SET_LVL`` if ``1``, ``negedge`` otherwise. +When both set and reset are active, the state and output is undefined. The Verilog +code model does not correspond to this due to limitations +of synthesizable Verilog. + .. code-block:: verilog :force: diff --git a/docs/source/cell/word_reg.rst b/docs/source/cell/word_reg.rst index 25c82b8e6..c5b369b33 100644 --- a/docs/source/cell/word_reg.rst +++ b/docs/source/cell/word_reg.rst @@ -78,6 +78,7 @@ D-type flip-flops with asynchronous set and reset are represented by `$dffsr` cells. As the `$dff` cells they have ``CLK``, ``D`` and ``Q`` ports. In addition they also have multi-bit ``SET`` and ``CLR`` input ports and the corresponding polarity parameters, like `$sr` cells. +When both set and reset are active, the state and output is undefined. D-type flip-flops with enable are represented by `$dffe`, `$adffe`, `$aldffe`, `$dffsre`, `$sdffe`, and `$sdffce` cells, which are enhanced variants of `$dff`, From 85013f9ed3216dae812438503e491580b0d0655e Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Fri, 6 Mar 2026 14:24:18 +0100 Subject: [PATCH 12/16] fixup! read_liberty: model clear_preset_variable correctly --- frontends/liberty/liberty.cc | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc index 04d5fd423..a006ae649 100644 --- a/frontends/liberty/liberty.cc +++ b/frontends/liberty/liberty.cc @@ -213,7 +213,6 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node) bool clk_polarity = true, clear_polarity = true, preset_polarity = true; const std::string name = RTLIL::unescape_id(module->name); - bool clear_preset_reported = false; std::optional clear_preset_var1; std::optional clear_preset_var2; for (auto child : node->children) { @@ -234,12 +233,6 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node) } } - if (clear_preset_var1 == 'X' || clear_preset_var2 == 'X') { - if (!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", name); @@ -844,3 +837,4 @@ skip_cell:; YOSYS_NAMESPACE_END + From 43ef4d290128b637378b355efcc7fc92977ddea5 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Mon, 9 Mar 2026 20:12:24 +0100 Subject: [PATCH 13/16] fixup! async2sync: $dffsr has undef output on S&R --- passes/sat/async2sync.cc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index 19fd029d9..707343a5d 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -160,26 +160,26 @@ struct Async2syncPass : public Pass { SigSpec sig_clr_inv = ff.sig_clr; if (!ff.pol_set) { - if (!ff.is_fine || sig_set.size() > 1) + if (!ff.is_fine) sig_set = module->Not(NEW_ID, sig_set); else sig_set = module->NotGate(NEW_ID, sig_set); } if (ff.pol_clr) { - if (!ff.is_fine || sig_clr.size() > 1) + 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.size() > 1) + if (!ff.is_fine) sig_clr = module->Not(NEW_ID, sig_clr); else sig_clr = module->NotGate(NEW_ID, sig_clr); } SigSpec set_and_clr; - if (!ff.is_fine || sig_clr.size() > 1 || sig_set.size() > 1) + if (!ff.is_fine) set_and_clr = module->And(NEW_ID, sig_set, sig_clr); else set_and_clr = module->AndGate(NEW_ID, sig_set, sig_clr); From 498cb79abe9b9239d5dcd5174185fc3bfd51261d Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Mon, 9 Mar 2026 20:18:56 +0100 Subject: [PATCH 14/16] async2sync: explain dffsr control signal variable polarity --- passes/sat/async2sync.cc | 3 +++ 1 file changed, 3 insertions(+) diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index 707343a5d..086dd5278 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -178,6 +178,9 @@ struct Async2syncPass : public Pass { sig_clr = module->NotGate(NEW_ID, sig_clr); } + // At this point, sig_set and sig_clr are now unconditionally + // active-high, and sig_clr_inv is inverted sig_clr + SigSpec set_and_clr; if (!ff.is_fine) set_and_clr = module->And(NEW_ID, sig_set, sig_clr); From 0e7f7c826d4451f084cc2bd84ad877d9c5d7280d Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Thu, 19 Mar 2026 19:27:30 +0100 Subject: [PATCH 15/16] simcells: $dffsr and derivatives undefine S&R in logic tables --- techlibs/common/simcells.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/techlibs/common/simcells.v b/techlibs/common/simcells.v index 1a113447e..3c38ca8b9 100644 --- a/techlibs/common/simcells.v +++ b/techlibs/common/simcells.v @@ -1613,6 +1613,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 0 0 - | x //- - - 0 - | 0 //- - 0 - - | 1 //- \ - - d | d @@ -1641,6 +1642,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 0 1 - | x //- - - 1 - | 0 //- - 0 - - | 1 //- \ - - d | d @@ -1669,6 +1671,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 1 0 - | x //- - - 0 - | 0 //- - 1 - - | 1 //- \ - - d | d @@ -1697,6 +1700,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 1 1 - | x //- - - 1 - | 0 //- - 1 - - | 1 //- \ - - d | d @@ -1725,6 +1729,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 0 0 - | x //- - - 0 - | 0 //- - 0 - - | 1 //- / - - d | d @@ -1753,6 +1758,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 0 1 - | x //- - - 1 - | 0 //- - 0 - - | 1 //- / - - d | d @@ -1781,6 +1787,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 1 0 - | x //- - - 0 - | 0 //- - 1 - - | 1 //- / - - d | d @@ -1809,6 +1816,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 1 1 - | x //- - - 1 - | 0 //- - 1 - - | 1 //- / - - d | d @@ -1837,6 +1845,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 0 - - | x //- - - 0 - - | 0 //- - 0 - - - | 1 //- \ - - 0 d | d @@ -1865,6 +1874,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 0 - - | x //- - - 0 - - | 0 //- - 0 - - - | 1 //- \ - - 1 d | d @@ -1893,6 +1903,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 1 - - | x //- - - 1 - - | 0 //- - 0 - - - | 1 //- \ - - 0 d | d @@ -1921,6 +1932,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 1 - - | x //- - - 1 - - | 0 //- - 0 - - - | 1 //- \ - - 1 d | d @@ -1949,6 +1961,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 0 - - | x //- - - 0 - - | 0 //- - 1 - - - | 1 //- \ - - 0 d | d @@ -1977,6 +1990,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 0 - - | x //- - - 0 - - | 0 //- - 1 - - - | 1 //- \ - - 1 d | d @@ -2005,6 +2019,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 1 - - | x //- - - 1 - - | 0 //- - 1 - - - | 1 //- \ - - 0 d | d @@ -2033,6 +2048,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 1 - - | x //- - - 1 - - | 0 //- - 1 - - - | 1 //- \ - - 1 d | d @@ -2061,6 +2077,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 0 - - | x //- - - 0 - - | 0 //- - 0 - - - | 1 //- / - - 0 d | d @@ -2089,6 +2106,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 0 - - | x //- - - 0 - - | 0 //- - 0 - - - | 1 //- / - - 1 d | d @@ -2117,6 +2135,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 1 - - | x //- - - 1 - - | 0 //- - 0 - - - | 1 //- / - - 0 d | d @@ -2145,6 +2164,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 1 - - | x //- - - 1 - - | 0 //- - 0 - - - | 1 //- / - - 1 d | d @@ -2173,6 +2193,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 0 - - | x //- - - 0 - - | 0 //- - 1 - - - | 1 //- / - - 0 d | d @@ -2201,6 +2222,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 0 - - | x //- - - 0 - - | 0 //- - 1 - - - | 1 //- / - - 1 d | d @@ -2229,6 +2251,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 1 - - | x //- - - 1 - - | 0 //- - 1 - - - | 1 //- / - - 0 d | d @@ -2257,6 +2280,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 1 - - | x //- - - 1 - - | 0 //- - 1 - - - | 1 //- / - - 1 d | d From 12b443e71c6d4767c65852b972abe40c3c44a3bf Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Thu, 19 Mar 2026 19:48:25 +0100 Subject: [PATCH 16/16] dfflibmap: consistent clk2fflogic usage in test --- tests/techmap/dfflibmap_proc_formal.ys | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/techmap/dfflibmap_proc_formal.ys b/tests/techmap/dfflibmap_proc_formal.ys index 43441a03a..88cb97cdb 100644 --- a/tests/techmap/dfflibmap_proc_formal.ys +++ b/tests/techmap/dfflibmap_proc_formal.ys @@ -78,7 +78,7 @@ delete top miter copy top_unmapped top dfflibmap -liberty dfflibmap_dffsr_mixedpol.lib top -async2sync +clk2fflogic flatten miter -equiv -make_assert -flatten top_unmapped top miter @@ -92,7 +92,7 @@ delete top miter copy top_unmapped top dfflibmap -liberty dfflibmap_dffsr_not_next.lib top -async2sync +clk2fflogic flatten miter -equiv -make_assert -flatten top_unmapped top miter