From ad8d899d6fb866930c4eb41d53983a59b13542f2 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 20 Jan 2026 13:00:12 +0100 Subject: [PATCH 01/11] 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 015b16467159457b4f777427cc91fc5fe10bb5df Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 28 Jan 2026 18:09:16 +0100 Subject: [PATCH 02/11] 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/11] 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/11] 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/11] 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 cf5afadf7b7da0a72efb126a91dd8ed592d36378 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Thu, 29 Jan 2026 11:53:24 +0100 Subject: [PATCH 06/11] 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 315692d804763fd9b61d4c71bec84525af2da490 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Thu, 29 Jan 2026 18:10:26 +0100 Subject: [PATCH 07/11] 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); } From 0a0cbf180586d5e93a01c86f8d9cb90840e857ad Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Fri, 27 Feb 2026 16:27:07 +0100 Subject: [PATCH 08/11] fixup! async2sync: $dffsr has undef output on S&R --- passes/sat/async2sync.cc | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index 291ebda33..19fd029d9 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -160,33 +160,38 @@ struct Async2syncPass : public Pass { 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) + 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 = module->AndGate(NEW_ID, sig_set, 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); tmp = module->And(NEW_ID, tmp, sig_clr_inv); - module->addMux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, new_d); + module->addBwmux(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_inv); - module->addMux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, ff.sig_q); + 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); tmp = module->AndGate(NEW_ID, tmp, sig_clr_inv); From 9d8b1ee43a1041af326269ab766a6595390c13c9 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Fri, 27 Feb 2026 20:05:53 +0100 Subject: [PATCH 09/11] 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 b2bf69be80d9321d543ddad34d0d45a3019859d5 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Mon, 2 Mar 2026 22:39:21 +0100 Subject: [PATCH 10/11] read_liberty: model clear_preset_variable correctly --- frontends/liberty/liberty.cc | 108 +++++++++++++++++++++++------------ 1 file changed, 72 insertions(+), 36 deletions(-) diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc index 6d762477c..1bcea024e 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,22 @@ 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]; } + + } + // 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 (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 +269,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 95978b68bedc086aa1e3db882dee038b509813c9 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Mar 2026 01:19:22 +0100 Subject: [PATCH 11/11] 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 <